Function DYAD-COMPONENT


Slots on this function:

Documentation:
Function to generate the i,j th scalar component for a dyad in a particular basis. The i,j scalar component of dyad T is equal to bi*T*bj (basis vector i dot T dot basis vector j.
Instance-Of: Function
Arity: 5

Equivalence Axioms:

(<=> (Dyad-Component ?T ?I ?J ?Basis)
     (And (Dyad ?T)
          (Positive-Integer ?I)
          (Positive-Integer ?J)
          (Orthonormal-Basis ?Basis)
          (Scalar-Quantity ?S)
          (= (Quantity.Dimension ?S) (Quantity.Dimension ?T))
          (= (Spatial.Dimension ?T) (Basis.Dimension ?B))
          (=< ?I (Spatial.Dimension ?T))
          (=< ?J (Spatial.Dimension ?T))
          (= ?S
             (Dot (Basis.Vec ?Basis ?I) (Dot ?T (Basis.Vec ?B ?J))))))


Axioms:

(Nth-Domain Dyad-Component 5 Scalar-Quantity)

(Nth-Domain Dyad-Component 4 Orthonormal-Basis)

(Nth-Domain Dyad-Component 3 Positive-Integer)

(Nth-Domain Dyad-Component 2 Positive-Integer)

(Nth-Domain Dyad-Component 1 Dyad)


Other Related Axioms:

(Forall (?B ?I ?J)
        (=> (And (Orthonormal-Basis ?B)
                 (= (Basis.Dimension ?B) (Spatial.Dimension ?D))
                 (Positive-Integer ?I)
                 (=< ?I (Spatial.Dimension ?D))
                 (Positive-Integer ?J)
                 (=< ?J (Spatial.Dimension ?D)))
            (And (Defined (Dyad-Component ?D ?I ?J ?B))
                 (= (Quantity.Dimension (Dyad-Component ?D ?I ?J ?B))
                    (Quantity.Dimension ?D)))))

(<=> (Dyad ?D)
     (And (Constant-Quantity ?D)
          (Tensor-Quantity ?D)
          (= (Tensor-Order ?D) 2)
          (Forall (?B ?I ?J)
                  (=> (And (Orthonormal-Basis ?B)
                           (= (Basis.Dimension ?B)
                              (Spatial.Dimension ?D))
                           (Positive-Integer ?I)
                           (=< ?I (Spatial.Dimension ?D))
                           (Positive-Integer ?J)
                           (=< ?J (Spatial.Dimension ?D)))
                      (And (Defined (Dyad-Component ?D ?I ?J ?B))
                           (= (Quantity.Dimension (Dyad-Component ?D
                                                                  ?I
                                                                  ?J
                                                                  ?B))
                              (Quantity.Dimension ?D)))))
          (Forall (?U)
                  (=> (And (Unit-Of-Measure ?U)
                           (= (Quantity.Dimension ?U)
                              (Quantity.Dimension ?D)))
                      (Numeric-Tensor (Magnitude ?D ?U))))))

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

(=> (= (Dyad-Component ?T ?I ?J ?Basis) ?S)
    (= ?S (Dot (Basis.Vec ?Basis ?I) (Dot ?T (Basis.Vec ?B ?J)))))

(=> (= (Dyad-Component ?T ?I ?J ?Basis) ?S)
    (=< ?J (Spatial.Dimension ?T)))

(=> (= (Dyad-Component ?T ?I ?J ?Basis) ?S)
    (=< ?I (Spatial.Dimension ?T)))

(=> (= (Dyad-Component ?T ?I ?J ?Basis) ?S)
    (= (Spatial.Dimension ?T) (Basis.Dimension ?B)))

(=> (= (Dyad-Component ?T ?I ?J ?Basis) ?S)
    (= (Quantity.Dimension ?S) (Quantity.Dimension ?T)))

(=> (= (Dyad-Component ?T ?I ?J ?Basis) ?S) (Scalar-Quantity ?S))

(=> (= (Dyad-Component ?T ?I ?J ?Basis) ?S)
    (Orthonormal-Basis ?Basis))

(=> (= (Dyad-Component ?T ?I ?J ?Basis) ?S) (Positive-Integer ?J))

(=> (= (Dyad-Component ?T ?I ?J ?Basis) ?S) (Positive-Integer ?I))

(=> (= (Dyad-Component ?T ?I ?J ?Basis) ?S) (Dyad ?T))

(=> (And (Dyad ?X) (Dyad ?Y))
    (=> (+ ?X ?Y ?Z)
        (And (Dyad ?Z)
             (Forall (?B ?I ?J)
                     (=> (And (Orthonormal-Basis ?B)
                              (= (Spatial.Dimension ?X)
                                 (Basis.Dimension ?B))
                              (Positive-Integer ?I)
                              (Positive-Integer ?J)
                              (=< ?I (Spatial.Dimension ?X))
                              (=< ?J (Spatial.Dimension ?X)))
                         (= (Dyad-Component ?Z ?I ?J ?B)
                            (+ (Dyad-Component ?X ?I ?J ?B)
                               (Dyad-Component ?Y ?I ?J ?B))))))))

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