Function THE-VECTOR-QUANTITY

• Defined in theory: Tensor-quantities
• Source code: tensor-quantities.lisp

Slots on this function:

Documentation:

Constructor function for vector quantities (first order tensors). Requires a matrix and an orthnormal-basis as arguments. The constructed vector-quantity is equal to the sum of matrix elements multiplied by their corresponding basis vectors.

Instance-Of: Function

Arity: 3

Equivalence Axioms:

(<=> (The-Vector-Quantity ?M ?B)
     (And (Matrix-Quantity ?M)
          (Row-Matrix ?M)
          (Orthonormal-Basis ?B)
          (= (Quantity.Dimension ?V) (Quantity.Dimension ?M))
          (= (Column-Dimension ?M) (Basis.Dimension ?B))
          (= (Spatial.Dimension ?V) (Column-Dimension ?M))
          (Vector-Quantity ?V)
          (= ?V
             (Summation (Lambda (?J)
                                (* (Value ?M 1 ?J) (Basis.Vec ?B ?J)))
                        1
                        (Spatial.Dimension ?V)))))

Axioms:

(Nth-Domain The-Vector-Quantity 3 Vector-Quantity)

(Nth-Domain The-Vector-Quantity 2 Orthonormal-Basis)

(Nth-Domain The-Vector-Quantity 1 Row-Matrix)

(Nth-Domain The-Vector-Quantity 1 Matrix-Quantity)

Other Related Axioms:

(=> (= (The-Vector-Quantity ?M ?B) ?V)
    (= ?V
       (Summation (Lambda (?J) (* (Value ?M 1 ?J) (Basis.Vec ?B ?J)))
                  1
                  (Spatial.Dimension ?V))))

(=> (= (The-Vector-Quantity ?M ?B) ?V) (Vector-Quantity ?V))

(=> (= (The-Vector-Quantity ?M ?B) ?V)
    (= (Spatial.Dimension ?V) (Column-Dimension ?M)))

(=> (= (The-Vector-Quantity ?M ?B) ?V)
    (= (Column-Dimension ?M) (Basis.Dimension ?B)))

(=> (= (The-Vector-Quantity ?M ?B) ?V)
    (= (Quantity.Dimension ?V) (Quantity.Dimension ?M)))

(=> (= (The-Vector-Quantity ?M ?B) ?V) (Orthonormal-Basis ?B))

(=> (= (The-Vector-Quantity ?M ?B) ?V) (Row-Matrix ?M))

(=> (= (The-Vector-Quantity ?M ?B) ?V) (Matrix-Quantity ?M))

(=> (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))))))))

Notes:

• Example: (= (the-vector-quantity (matrix-of-columns (* 3 feet) (* 1 yard)) 2d-frame-n) (* (the-vector-quantity (matrix-of-columns 3 3) 2d-frame-n) feet))