(=> (= (Tensor-To-Matrix ?T ?Basis) ?M)
(=> (= (Tensor-Order ?T) 2)
(Square-Matrix ?M)
(= (Size ?M) (Spatial.Dimension ?T))
(Forall (?I ?J)
(= (Value ?M ?I ?J) (Dyad-Component ?T ?I ?J ?Basis)))))
(=> (= (Tensor-To-Matrix ?T ?Basis) ?M)
(=> (= (Tensor-Order ?T) 1)
(= (Row-Dimension ?M) 1)
(= (Column-Dimension ?M) (Spatial.Dimension ?T))
(Forall (?I)
(= (Value ?M 1 ?I) (Vector-Component ?T ?I ?Basis)))))
(=> (= (Tensor-To-Matrix ?T ?Basis) ?M) (Matrix-Quantity ?M))
(=> (= (Tensor-To-Matrix ?T ?Basis) ?M)
(=> (Member ?Q (Tensor-Order ?T)) (Member ?Q (Setof 1 2))))
(=> (= (Tensor-To-Matrix ?T ?Basis) ?M) (Orthonormal-Basis ?Basis))
(=> (= (Tensor-To-Matrix ?T ?Basis) ?M) (Tensor-Quantity ?T))
(=> (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))))))))