The DOT or inner product is defined for tensors of the same spatial dimension. The quantity.dimension of the product equals the product of the quantity.dimensions of the operands. The dot operator distributes over addition.For vectors:
When the operands are both vector-quantities, the dot (scalar product) can be decomposed into the multiplication of a row- and a column-matrix. The product is a scalar (zero order tensor) and is the sum of the products of the corresponding scalar components of the argument vectors for a common basis.
For dyads:
When the operands are both dyads, the dot product can be decomposed into a multiplication of square matrices (with dimension equal to the spatial.dimension of the dyads). The product is a dyad (second order tensor) and is equal to the sum of the products of the corresponding scalar components of the argument tensors for a common basis.
For dyad dot vector:
The dot product of a dyad and a vector-quantity results in a vector-quantity. This product can be decomposed into the multiplication of a square matrix an a column-matrix or row-matrix. The product is a vector-quantity (first order tensor) and is equal to the sum of the products of the corresponding scalar components of the argument tensors for a common basis.
The reverse, vector dot dyad, is analogous.
(=> (And (Vector-Quantity ?V1) (Dyad ?T1))
(<=> (Dot ?V1 ?T1 ?V)
(And (Vector-Quantity ?V)
(Forall (?B)
(= ?T
(The-Vector-Quantity (* (Tensor-To-Matrix ?V1
?B)
(Tensor-To-Matrix ?T1
?B))
?B)))
(Forall
(?B ?I ?J)
(=> (= (Basis.Dimension ?B)
(Spatial.Dimension ?V1))
(= ?T
(Summation
(Lambda
(?I)
(* (Basis.Vec ?B ?I)
(Summation
(Lambda (?J)
(* (Vector-Component
?V1
?J
?B)
(Dyad-Component ?T1
?J
?I
?B)))
1
(Spatial.Dimension ?V1))))
1
(Spatial.Dimension ?V1))))))))
(=> (And (Dyad ?T1) (Vector-Quantity ?V1))
(<=> (Dot ?T1 ?V1 ?V)
(And (Vector-Quantity ?V)
(Forall
(?B)
(= ?T
(The-Vector-Quantity
(Transpose (* (Tensor-To-Matrix ?T1 ?B)
(Transpose (Tensor-To-Matrix
?V1
?B))))
?B)))
(Forall
(?B ?I ?J)
(=> (= (Basis.Dimension ?B)
(Spatial.Dimension ?V1))
(= ?T
(Summation
(Lambda
(?I)
(* (Basis.Vec ?B ?I)
(Summation
(Lambda (?J)
(* (Dyad-Component ?T1
?I
?J
?B)
(Vector-Component
?V1
?J
?B)))
1
(Spatial.Dimension ?V1))))
1
(Spatial.Dimension ?V1))))))))
(=> (And (Dyad ?T1) (Dyad ?T2))
(<=> (Dot ?T1 ?T2 ?T)
(And (Dyad ?T)
(Forall (?B)
(= ?T
(The-Dyad (* (Tensor-To-Matrix ?T1 ?B)
(Tensor-To-Matrix ?T2 ?B))
?B)))
(Forall
(?B ?I ?J)
(=> (= (Basis.Dimension ?B)
(Spatial.Dimension ?T1))
(= ?T
(Summation
(Lambda
(?I)
(Summation
(Lambda (?J)
(* (* (Basis.Vec ?B ?I)
(Basis.Vec ?B ?J))
(* (Dyad-Component ?T1
?I
?J
?B)
(Dyad-Component ?T2
?J
?I
?B))))
1
(Spatial.Dimension ?T1)))
1
(Spatial.Dimension ?T1))))))))
(=> (And (Vector-Quantity ?V1) (Vector-Quantity ?V2))
(<=> (Dot ?V1 ?V2 ?S)
(And (Scalar-Quantity ?S)
(Forall (?B)
(= ?S
(Value (* (Tensor-To-Matrix ?V1 ?B)
(Transpose (Tensor-To-Matrix ?V2
?B)))
11)))
(Forall (?B ?J)
(=> (= (Basis.Dimension ?B)
(Spatial.Dimension ?V1))
(= ?S
(Summation (Lambda (?J)
(* (Vector-Component
?V1
?J
?B)
(Vector-Component
?V2
?J
?B)))
1
(Spatial.Dimension ?V1))))))))
(Nth-Domain Dot 3 Tensor-Quantity) (Nth-Domain Dot 2 Tensor-Quantity) (Nth-Domain Dot 1 Tensor-Quantity) (Distributes Dot + Tensor-Quantity)
(= (Dot ?V ?V) 1)
(<=> (Unit-Vec ?V)
(And (Vector-Quantity ?V)
(= (Quantity.Dimension ?V) Identity-Dimension)
(= (Dot ?V ?V) 1)))
(Forall (?N1 ?N2)
(=> (And (Positive-Integer ?N1)
(Positive-Integer ?N2)
(=< ?N1 (Basis.Dimension ?B))
(=< ?N2 (Basis.Dimension ?B)))
(=> (= ?N1 ?N2)
(= (Dot (Basis.Vec ?B ?N1) (Basis.Vec ?B ?N2)) 1))
(=> (/= ?N1 ?N2)
(= (Dot (Basis.Vec ?B ?N1) (Basis.Vec ?B ?N2)) 0))))
(=> (Orthonormal-Basis ?B)
(And (Value-Cardinality ?B Basis.Dimension 1)
(Forall (?N)
(=> (And (Positive-Integer ?N)
(=< ?N (Basis.Dimension ?B)))
(Defined (Basis.Vec ?B ?N))))
(Forall (?N1 ?N2)
(=> (And (Positive-Integer ?N1)
(Positive-Integer ?N2)
(=< ?N1 (Basis.Dimension ?B))
(=< ?N2 (Basis.Dimension ?B)))
(=> (= ?N1 ?N2)
(= (Dot (Basis.Vec ?B ?N1)
(Basis.Vec ?B ?N2))
1))
(=> (/= ?N1 ?N2)
(= (Dot (Basis.Vec ?B ?N1)
(Basis.Vec ?B ?N2))
0))))))
(=> (= (Vector-Component ?V ?I ?B) ?S)
(= ?S (Dot ?V (Basis.Vec ?B ?I))))
(=> (= (Dyad-Component ?T ?I ?J ?Basis) ?S)
(= ?S (Dot (Basis.Vec ?Basis ?I) (Dot ?T (Basis.Vec ?B ?J)))))
(=> (And (Vector-Quantity ?V1) (Dyad ?T1))
(<=> (Dot ?V1 ?T1 ?V)
(And (Vector-Quantity ?V)
(Forall (?B)
(= ?T
(The-Vector-Quantity (* (Tensor-To-Matrix ?V1
?B)
(Tensor-To-Matrix ?T1
?B))
?B)))
(Forall
(?B ?I ?J)
(=> (= (Basis.Dimension ?B)
(Spatial.Dimension ?V1))
(= ?T
(Summation
(Lambda
(?I)
(* (Basis.Vec ?B ?I)
(Summation
(Lambda (?J)
(* (Vector-Component
?V1
?J
?B)
(Dyad-Component ?T1
?J
?I
?B)))
1
(Spatial.Dimension ?V1))))
1
(Spatial.Dimension ?V1))))))))
(=> (And (Dyad ?T1) (Vector-Quantity ?V1))
(<=> (Dot ?T1 ?V1 ?V)
(And (Vector-Quantity ?V)
(Forall
(?B)
(= ?T
(The-Vector-Quantity
(Transpose (* (Tensor-To-Matrix ?T1 ?B)
(Transpose (Tensor-To-Matrix
?V1
?B))))
?B)))
(Forall
(?B ?I ?J)
(=> (= (Basis.Dimension ?B)
(Spatial.Dimension ?V1))
(= ?T
(Summation
(Lambda
(?I)
(* (Basis.Vec ?B ?I)
(Summation
(Lambda (?J)
(* (Dyad-Component ?T1
?I
?J
?B)
(Vector-Component
?V1
?J
?B)))
1
(Spatial.Dimension ?V1))))
1
(Spatial.Dimension ?V1))))))))
(=> (And (Dyad ?T1) (Dyad ?T2))
(<=> (Dot ?T1 ?T2 ?T)
(And (Dyad ?T)
(Forall (?B)
(= ?T
(The-Dyad (* (Tensor-To-Matrix ?T1 ?B)
(Tensor-To-Matrix ?T2 ?B))
?B)))
(Forall
(?B ?I ?J)
(=> (= (Basis.Dimension ?B)
(Spatial.Dimension ?T1))
(= ?T
(Summation
(Lambda
(?I)
(Summation
(Lambda (?J)
(* (* (Basis.Vec ?B ?I)
(Basis.Vec ?B ?J))
(* (Dyad-Component ?T1
?I
?J
?B)
(Dyad-Component ?T2
?J
?I
?B))))
1
(Spatial.Dimension ?T1)))
1
(Spatial.Dimension ?T1))))))))
(=> (And (Vector-Quantity ?V1) (Vector-Quantity ?V2))
(<=> (Dot ?V1 ?V2 ?S)
(And (Scalar-Quantity ?S)
(Forall (?B)
(= ?S
(Value (* (Tensor-To-Matrix ?V1 ?B)
(Transpose (Tensor-To-Matrix ?V2
?B)))
11)))
(Forall (?B ?J)
(=> (= (Basis.Dimension ?B)
(Spatial.Dimension ?V1))
(= ?S
(Summation (Lambda (?J)
(* (Vector-Component
?V1
?J
?B)
(Vector-Component
?V2
?J
?B)))
1
(Spatial.Dimension ?V1))))))))
(=> (= (Dot ?T1 ?T2) ?T)
(= (Quantity.Dimension ?T)
(* (Quantity.Dimension ?T1) (Quantity.Dimension ?T2))))
(=> (= (Dot ?T1 ?T2) ?T)
(= (Spatial.Dimension ?T1) (Spatial.Dimension ?T2)))
(=> (= (The-Zero-Vector-Of-Type ?Spatdim ?Physdim) ?V0)
(Forall (?V)
(=> (Vector-Quantity ?V)
(= (Dot ?V ?V0)
(The-Zero-Scalar-For-Dimension ?Physdim)))))
(=> (= (The-Zero-Dyad-Of-Type ?Spatdim ?Physdim) ?V0)
(Forall (?V)
(=> (Dyad ?V)
(= (Dot ?V ?V0)
(The-Zero-Scalar-For-Dimension ?Physdim)))))