:: Cross Products and Tripple Vector Products in 3-dimensional Euclidian Space :: by Kanchun, Hiroshi Yamazaki and Yatsuka Nakamura :: :: Received August 8, 2003 :: Copyright (c) 2003-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, REAL_1, SUBSET_1, PRE_TOPC, EUCLID, FINSEQ_1, STRUCT_0, FINSEQ_2, MCART_1, FUNCT_1, SUPINF_2, CARD_1, ARYTM_3, RELAT_1, ARYTM_1, RVSUM_1, BINOP_2, CARD_3, EUCLID_5, INCSP_1; notations SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, FUNCT_1, BINOP_1, BINOP_2, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSEQOP, PRE_TOPC, RVSUM_1, RLVECT_1, EUCLID, STRUCT_0, REAL_1, INCSP_1, ANPROJ_2; constructors REAL_1, BINOP_2, FINSEQOP, FINSEQ_4, MONOID_0, EUCLID, BINOP_1, INCSP_1, ANPROJ_2; registrations RELSET_1, NUMBERS, XREAL_0, MEMBERED, MONOID_0, EUCLID, VALUED_0, FINSEQ_2, RVSUM_1, FINSEQ_1; requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE; begin reserve x,y,z for Real, x3,y3 for 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 equals :: EUCLID_5:def 1 p.1; func p`2 -> Real equals :: EUCLID_5:def 2 p.2; func p`3 -> Real equals :: EUCLID_5:def 3 p.3; end; notation let x, y, z be Real; synonym |[ x,y,z ]| for <*x,y,z*>; end; definition let x, y, z be Real; redefine func |[ x,y,z ]| -> Point of TOP-REAL 3; 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.TOP-REAL 3 = |[ 0,0,0 ]|; reserve p1,p2,p3,p4 for Point of TOP-REAL 3, x1,x2,y1,y2,z1,z2 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 p2 -> Point of TOP-REAL 3 equals :: EUCLID_5:def 4 |[ (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]| |[x2, y2, z2]| = |[ (y1 * z2) - (z1 * y2), (z1 * x2) - (x1 * z2), (x1 * y2) - (y1 * x2) ]|; theorem :: EUCLID_5:16 (x*p1) p2 = x* (p1 p2) & (x*p1) p2 = p1 (x*p2); theorem :: EUCLID_5:17 p1p2 = - p2p1; theorem :: EUCLID_5:18 (-p1) p2 = p1 (-p2); theorem :: EUCLID_5:19 |[0, 0, 0]| |[x, y, z]| = 0.TOP-REAL 3; theorem :: EUCLID_5:20 |[x1, 0, 0]| |[x2, 0, 0]| = 0.TOP-REAL 3; theorem :: EUCLID_5:21 |[0, y1, 0]| |[0, y2, 0]| = 0.TOP-REAL 3; theorem :: EUCLID_5:22 |[0, 0, z1]| |[0, 0, z2]| = 0.TOP-REAL 3; theorem :: EUCLID_5:23 p1 (p2+p3) = ( p1 p2 ) + ( p1 p3 ); theorem :: EUCLID_5:24 (p1+p2) p3 = ( p1 p3 ) + ( p2 p3 ); theorem :: EUCLID_5:25 p1 p1 = 0.TOP-REAL 3; theorem :: EUCLID_5:26 (p1+p2) (p3+p4) = p1p3 + p1p4 + p2p3 + p2p4; :: :: 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 equals :: EUCLID_5:def 5 |(p1, p2p3)|; end; theorem :: EUCLID_5:31 |{ p1, p1, p2 }| = 0 & |{ p2, p1, p2 }| = 0; theorem :: EUCLID_5:32 p1 ( p2p3 ) = ( |(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 }| = |( p1p2, p3 )|; registration cluster TOP-REAL 3 -> up-3-dimensional; end;