The abstract of the Mizar article:

Cross Products and Tripple Vector Products in 3-dimensional Euclidian Space

by

Kanchun ,

Hiroshi Yamazaki, and

Yatsuka Nakamura

Received August 8, 2003

MML identifier: EUCLID_5

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, ARYTM, FINSEQ_1, FINSEQ_2, EUCLID, EUCLID_2, RLVECT_1,
      RVSUM_1, ARYTM_1, RELAT_1, FUNCT_1, MCART_1, EUCLID_5, VECTSP_1;
 notation SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, REAL_1, NAT_1, FUNCT_1,
      BINOP_1, VECTSP_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, SEQ_1, FINSEQOP,
      PRE_TOPC, RVSUM_1, EUCLID, STRUCT_0, EUCLID_2;
 constructors REAL_1, VECTSP_1, FINSEQOP, FINSEQ_4, SEQ_1, EUCLID_2, MEMBERED;
 clusters XREAL_0, RELSET_1, ARYTM_3, MEMBERED;
 requirements REAL, SUBSET, NUMERALS, ARITHM;


begin

reserve
  i, n, j for Nat,
  a,x,y,z for Real,
  x1,y1,z1,x2,y2,z2,x3,y3,z3 for Element of REAL,
  v for Element of n-tuples_on REAL,
  f1, f2 for FinSequence of REAL,
  p for Point of TOP-REAL 3;

theorem :: EUCLID_5:1
ex x, y, z st p= <* x, y, z *>;

definition let p;
  func p`1 -> Real means
:: EUCLID_5:def 1
     for f being FinSequence st p=f holds it = f.1;
  func p`2 -> Real means
:: EUCLID_5:def 2
     for f being FinSequence st p=f holds it = f.2;

  func p`3 -> Real means
:: EUCLID_5:def 3
     for f being FinSequence st p=f holds it = f.3;
end;

definition let x, y, z;
  func |[ x,y,z ]| -> Point of TOP-REAL 3 equals
:: EUCLID_5:def 4
<*x,y,z*>;
  end;

theorem :: EUCLID_5:2
|[ x,y,z ]|`1 = x & |[x,y,z]|`2 = y & |[x,y,z]|`3 = z;

theorem :: EUCLID_5:3
p = |[ p`1, p`2, p`3 ]|;

theorem :: EUCLID_5:4
0.REAL 3 = |[ 0,0,0 ]|;

reserve p1,p2,p3,p4 for Point of TOP-REAL 3,
        x1,x2,y1,y2,z1,z2,n for Real;

theorem :: EUCLID_5:5
p1 + p2 = |[ p1`1 + p2`1, p1`2 + p2`2, p1`3 + p2`3]|;

theorem :: EUCLID_5:6
|[x1,y1,z1]| + |[x2,y2,z2]| = |[x1+x2, y1+y2, z1+z2]|;

theorem :: EUCLID_5:7
x*p = |[ x*p`1, x*p`2, x*p`3]|;

theorem :: EUCLID_5:8
x * |[x1,y1,z1]| = |[ x*x1, x*y1, x*z1]|;

theorem :: EUCLID_5:9
(x*p)`1 = x * p`1 &
                 (x*p)`2 = x * p`2 &
                 (x*p)`3 = x * p`3;

theorem :: EUCLID_5:10
-p = |[ -p`1, -p`2, -p`3]|;

theorem :: EUCLID_5:11
-|[x1,y1,z1]| = |[ -x1, -y1, -z1]|;

theorem :: EUCLID_5:12
p1 - p2 = |[ p1`1 - p2`1, p1`2 - p2`2, p1`3 - p2`3]|;

theorem :: EUCLID_5:13
  |[x1, y1, z1]| - |[x2, y2, z2]| = |[ x1-x2, y1-y2, z1-z2]|;

definition let p1, p2;
  func p1 <X> p2 -> Point of TOP-REAL 3 equals
:: EUCLID_5:def 5
        |[ (p1`2 * p2`3) - (p1`3 * p2`2) ,
           (p1`3 * p2`1) - (p1`1 * p2`3) ,
           (p1`1 * p2`2) - (p1`2 * p2`1) ]|;
end;

theorem :: EUCLID_5:14
p = |[x, y, z]| implies
                p`1 = x & p`2 = y & p`3 = z;

theorem :: EUCLID_5:15
  |[x1, y1, z1]| <X> |[x2, y2, z2]|
              = |[ (y1 * z2) - (z1 * y2) ,
                   (z1 * x2) - (x1 * z2) ,
                   (x1 * y2) - (y1 * x2) ]|;

theorem :: EUCLID_5:16
(x*p1) <X> p2 =  x* (p1 <X> p2) &
                 (x*p1) <X> p2 =  p1 <X> (x*p2);

theorem :: EUCLID_5:17
p1<X>p2 = - p2<X>p1;

theorem :: EUCLID_5:18
(-p1) <X> p2 = p1 <X> (-p2);

theorem :: EUCLID_5:19
|[0, 0, 0]| <X> |[x, y, z]| = 0.REAL 3;

theorem :: EUCLID_5:20
|[x1, 0, 0]| <X> |[x2, 0, 0]| = 0.REAL 3;

theorem :: EUCLID_5:21
|[0, y1, 0]| <X> |[0, y2, 0]| = 0.REAL 3;

theorem :: EUCLID_5:22
|[0, 0, z1]| <X> |[0, 0, z2]| = 0.REAL 3;

theorem :: EUCLID_5:23
p1 <X> (p2+p3) = ( p1 <X> p2 ) + ( p1 <X> p3 );

theorem :: EUCLID_5:24
(p1+p2) <X> p3 = ( p1 <X> p3 ) + ( p2 <X> p3 );

theorem :: EUCLID_5:25
p1 <X> p1 = 0.REAL 3;

theorem :: EUCLID_5:26
(p1+p2) <X> (p3+p4) = p1<X>p3 + p1<X>p4 + p2<X>p3 + p2<X>p4;

::
:: Inner Product for Point of TOP-REAL 3
::

theorem :: EUCLID_5:27
  p = <* p`1, p`2, p`3 *>;

theorem :: EUCLID_5:28
  for f1, f2 be FinSequence of REAL st len f1 = 3 & len f2 = 3 holds
  mlt(f1, f2) = <* f1.1*f2.1, f1.2*f2.2, f1.3*f2.3 *>;

theorem :: EUCLID_5:29
  |(p1,p2)| = p1`1*p2`1 + p1`2*p2`2 + p1`3*p2`3;

theorem :: EUCLID_5:30
  |( |[ x1, x2, x3 ]|, |[ y1, y2, y3 ]| )| = x1*y1 + x2*y2 + x3*y3;

::
:: Scalar and Vector : Triple Products
::
definition let p1, p2, p3;
     func |{ p1,p2,p3 }| -> real number equals
:: EUCLID_5:def 6
      |(p1, p2<X>p3)|;
end;

theorem :: EUCLID_5:31
|{ p1, p1, p2 }| = 0 &
        |{ p2, p1, p2 }| = 0;

theorem :: EUCLID_5:32
  p1 <X> ( p2<X>p3 ) = ( |(p1,p3)| * p2 ) - ( |(p1,p2)| * p3 );

theorem :: EUCLID_5:33
  |{ p1, p2, p3 }| = |{ p2, p3, p1 }|;

theorem :: EUCLID_5:34
  |{ p1, p2, p3 }| = |{ p3, p1, p2 }|;

theorem :: EUCLID_5:35
  |{ p1, p2, p3 }| = |( p1<X>p2, p3 )|;