:: EUCLID_5 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: EUCLID_5:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Point of (TOP-REAL 3) ex x, y, z being Real st p = <*x,y,z*>
proof end;

definition
let p be Point of (TOP-REAL 3);
func p `1 -> Real means :Def1: :: EUCLID_5:def 1
for f being FinSequence st p = f holds
it = f . 1;
existence
ex b1 being Real st
for f being FinSequence st p = f holds
b1 = f . 1
proof end;
uniqueness
for b1, b2 being Real st ( for f being FinSequence st p = f holds
b1 = f . 1 ) & ( for f being FinSequence st p = f holds
b2 = f . 1 ) holds
b1 = b2
proof end;
func p `2 -> Real means :Def2: :: EUCLID_5:def 2
for f being FinSequence st p = f holds
it = f . 2;
existence
ex b1 being Real st
for f being FinSequence st p = f holds
b1 = f . 2
proof end;
uniqueness
for b1, b2 being Real st ( for f being FinSequence st p = f holds
b1 = f . 2 ) & ( for f being FinSequence st p = f holds
b2 = f . 2 ) holds
b1 = b2
proof end;
func p `3 -> Real means :Def3: :: EUCLID_5:def 3
for f being FinSequence st p = f holds
it = f . 3;
existence
ex b1 being Real st
for f being FinSequence st p = f holds
b1 = f . 3
proof end;
uniqueness
for b1, b2 being Real st ( for f being FinSequence st p = f holds
b1 = f . 3 ) & ( for f being FinSequence st p = f holds
b2 = f . 3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines `1 EUCLID_5:def 1 :
for p being Point of (TOP-REAL 3)
for b2 being Real holds
( b2 = p `1 iff for f being FinSequence st p = f holds
b2 = f . 1 );

:: deftheorem Def2 defines `2 EUCLID_5:def 2 :
for p being Point of (TOP-REAL 3)
for b2 being Real holds
( b2 = p `2 iff for f being FinSequence st p = f holds
b2 = f . 2 );

:: deftheorem Def3 defines `3 EUCLID_5:def 3 :
for p being Point of (TOP-REAL 3)
for b2 being Real holds
( b2 = p `3 iff for f being FinSequence st p = f holds
b2 = f . 3 );

definition
let x, y, z be Real;
func |[x,y,z]| -> Point of (TOP-REAL 3) equals :: EUCLID_5:def 4
<*x,y,z*>;
coherence
<*x,y,z*> is Point of (TOP-REAL 3)
proof end;
end;

:: deftheorem defines |[ EUCLID_5:def 4 :
for x, y, z being Real holds |[x,y,z]| = <*x,y,z*>;

theorem Th2: :: EUCLID_5:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being Real holds
( |[x,y,z]| `1 = x & |[x,y,z]| `2 = y & |[x,y,z]| `3 = z )
proof end;

theorem Th3: :: EUCLID_5:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Point of (TOP-REAL 3) holds p = |[(p `1 ),(p `2 ),(p `3 )]|
proof end;

theorem Th4: :: EUCLID_5:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
0.REAL 3 = |[0,0,0]|
proof end;

theorem Th5: :: EUCLID_5:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being Point of (TOP-REAL 3) holds p1 + p2 = |[((p1 `1 ) + (p2 `1 )),((p1 `2 ) + (p2 `2 )),((p1 `3 ) + (p2 `3 ))]|
proof end;

theorem Th6: :: EUCLID_5:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, y1, z1, x2, y2, z2 being Real holds |[x1,y1,z1]| + |[x2,y2,z2]| = |[(x1 + x2),(y1 + y2),(z1 + z2)]|
proof end;

theorem Th7: :: EUCLID_5:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Real
for p being Point of (TOP-REAL 3) holds x * p = |[(x * (p `1 )),(x * (p `2 )),(x * (p `3 ))]|
proof end;

theorem Th8: :: EUCLID_5:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, x1, y1, z1 being Real holds x * |[x1,y1,z1]| = |[(x * x1),(x * y1),(x * z1)]|
proof end;

theorem :: EUCLID_5:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Real
for p being Point of (TOP-REAL 3) holds
( (x * p) `1 = x * (p `1 ) & (x * p) `2 = x * (p `2 ) & (x * p) `3 = x * (p `3 ) )
proof end;

