Function CROSS

• Defined in theory: 3d-tensor-quantities
• Source code: 3D-tensor-quantities.lisp

Slots on this function:

Documentation:

Vector or cross product of two three dimensional vectors. If we know the components of two vectors with respect to a common basis, we can determine the components of the cross product in that basis.

Arity: 3

Axioms:

(Nth-Domain Cross 3 3d-Vector-Quantity)

(Nth-Domain Cross 2 3d-Vector-Quantity)

(Nth-Domain Cross 1 3d-Vector-Quantity)

(<=> (Cross ?V1 ?V2 ?V)
     (And (3d-Vector-Quantity ?V1)
          (3d-Vector-Quantity ?V2)
          (3d-Vector-Quantity ?V)
          (= (Quantity.Dimension ?V)
             (* (Quantity.Dimension ?V1) (Quantity.Dimension ?V2)))
          (= (Dot ?V1 ?V)
             (The-Zero-Scalar-For-Dimension (* (Quantity.Dimension ?V1)
                                               (Quantity.Dimension ?V))))
          (= (Dot ?V2 ?V)
             (The-Zero-Scalar-For-Dimension (* (Quantity.Dimension ?V2)
                                               (Quantity.Dimension ?V))))
          (= (Vector-Component ?V 1 ?B)
             (- (* (Vector-Component ?V1 2 ?B)
                   (Vector-Component ?V2 3 ?B))
                (* (Vector-Component ?V2 2 ?B)
                   (Vector-Component ?V1 3 ?B))))
          (= (Vector-Component ?V 2 ?B)
             (- (* (Vector-Component ?V2 1 ?B)
                   (Vector-Component ?V1 3 ?B))
                (* (Vector-Component ?V1 1 ?B)
                   (Vector-Component ?V2 3 ?B))))
          (= (Vector-Component ?V 3 ?B)
             (- (* (Vector-Component ?V1 1 ?B)
                   (Vector-Component ?V2 2 ?B))
                (* (Vector-Component ?V2 1 ?B)
                   (Vector-Component ?V1 2 ?B))))))