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.

Instance-Of: Function

Arity: 3

Equivalence Axioms:

(<=> (Cross ?V1 ?V2)
     (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))))))

Axioms:

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

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

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

Other Related Axioms:

(=> (= (Cross ?V1 ?V2) ?V)
    (= (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)))))

(=> (= (Cross ?V1 ?V2) ?V)
    (= (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)))))

(=> (= (Cross ?V1 ?V2) ?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)))))

(=> (= (Cross ?V1 ?V2) ?V)
    (= (Dot ?V2 ?V)
       (The-Zero-Scalar-For-Dimension (* (Quantity.Dimension ?V2)
                                         (Quantity.Dimension ?V)))))

(=> (= (Cross ?V1 ?V2) ?V)
    (= (Dot ?V1 ?V)
       (The-Zero-Scalar-For-Dimension (* (Quantity.Dimension ?V1)
                                         (Quantity.Dimension ?V)))))

(=> (= (Cross ?V1 ?V2) ?V)
    (= (Quantity.Dimension ?V)
       (* (Quantity.Dimension ?V1) (Quantity.Dimension ?V2))))

(=> (= (Cross ?V1 ?V2) ?V) (3d-Vector-Quantity ?V))

(=> (= (Cross ?V1 ?V2) ?V) (3d-Vector-Quantity ?V2))

(=> (= (Cross ?V1 ?V2) ?V) (3d-Vector-Quantity ?V1))