theorem Th10: :: EUCLID_5:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Point of (TOP-REAL 3) holds - p = |[(- (p `1 )),(- (p `2 )),(- (p `3 ))]|
proof end;

theorem :: EUCLID_5:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, y1, z1 being Real holds - |[x1,y1,z1]| = |[(- x1),(- y1),(- z1)]|
proof end;

theorem Th12: :: EUCLID_5:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being Point of (TOP-REAL 3) holds p1 - p2 = |[((p1 `1 ) - (p2 `1 )),((p1 `2 ) - (p2 `2 )),((p1 `3 ) - (p2 `3 ))]|
proof end;

theorem Th13: :: EUCLID_5:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, y1, z1, x2, y2, z2 being Real holds |[x1,y1,z1]| - |[x2,y2,z2]| = |[(x1 - x2),(y1 - y2),(z1 - z2)]|
proof end;

definition
let p1, p2 be Point of (TOP-REAL 3);
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 )))]|;
correctness
coherence
|[(((p1 `2 ) * (p2 `3 )) - ((p1 `3 ) * (p2 `2 ))),(((p1 `3 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `3 ))),(((p1 `1 ) * (p2 `2 )) - ((p1 `2 ) * (p2 `1 )))]| is Point of (TOP-REAL 3)
;
;
end;

:: deftheorem defines <X> EUCLID_5:def 5 :
for p1, p2 being Point of (TOP-REAL 3) holds p1 <X> p2 = |[(((p1 `2 ) * (p2 `3 )) - ((p1 `3 ) * (p2 `2 ))),(((p1 `3 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `3 ))),(((p1 `1 ) * (p2 `2 )) - ((p1 `2 ) * (p2 `1 )))]|;

theorem :: EUCLID_5:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being Real
for p being Point of (TOP-REAL 3) st p = |[x,y,z]| holds
( p `1 = x & p `2 = y & p `3 = z ) by Th2;

theorem Th15: :: EUCLID_5:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, y1, z1, x2, y2, z2 being Real holds |[x1,y1,z1]| <X> |[x2,y2,z2]| = |[((y1 * z2) - (z1 * y2)),((z1 * x2) - (x1 * z2)),((x1 * y2) - (y1 * x2))]|
proof end;

theorem :: EUCLID_5:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Real
for p1, p2 being Point of (TOP-REAL 3) holds
( (x * p1) <X> p2 = x * (p1 <X> p2) & (x * p1) <X> p2 = p1 <X> (x * p2) )
proof end;

theorem Th17: :: EUCLID_5:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being Point of (TOP-REAL 3) holds p1 <X> p2 = - (p2 <X> p1)
proof end;

theorem :: EUCLID_5:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being Point of (TOP-REAL 3) holds (- p1) <X> p2 = p1 <X> (- p2)
proof end;

theorem :: EUCLID_5:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being Real holds |[0,0,0]| <X> |[x,y,z]| = 0.REAL 3
proof end;

theorem :: EUCLID_5:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2 being Real holds |[x1,0,0]| <X> |[x2,0,0]| = 0.REAL 3
proof end;

theorem :: EUCLID_5:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y1, y2 being Real holds |[0,y1,0]| <X> |[0,y2,0]| = 0.REAL 3
proof end;

theorem :: EUCLID_5:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Real holds |[0,0,z1]| <X> |[0,0,z2]| = 0.REAL 3
proof end;

theorem Th23: :: EUCLID_5:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2, p3 being Point of (TOP-REAL 3) holds p1 <X> (p2 + p3) = (p1 <X> p2) + (p1 <X> p3)
proof end;

theorem Th24: :: EUCLID_5:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2, p3 being Point of (TOP-REAL 3) holds (p1 + p2) <X> p3 = (p1 <X> p3) + (p2 <X> p3)
proof end;

theorem :: EUCLID_5:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1 being Point of (TOP-REAL 3) holds p1 <X> p1 = 0.REAL 3 by Th4;

theorem :: EUCLID_5:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2, p3, p4 being Point of (TOP-REAL 3) holds (p1 + p2) <X> (p3 + p4) = (((p1 <X> p3) + (p1 <X> p4)) + (p2 <X> p3)) + (p2 <X> p4)
proof end;

theorem Th27: :: EUCLID_5:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Point of (TOP-REAL 3) holds p = <*(p `1 ),(p `2 ),(p `3 )*>
proof end;

theorem Th28: :: EUCLID_5:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being 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 end;

theorem Th29: :: EUCLID_5:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being Point of (TOP-REAL 3) holds |(p1,p2)| = (((p1 `1 ) * (p2 `1 )) + ((p1 `2 ) * (p2 `2 ))) + ((p1 `3 ) * (p2 `3 ))
proof end;

theorem Th30: :: EUCLID_5:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x3, y3 being Element of REAL
for x1, x2, y1, y2 being Real holds |(|[x1,x2,x3]|,|[y1,y2,y3]|)| = ((x1 * y1) + (x2 * y2)) + (x3 * y3)
proof end;

definition
let p1, p2, p3 be Point of (TOP-REAL 3);
func |{p1,p2,p3}| -> real number equals :: EUCLID_5:def 6
|(p1,(p2 <X> p3))|;
coherence
|(p1,(p2 <X> p3))| is real number
;
end;

:: deftheorem defines |{ EUCLID_5:def 6 :
for p1, p2, p3 being Point of (TOP-REAL 3) holds |{p1,p2,p3}| = |(p1,(p2 <X> p3))|;

theorem :: EUCLID_5:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being Point of (TOP-REAL 3) holds
( |{p1,p1,p2}| = 0 & |{p2,p1,p2}| = 0 )
proof end;

theorem :: EUCLID_5:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2, p3 being Point of (TOP-REAL 3) holds p1 <X> (p2 <X> p3) = (|(p1,p3)| * p2) - (|(p1,p2)| * p3)
proof end;

theorem Th33: :: EUCLID_5:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2, p3 being Point of (TOP-REAL 3) holds |{p1,p2,p3}| = |{p2,p3,p1}|
proof end;

theorem :: EUCLID_5:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2, p3 being Point of (TOP-REAL 3) holds |{p1,p2,p3}| = |{p3,p1,p2}| by Th33;

theorem :: EUCLID_5:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2, p3 being Point of (TOP-REAL 3) holds |{p1,p2,p3}| = |((p1 <X> p2),p3)|
proof end;