Function BASIS.VEC

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

Slots on this function:

Documentation:

Function to select the individual unit vectors of a basis.

Instance-Of: Function

Arity: 3

Axioms:

(Nth-Domain Basis.Vec 3 Unit-Vec)

(Nth-Domain Basis.Vec 2 Positive-Integer)

(Nth-Domain Basis.Vec 1 Orthonormal-Basis)

Other Related Axioms:

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

(Forall (?N)
        (=> (And (Positive-Integer ?N) (=< ?N (Basis.Dimension ?B)))
            (Defined (Basis.Vec ?B ?N))))

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

(=> (= (Basis.Vec ?Basis ?N) ?Uv) (=< ?N (Basis.Dimension ?Basis)))

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

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

(=> (= (The-Dyad ?M ?B) ?T)
    (= ?T
       (Summation (Lambda (?I)
                          (Summation (Lambda (?J)
                                             (* (Basis.Vec ?B ?I)
                                                (* (Value ?M ?I ?J)
                                                   (Basis.Vec ?B ?J))))
                                     1
                                     (Spatial.Dimension ?T)))
                  1
                  (Spatial.Dimension ?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))))))))