:: 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-2026 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;
definitions ANPROJ_2;
equalities ALGSTR_0;
theorems EUCLID, RVSUM_1, FINSEQ_2, FINSEQ_1, BINOP_2, XREAL_0, VALUED_1,
CARD_1, RLVECT_1;
begin
reserve x,y,z for Real,
x3,y3 for Real,
p for Point of TOP-REAL 3;
theorem Th1:
ex x, y, z st p = <* x, y, z *>
proof
the carrier of TOP-REAL 3 = REAL 3 by EUCLID:22;
then p is Element of 3-tuples_on REAL by EUCLID:def 1;
then p in 3-tuples_on REAL;
then reconsider p as Tuple of 3,REAL by FINSEQ_2:131;
ex x,y,z being Element of REAL st p=<*x,y,z*> by FINSEQ_2:103;
hence thesis;
end;
definition
let p;
func p`1 -> Real equals
p.1;
coherence;
func p`2 -> Real equals
p.2;
coherence;
func p`3 -> Real equals
p.3;
coherence;
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; :: redefines |[ (EUCLID_5, synonym) → <* (FINSEQ_1, definition)
coherence
proof
reconsider x,y,z as Element of REAL by XREAL_0:def 1;
<*x,y,z*> is Element of 3-tuples_on REAL by FINSEQ_2:104;
then <*x,y,z*> is Element of REAL 3 by EUCLID:def 1;
hence thesis by EUCLID:22;
end;
end;
theorem Th2:
|[ x,y,z ]|`1 = x & |[x,y,z]|`2 = y & |[x,y,z]|`3 = z;
theorem Th3:
p = |[ p`1, p`2, p`3 ]|
proof
ex x,y,z st p = <*x,y,z*> by Th1;
hence thesis;
end;
theorem Th4:
0.TOP-REAL 3 = |[ 0,0,0 ]|
proof
0.TOP-REAL 3 = 0*3 by EUCLID:70
.= 3 |-> 0 by EUCLID:def 4
.= <* 0, 0, 0 *> by FINSEQ_2:62;
hence thesis;
end;
reserve p1,p2,p3,p4 for Point of TOP-REAL 3,
x1,x2,y1,y2,z1,z2 for Real;
theorem Th5:
p1 + p2 = |[ p1`1 + p2`1, p1`2 + p2`2, p1`3 + p2`3]|
proof
reconsider p19=p1, p29=p2 as Element of REAL 3 by EUCLID:22;
len(p19+p29) = 3 by CARD_1:def 7;
then
A1: dom(p19+p29) = Seg 3 by FINSEQ_1:def 3;
then 2 in dom(p19+p29) by FINSEQ_1:1;
then (p19+p29).2 = p19.2 + p29.2 by VALUED_1:def 1;
then
A2: (p1+p2)`2 = p1`2 + p2`2;
3 in dom(p19+p29) by A1,FINSEQ_1:1;
then (p19+p29).3 = p19.3 + p29.3 by VALUED_1:def 1;
then
A3: (p1+p2)`3 = p1`3 + p2`3;
1 in dom(p19+p29) by A1,FINSEQ_1:1;
then (p19+p29).1 = p19.1 + p29.1 by VALUED_1:def 1;
then (p1+p2)`1 = p1`1 + p2`1;
hence thesis by A2,A3,Th3;
end;
theorem Th6:
|[x1,y1,z1]| + |[x2,y2,z2]| = |[x1+x2, y1+y2, z1+z2]|
proof
A1: |[x1, y1, z1]|`3 = z1 & |[x2, y2, z2]|`1 = x2;
A2: |[x2, y2, z2]|`2 = y2 & |[x2, y2, z2]|`3 = z2;
|[x1, y1, z1]|`1 = x1 & |[x1, y1, z1]|`2 = y1;
hence thesis by A1,A2,Th5;
end;
theorem Th7:
x*p = |[ x*p`1, x*p`2, x*p`3]|
proof
reconsider q = p as Element of REAL 3 by EUCLID:22;
(x*q).2 = x*(q.2) by RVSUM_1:44; then
A1: (x*p)`2 = x*(p`2);
(x*q).3 = x*(q.3) by RVSUM_1:44; then
A2: (x*p)`3 = x*(p`3);
(x*q).1 = x*(q.1) by RVSUM_1:44;
then (x*p)`1 = x*(p`1);
hence thesis by A1,A2,Th3;
end;
theorem Th8:
x * |[x1,y1,z1]| = |[ x*x1, x*y1, x*z1]|
proof
A1: |[x1,y1,z1]|`3 = z1;
|[x1,y1,z1]|`1 = x1 & |[x1,y1,z1]|`2 = y1;
hence thesis by A1,Th7;
end;
theorem
(x*p)`1 = x * p`1 & (x*p)`2 = x * p`2 & (x*p)`3 = x * p`3
proof
A1: (x*p)`3 = |[ x*p`1 ,x*p`2 ,x*p`3]|`3 by Th7;
(x*p)`1 = |[ x*p`1 ,x*p`2 ,x*p`3]|`1 & (x*p)`2 = |[ x*p`1 ,x*p`2 ,x*p`3
]|`2 by Th7;
hence thesis by A1;
end;
theorem Th10:
-p = |[ -p`1, -p`2, -p`3]|
proof
thus -p = (-1)*p by RLVECT_1:16
.= |[ (-1)*p`1, (-1)*p`2, (-1)*p`3]| by Th7
.= |[ -p`1, -p`2, -p`3]|;
end;
theorem
-|[x1,y1,z1]| = |[ -x1, -y1, -z1]|
proof
A1: |[x1,y1,z1]|`3 = z1;
|[x1,y1,z1]|`1 = x1 & |[x1,y1,z1]|`2 = y1;
hence thesis by A1,Th10;
end;
theorem Th12:
p1 - p2 = |[ p1`1 - p2`1, p1`2 - p2`2, p1`3 - p2`3]|
proof
A1: -p2 = |[ -p2`1, -p2`2, -p2`3]| by Th10;
then
A2: (-p2)`3 = -p2`3;
(-p2)`1 = -p2`1 & (-p2)`2 = -p2`2 by A1;
hence p1 - p2 = |[ p1`1 + -p2`1, p1`2 + -p2`2, p1`3 + -p2`3]| by A2,Th5
.= |[ p1`1 - p2`1, p1`2 - p2`2, p1`3 - p2`3]|;
end;
theorem Th13:
|[x1, y1, z1]| - |[x2, y2, z2]| = |[ x1-x2, y1-y2, z1-z2]|
proof
A1: |[x1, y1, z1]|`3 = z1 & |[x2, y2, z2]|`1 = x2;
A2: |[x2, y2, z2]|`2 = y2 & |[x2, y2, z2]|`3 = z2;
|[x1, y1, z1]|`1 = x1 & |[x1, y1, z1]|`2 = y1;
hence thesis by A1,A2,Th12;
end;
definition
let p1, p2;
func p1 <X> p2 -> Point of TOP-REAL 3 equals
|[ (p1`2 * p2`3) - (p1`3 * p2`2) ,
(p1`3 * p2`1) - (p1`1 * p2`3) ,
(p1`1 * p2`2) - (p1`2 * p2`1) ]|;
correctness;
end;
theorem
p = |[x, y, z]| implies p`1 = x & p`2 = y & p`3 = z;
theorem
|[x1, y1, z1]| <X> |[x2, y2, z2]| =
|[ (y1 * z2) - (z1 * y2), (z1 * x2) - (x1 * z2), (x1 * y2) - (y1 * x2) ]|;
theorem
(x*p1) <X> p2 = x* (p1 <X> p2) & (x*p1) <X> p2 = p1 <X> (x*p2)
proof
A1: (x*p1) <X> p2 = |[ x*p1`1 ,x*p1`2 ,x*p1`3]| <X> p2 by Th7
.= |[ x*p1`1 ,x*p1`2 ,x*p1`3]| <X> |[ p2`1,p2`2,p2`3]|
.= |[ (x*p1`2 * p2`3) - (x*p1`3 * p2`2) , (x*p1`3 * p2`1) - (x*p1`1 * p2
`3) , (x*p1`1 * p2`2) - (x*p1`2 * p2`1) ]|;
then
A2: (x*p1) <X> p2 = |[ x * ( (p1`2 * p2`3) - (p1`3 * p2`2) ), x * ( (p1`3 *
p2`1) - (p1`1 * p2`3) ), x * ( (p1`1 * p2`2) - (p1`2 * p2`1) ) ]|
.= x * (p1 <X> p2) by Th8;
(x*p1) <X> p2 = |[ p1`2 * (x * p2`3) - p1`3 * (x * p2`2), p1`3 * (x * p2
`1) - p1`1 * (x * p2`3), p1`1 * (x * p2`2) - p1`2 * (x * p2`1) ]| by A1
.= |[ p1`1, p1`2, p1`3]| <X> |[ x*p2`1 ,x*p2`2 ,x*p2`3]|
.= p1 <X> |[ x*p2`1 ,x*p2`2 ,x*p2`3]|
.= p1 <X> (x*p2) by Th7;
hence thesis by A2;
end;
theorem Th17:
p1<X>p2 = - p2<X>p1
proof
- p2 <X> p1 = (-1)*(p2 <X> p1) by RLVECT_1:16
.= |[ (-1) * ( (p2`2 * p1`3) - (p2`3 * p1`2) ), (-1) * ( (p2`3 * p1`1) -
(p2`1 * p1`3) ), (-1) * ( (p2`1 * p1`2) - (p2`2 * p1`1) ) ]| by Th8
.= p1 <X> p2;
hence thesis;
end;
theorem
(-p1) <X> p2 = p1 <X> (-p2)
proof
(-p1) <X> p2 = |[ -p1`1, -p1`2, -p1`3 ]| <X> p2 by Th10
.= |[ -p1`1, -p1`2, -p1`3 ]| <X> |[ p2`1, p2`2, p2`3 ]|
.= |[ ((-p1`2) * p2`3) - ((-p1`3) * p2`2) , ((-p1`3) * p2`1) - ((-p1`1)
* p2`3) , ((-p1`1) * p2`2) - ((-p1`2) * p2`1) ]|
.= |[ (p1`2 * (-p2`3)) - (p1`3 * (-p2`2)) , (p1`3 * (-p2`1)) - (p1`1 * (
-p2`3)) , (p1`1 * (-p2`2)) - (p1`2 * (-p2`1)) ]|
.= |[ p1`1, p1`2, p1`3 ]| <X> |[ -p2`1, -p2`2, -p2`3 ]|
.= |[ p1`1, p1`2, p1`3 ]| <X> -p2 by Th10;
hence thesis;
end;
theorem
|[0, 0, 0]| <X> |[x, y, z]| = 0.TOP-REAL 3
proof
|[0, 0, 0]| <X> |[x, y, z]|
= |[ (0 * z) - (0 * y) , (0 * x) - (0 * z) , (0 * y) - (0 * x) ]|
.= |[ 0 * (z - y) , 0 * (x - z) , 0 * (y - x) ]|
.= 0 * |[ (z - y), (x - z), (y - x) ]| by Th8;
hence thesis by RLVECT_1:10;
end;
theorem
|[x1, 0, 0]| <X> |[x2, 0, 0]| = 0.TOP-REAL 3
proof
|[x1, 0, 0]| <X> |[x2, 0, 0]| = |[ (0 * 0) - (0 * 0) , (0 * x2) - (x1 *
0) , (x1 * 0) - (0 * x2) ]|
.= |[ 0 * (0 - 0), 0 * (x2 - x1), 0 * (x1 - x2) ]|
.= 0 * |[ (0 - 0), (x2 - x1), (x1 - x2) ]| by Th8
.= 0.TOP-REAL 3 by RLVECT_1:10;
hence thesis;
end;
theorem
|[0, y1, 0]| <X> |[0, y2, 0]| = 0.TOP-REAL 3
proof
|[0, y1, 0]| <X> |[0, y2, 0]| = |[ (y1 * 0) - (0 * y2), (0 * 0) - (0 * 0
), (0 * y2) - (y1 * 0) ]|
.= |[ 0 * (y1 - y2), 0 * (0 - 0), 0 * (y2 - y1) ]|
.= 0 * |[ (y1 - y2), (0 - 0), (y2 - y1) ]| by Th8
.= 0.TOP-REAL 3 by RLVECT_1:10;
hence thesis;
end;
theorem
|[0, 0, z1]| <X> |[0, 0, z2]| = 0.TOP-REAL 3
proof
|[0, 0, z1]| <X> |[0, 0, z2]| = |[ (0 * z2) - (z1 * 0), (z1 * 0) - (0 *
z2), (0 * 0) - (0 * 0) ]|
.= |[ 0 * (z2 - z1), 0 * (z1 - z2), 0 * (0 * 0) ]|
.= 0 * |[ (z2 - z1), (z1 - z2), (0 - 0) ]| by Th8
.= 0.TOP-REAL 3 by RLVECT_1:10;
hence thesis;
end;
theorem Th23:
p1 <X> (p2+p3) = ( p1 <X> p2 ) + ( p1 <X> p3 )
proof
A1: ( p1 <X> p2 ) + ( p1 <X> p3 ) = |[ (p1`2 * p2`3 - p1`3 * p2`2) + (p1`2 *
p3`3 - p1`3 * p3`2), (p1`3 * p2`1 - p1`1 * p2`3) + (p1`3 * p3`1 - p1`1 * p3`3),
(p1`1 * p2`2 - p1`2 * p2`1) + (p1`1 * p3`2 - p1`2 * p3`1) ]| by Th6
.= |[ p1`2 * p2`3 - p1`3 * p2`2 + p1`2 * p3`3 - p1`3 * p3`2, p1`3 * p2`1
- p1`1 * p2`3 + p1`3 * p3`1 - p1`1 * p3`3, p1`1 * p2`2 - p1`2 * p2`1 + p1`1 *
p3`2 - p1`2 * p3`1 ]|;
A2: p2+p3 = |[ p2`1 + p3`1, p2`2 + p3`2, p2`3 + p3`3]| by Th5;
then
A3: (p2+p3)`3 = p2`3 + p3`3;
(p2+p3)`1 = p2`1 + p3`1 & (p2+p3)`2 = p2`2 + p3`2 by A2;
hence thesis by A3,A1;
end;
theorem Th24:
(p1+p2) <X> p3 = ( p1 <X> p3 ) + ( p2 <X> p3 )
proof
(p1+p2) <X> p3 = - ( p3 <X> (p1+p2) ) by Th17
.= - ( ( p3 <X> p1 ) + ( p3 <X> p2 ) ) by Th23
.= - ( ( p3 <X> p1 ) - ( p2 <X> p3 ) ) by Th17
.= - ( p3 <X> p1 ) + ( p2 <X> p3 ) by RLVECT_1:33;
hence thesis by Th17;
end;
theorem
p1 <X> p1 = 0.TOP-REAL 3 by Th4;
theorem
(p1+p2) <X> (p3+p4) = p1<X>p3 + p1<X>p4 + p2<X>p3 + p2<X>p4
proof
(p1+p2) <X> (p3+p4) = ( p1 <X> (p3+p4) ) + ( p2 <X> (p3+p4) ) by Th24
.= ( p1 <X> p3 + p1 <X> p4 ) + ( p2 <X> (p3+p4) ) by Th23
.= ( p1 <X> p3 + p1 <X> p4 ) + (p2 <X> p3 + p2 <X> p4 ) by Th23;
hence thesis by RLVECT_1:def 3;
end;
::
:: Inner Product for Point of TOP-REAL 3
::
theorem Th27:
p = <* p`1, p`2, p`3 *>
proof
ex x, y, z being Real st p = <* x, y, z *> by Th1;
hence thesis;
end;
theorem Th28:
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 *>
proof
let f1, f2 be FinSequence of REAL such that
A1: len f1 = 3 and
A2: len f2 = 3;
A3: f2 = <* f2.1, f2.2, f2.3 *> by A2,FINSEQ_1:45;
reconsider f11=f1.1, f12=f1.2, f13=f1.3, f21=f2.1, f22=f2.2, f23=f2.3
as Element of REAL by XREAL_0:def 1;
mlt(f1, f2) = multreal.:(f1, f2) by RVSUM_1:def 9
.= multreal.:(<* f11, f12, f13 *>, <* f21, f22, f23 *>)
by A1,A3,FINSEQ_1:45
.= <* multreal.(f1.1, f2.1), multreal.(f1.2, f2.2), multreal.(f1.3, f2.3
)*> by FINSEQ_2:76
.= <* f1.1*f2.1, multreal.(f1.2, f2.2), multreal.(f1.3, f2.3)*> by
BINOP_2:def 11
.= <* f1.1*f2.1, f1.2*f2.2, multreal.(f1.3, f2.3)*> by BINOP_2:def 11;
hence thesis by BINOP_2:def 11;
end;
theorem Th29:
|(p1,p2)| = p1`1*p2`1 + p1`2*p2`2 + p1`3*p2`3
proof
reconsider f1=p1, f2=p2 as FinSequence of REAL by EUCLID:24;
A1: len f1 = len <* p1`1, p1`2, p1`3 *> by Th27
.= 3 by FINSEQ_1:45;
A2: len f2 = len <* p2`1, p2`2, p2`3 *> by Th27
.= 3 by FINSEQ_1:45;
|(p1,p2)| = Sum mlt(f1, f2) by RVSUM_1:def 16
.= Sum <* f1.1*f2.1, f1.2*f2.2, f1.3*f2.3 *> by A1,A2,Th28
.= p1`1*p2`1 + p1`2*p2`2 + p1`3*f2.3 by RVSUM_1:78;
hence thesis;
end;
theorem Th30:
|( |[ x1, x2, x3 ]|, |[ y1, y2, y3 ]| )| = x1*y1 + x2*y2 + x3*y3
proof
consider p1 such that
A1: p1 = |[x1, x2, x3]|;
A2: p1`3 = x3 by A1;
consider p2 such that
A3: p2 = |[y1, y2, y3]|;
A4: p2`3 = y3 by A3;
A5: p2`1 = y1 & p2`2 = y2 by A3;
p1`1 = x1 & p1`2 = x2 by A1;
hence thesis by A1,A2,A3,A5,A4,Th29;
end;
::
:: Scalar and Vector : Triple Products
::
definition
let p1, p2, p3;
func |{ p1,p2,p3 }| -> Real equals
|(p1, p2<X>p3)|;
coherence;
end;
theorem
|{ p1, p1, p2 }| = 0 & |{ p2, p1, p2 }| = 0
proof
A1: |{ p2, p1, p2 }| = p2`1*(p1<X>p2)`1 + p2`2*(p1<X>p2)`2 + p2`3*(p1<X>p2)
`3 by Th29
.= p2`1*((p1`2 * p2`3) - (p1`3 * p2`2)) + p2`2*(p1<X>p2)`2 + p2`3*(p1<X>
p2)`3
.= p2`1*( (p1`2 * p2`3) - (p1`3 * p2`2) ) + p2`2*( (p1`3 * p2`1) - (p1`1
* p2`3) ) + p2`3*(p1<X>p2)`3
.= ( p2`1*(p1`2 * p2`3) - p2`1*(p1`3 * p2`2) ) + p2`2*( (p1`3 * p2`1) -
(p1`1 * p2`3) ) + p2`3*( (p1`1 * p2`2) - (p1`2 * p2`1) )
.= 0 - p2`2*(p1`1 * p2`3) + p2`2*(p1`1 * p2`3);
|{ p1, p1, p2 }| = p1`1*(p1<X>p2)`1 + p1`2*(p1<X>p2)`2 + p1`3*(p1<X>p2)
`3 by Th29
.= p1`1*((p1`2 * p2`3) - (p1`3 * p2`2)) + p1`2*(p1<X>p2)`2 + p1`3*(p1<X>
p2)`3
.= p1`1*( (p1`2 * p2`3) - (p1`3 * p2`2) ) + p1`2*( (p1`3 * p2`1) - (p1`1
* p2`3) ) + p1`3*(p1<X>p2)`3
.= ( p1`1*(p1`2 * p2`3) - p1`1*(p1`3 * p2`2) ) + p1`2*( (p1`3 * p2`1) -
(p1`1 * p2`3) ) + p1`3*( (p1`1 * p2`2) - (p1`2 * p2`1) )
.= 0;
hence thesis by A1;
end;
theorem
p1 <X> ( p2<X>p3 ) = |(p1,p3)| * p2 - |(p1,p2)| * p3
proof
A1: (p1`2*((p2`1 * p3`2) - (p2`2 * p3`1))) - (p1`3*((p2`3 * p3`1) - (p2`1 *
p3`3) )) = (p1`2*p3`2 + p1`3*p3`3 + p1`1*p3`1)*p2`1 - (p1`2*p2`2 + p1`3*p2`3 +
p1`1* p2`1)*p3`1 & (p1`3*((p2`2 * p3`3) - (p2`3 * p3`2))) - (p1`1*((p2`1 * p3`2
) - ( p2`2 * p3`1))) = (p1`3*p3`3 + p1`1*p3`1 + p1`2*p3`2)*p2`2 - (p1`3*p2`3 +
p1`1* p2`1 + p1`2*p2`2)*p3`2;
A2: (p1`1*((p2`3 * p3`1) - (p2`1 * p3`3))) - (p1`2*((p2`2 * p3`3) - (p2`3 *
p3`2))) = (p1`1*p3`1 + p1`2*p3`2 + p1`3*p3`3)*p2`3 - (p1`1*p2`1 + p1`2*p2`2 +
p1`3*p2`3)*p3`3;
p1 <X> (p2 <X> p3) = |[ (p1`1*p3`1 + p1`2*p3`2 + p1`3*p3`3)*p2`1, (p1`1*
p3`1 + p1`2*p3`2 + p1`3*p3`3)*p2`2, (p1`1*p3`1 + p1`2*p3`2 + p1`3*p3`3)*p2`3 ]|
- |[ (p1`1*p2`1 + p1`2*p2`2 + p1`3*p2`3)*p3`1, (p1`1*p2`1 + p1`2*p2`2 + p1`3*p2
`3)*p3`2, (p1`1*p2`1 + p1`2*p2`2 + p1`3*p2`3)*p3`3 ]| by A1,A2,Th13
.= (p1`1*p3`1 + p1`2*p3`2 + p1`3*p3`3) * |[p2`1, p2`2, p2`3 ]| - |[ (p1
`1*p2`1 + p1`2*p2`2 + p1`3*p2`3)*p3`1, (p1`1*p2`1 + p1`2*p2`2 + p1`3*p2`3)*p3`2
, (p1`1*p2`1 + p1`2*p2`2 + p1`3*p2`3)*p3`3 ]| by Th8
.= (p1`1*p3`1 + p1`2*p3`2 + p1`3*p3`3) * |[ p2`1, p2`2, p2`3 ]| - (p1`1*
p2`1 + p1`2*p2`2 + p1`3*p2`3) * |[ p3`1, p3`2, p3`3 ]| by Th8
.= |(p1, p3)| * |[ p2`1, p2`2, p2`3 ]| - (p1`1*p2`1 + p1`2*p2`2 + p1`3*
p2`3) * |[ p3`1, p3`2, p3`3 ]| by Th29
.= |(p1, p3)| * |[ p2`1, p2`2, p2`3 ]| - |(p1, p2 )| * |[ p3`1, p3`2, p3
`3 ]| by Th29
.= |(p1, p3)| * p2 - |(p1, p2 )| * |[ p3`1, p3`2, p3`3 ]| by Th3;
hence thesis by Th3;
end;
theorem Th33:
|{ p1, p2, p3 }| = |{ p2, p3, p1 }|
proof
|{ p1, p2, p3 }| = |(|[ p1`1, p1`2, p1`3 ]|, |[ (p2`2*p3`3) - (p2`3*p3`2
), (p2`3*p3`1) - (p2`1*p3`3), (p2`1*p3`2) - (p2`2*p3`1) ]|)| by Th3
.= p1`1*((p2`2*p3`3) - (p2`3*p3`2)) + p1`2*((p2`3*p3`1) - (p2`1*p3`3)) +
p1`3*((p2`1*p3`2) - (p2`2*p3`1)) by Th30
.= p2`1*(p3`2*p1`3 - p3`3*p1`2) + p2`2*(p3`3*p1`1 - p3`1*p1`3) + p2`3*(
p3`1*p1`2 - p3`2*p1`1)
.= |( |[ p2`1, p2`2, p2`3 ]|, |[ p3`2*p1`3 - p3`3*p1`2, p3`3*p1`1 - p3`1
*p1`3, p3`1*p1`2 - p3`2*p1`1 ]| )| by Th30
.= |( p2, p3 <X> p1 )| by Th3;
hence thesis;
end;
theorem
|{ p1, p2, p3 }| = |{ p3, p1, p2 }| by Th33;
theorem
|{ p1, p2, p3 }| = |( p1<X>p2, p3 )|
proof
|{ p1, p2, p3 }| = |(|[ p1`1, p1`2, p1`3 ]|, |[ (p2`2*p3`3) - (p2`3*p3`2
), (p2`3*p3`1) - (p2`1*p3`3), (p2`1*p3`2) - (p2`2*p3`1) ]|)| by Th3
.= p1`1*((p2`2*p3`3) - (p2`3*p3`2)) + p1`2*((p2`3*p3`1) - (p2`1*p3`3)) +
p1`3*((p2`1*p3`2) - (p2`2*p3`1)) by Th30
.= p2`2*(p1`1*p3`3) - p2`3*(p1`1*p3`2) + (p2`3*(p1`2*p3`1) - p2`1*(p1`2*
p3`3)) + (p2`1*(p1`3*p3`2) - p2`2*(p1`3*p3`1));
then
|{ p1, p2, p3 }| = (p2`3*p1`2 - p2`2*p1`3)*p3`1 + (p2`1*p1`3 - p2`3*p1`1
)*p3`2 + (p2`2*p1`1 - p2`1*p1`2)*p3`3
.= |( p1 <X> p2, |[ p3`1, p3`2, p3`3 ]| )| by Th30
.= |( p1 <X> p2, p3 )| by Th3;
hence thesis;
end;
registration
cluster TOP-REAL 3 -> up-3-dimensional;
coherence
proof
take u = |[1,0,0]|, v = |[0,1,0]|, w = |[0,0,1]|;
let a,b,c be Real such that
A1: a*u + b*v + c*w = 0.TOP-REAL 3;
A2: |[a,b,c]|`1 = a & |[a,b,c]|`2 = b & |[a,b,c]|`3 = c;
A3: c*w = |[c*0,c*0,c*1]| by Th8;
a*u = |[a*1,a*0,a*0]| & b*v = |[b*0,b*1,b*0]| by Th8;
then a*u + b*v + c*w = |[a+0,0+b,0+0]| + c*w by Th6
.= |[a+0,b+0,0+c]| by A3,Th6;
hence thesis by A1,A2,Th2,Th4;
end;
end;