:: EUCLID_5 semantic presentation

theorem Th1: :: EUCLID_5:1

for b₁ being Point of (TOP-REAL 3) ex b₂, b₃, b₄ being Real st b₁ = <*b₂,b₃,b₄*>

proof end;

definition

let c₁ be Point of (TOP-REAL 3);
func c₁ `1 -> Real means :Def1: :: EUCLID_5:def 1
for b₁ being FinSequence st a₁ = b₁ holds
a₂ = b₁ . 1;
existence

proof end;

uniqueness

proof end;

func c₁ `2 -> Real means :Def2: :: EUCLID_5:def 2
for b₁ being FinSequence st a₁ = b₁ holds
a₂ = b₁ . 2;
existence

proof end;

uniqueness

proof end;

func c₁ `3 -> Real means :Def3: :: EUCLID_5:def 3
for b₁ being FinSequence st a₁ = b₁ holds
a₂ = b₁ . 3;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines `1 EUCLID_5:def 1 :

:: deftheorem Def2 defines `2 EUCLID_5:def 2 :

:: deftheorem Def3 defines `3 EUCLID_5:def 3 :

definition

let c₁, c₂, c₃ be Real;
func |[c₁,c₂,c₃]| -> Point of (TOP-REAL 3) equals :: EUCLID_5:def 4
<*a₁,a₂,a₃*>;
coherence

proof end;

end;

:: deftheorem Def4 defines |[ EUCLID_5:def 4 :

theorem Th2: :: EUCLID_5:2

for b₁, b₂, b₃ being Real holds
( |[b₁,b₂,b₃]| `1 = b₁ & |[b₁,b₂,b₃]| `2 = b₂ & |[b₁,b₂,b₃]| `3 = b₃ )

proof end;

theorem Th3: :: EUCLID_5:3

for b₁ being Point of (TOP-REAL 3) holds b₁ = |[(b₁ `1 ),(b₁ `2 ),(b₁ `3 )]|

proof end;

theorem Th4: :: EUCLID_5:4

0.REAL 3 = |[0,0,0]|

proof end;

theorem Th5: :: EUCLID_5:5

for b₁, b₂ being Point of (TOP-REAL 3) holds b₁ + b₂ = |[((b₁ `1 ) + (b₂ `1 )),((b₁ `2 ) + (b₂ `2 )),((b₁ `3 ) + (b₂ `3 ))]|

proof end;

theorem Th6: :: EUCLID_5:6

for b₁, b₂, b₃, b₄, b₅, b₆ being Real holds |[b₁,b₂,b₃]| + |[b₄,b₅,b₆]| = |[(b₁ + b₄),(b₂ + b₅),(b₃ + b₆)]|

proof end;

theorem Th7: :: EUCLID_5:7

for b₁ being Real
for b₂ being Point of (TOP-REAL 3) holds b₁ * b₂ = |[(b₁ * (b₂ `1 )),(b₁ * (b₂ `2 )),(b₁ * (b₂ `3 ))]|

proof end;

theorem Th8: :: EUCLID_5:8

for b₁, b₂, b₃, b₄ being Real holds b₁ * |[b₂,b₃,b₄]| = |[(b₁ * b₂),(b₁ * b₃),(b₁ * b₄)]|

proof end;

theorem Th9: :: EUCLID_5:9

for b₁ being Real
for b₂ being Point of (TOP-REAL 3) holds
( (b₁ * b₂) `1 = b₁ * (b₂ `1 ) & (b₁ * b₂) `2 = b₁ * (b₂ `2 ) & (b₁ * b₂) `3 = b₁ * (b₂ `3 ) )

proof end;

theorem Th10: :: EUCLID_5:10

for b₁ being Point of (TOP-REAL 3) holds - b₁ = |[(- (b₁ `1 )),(- (b₁ `2 )),(- (b₁ `3 ))]|

proof end;

theorem Th11: :: EUCLID_5:11

for b₁, b₂, b₃ being Real holds - |[b₁,b₂,b₃]| = |[(- b₁),(- b₂),(- b₃)]|

proof end;

theorem Th12: :: EUCLID_5:12

for b₁, b₂ being Point of (TOP-REAL 3) holds b₁ - b₂ = |[((b₁ `1 ) - (b₂ `1 )),((b₁ `2 ) - (b₂ `2 )),((b₁ `3 ) - (b₂ `3 ))]|

proof end;

theorem Th13: :: EUCLID_5:13

for b₁, b₂, b₃, b₄, b₅, b₆ being Real holds |[b₁,b₂,b₃]| - |[b₄,b₅,b₆]| = |[(b₁ - b₄),(b₂ - b₅),(b₃ - b₆)]|

proof end;

definition

let c₁, c₂ be Point of (TOP-REAL 3);
func c₁ <X> c₂ -> Point of (TOP-REAL 3) equals :: EUCLID_5:def 5
|[(((a₁ `2 ) * (a₂ `3 )) - ((a₁ `3 ) * (a₂ `2 ))),(((a₁ `3 ) * (a₂ `1 )) - ((a₁ `1 ) * (a₂ `3 ))),(((a₁ `1 ) * (a₂ `2 )) - ((a₁ `2 ) * (a₂ `1 )))]|;
correctness ;

end;

:: deftheorem Def5 defines <X> EUCLID_5:def 5 :

theorem Th14: :: EUCLID_5:14

for b₁, b₂, b₃ being Real
for b₄ being Point of (TOP-REAL 3) st b₄ = |[b₁,b₂,b₃]| holds
( b₄ `1 = b₁ & b₄ `2 = b₂ & b₄ `3 = b₃ ) by Th2;

theorem Th15: :: EUCLID_5:15

for b₁, b₂, b₃, b₄, b₅, b₆ being Real holds |[b₁,b₂,b₃]| <X> |[b₄,b₅,b₆]| = |[((b₂ * b₆) - (b₃ * b₅)),((b₃ * b₄) - (b₁ * b₆)),((b₁ * b₅) - (b₂ * b₄))]|

proof end;

theorem Th16: :: EUCLID_5:16

for b₁ being Real
for b₂, b₃ being Point of (TOP-REAL 3) holds
( (b₁ * b₂) <X> b₃ = b₁ * (b₂ <X> b₃) & (b₁ * b₂) <X> b₃ = b₂ <X> (b₁ * b₃) )

proof end;

theorem Th17: :: EUCLID_5:17

for b₁, b₂ being Point of (TOP-REAL 3) holds b₁ <X> b₂ = - (b₂ <X> b₁)

proof end;

theorem Th18: :: EUCLID_5:18

for b₁, b₂ being Point of (TOP-REAL 3) holds (- b₁) <X> b₂ = b₁ <X> (- b₂)

proof end;

theorem Th19: :: EUCLID_5:19

for b₁, b₂, b₃ being Real holds |[0,0,0]| <X> |[b₁,b₂,b₃]| = 0.REAL 3

proof end;

theorem Th20: :: EUCLID_5:20

for b₁, b₂ being Real holds |[b₁,0,0]| <X> |[b₂,0,0]| = 0.REAL 3

proof end;

theorem Th21: :: EUCLID_5:21

for b₁, b₂ being Real holds |[0,b₁,0]| <X> |[0,b₂,0]| = 0.REAL 3

proof end;

theorem Th22: :: EUCLID_5:22

for b₁, b₂ being Real holds |[0,0,b₁]| <X> |[0,0,b₂]| = 0.REAL 3

proof end;

theorem Th23: :: EUCLID_5:23

for b₁, b₂, b₃ being Point of (TOP-REAL 3) holds b₁ <X> (b₂ + b₃) = (b₁ <X> b₂) + (b₁ <X> b₃)

proof end;

theorem Th24: :: EUCLID_5:24

for b₁, b₂, b₃ being Point of (TOP-REAL 3) holds (b₁ + b₂) <X> b₃ = (b₁ <X> b₃) + (b₂ <X> b₃)

proof end;

theorem Th25: :: EUCLID_5:25

for b₁ being Point of (TOP-REAL 3) holds b₁ <X> b₁ = 0.REAL 3 by Th4;

theorem Th26: :: EUCLID_5:26

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 3) holds (b₁ + b₂) <X> (b₃ + b₄) = (((b₁ <X> b₃) + (b₁ <X> b₄)) + (b₂ <X> b₃)) + (b₂ <X> b₄)

proof end;

theorem Th27: :: EUCLID_5:27

for b₁ being Point of (TOP-REAL 3) holds b₁ = <*(b₁ `1 ),(b₁ `2 ),(b₁ `3 )*>

proof end;

theorem Th28: :: EUCLID_5:28

for b₁, b₂ being FinSequence of REAL st len b₁ = 3 & len b₂ = 3 holds
mlt b₁,b₂ = <*((b₁ . 1) * (b₂ . 1)),((b₁ . 2) * (b₂ . 2)),((b₁ . 3) * (b₂ . 3))*>

proof end;

theorem Th29: :: EUCLID_5:29

for b₁, b₂ being Point of (TOP-REAL 3) holds |(b₁,b₂)| = (((b₁ `1 ) * (b₂ `1 )) + ((b₁ `2 ) * (b₂ `2 ))) + ((b₁ `3 ) * (b₂ `3 ))

proof end;

theorem Th30: :: EUCLID_5:30

for b₁, b₂ being Element of REAL
for b₃, b₄, b₅, b₆ being Real holds |(|[b₃,b₄,b₁]|,|[b₅,b₆,b₂]|)| = ((b₃ * b₅) + (b₄ * b₆)) + (b₁ * b₂)

proof end;

definition

let c₁, c₂, c₃ be Point of (TOP-REAL 3);
func |{c₁,c₂,c₃}| -> real number equals :: EUCLID_5:def 6
|(a₁,(a₂ <X> a₃))|;
coherence ;

end;

:: deftheorem Def6 defines |{ EUCLID_5:def 6 :

theorem Th31: :: EUCLID_5:31

for b₁, b₂ being Point of (TOP-REAL 3) holds
( |{b₁,b₁,b₂}| = 0 & |{b₂,b₁,b₂}| = 0 )

proof end;

theorem Th32: :: EUCLID_5:32

for b₁, b₂, b₃ being Point of (TOP-REAL 3) holds b₁ <X> (b₂ <X> b₃) = (|(b₁,b₃)| * b₂) - (|(b₁,b₂)| * b₃)

proof end;

theorem Th33: :: EUCLID_5:33

for b₁, b₂, b₃ being Point of (TOP-REAL 3) holds |{b₁,b₂,b₃}| = |{b₂,b₃,b₁}|

proof end;

theorem Th34: :: EUCLID_5:34

for b₁, b₂, b₃ being Point of (TOP-REAL 3) holds |{b₁,b₂,b₃}| = |{b₃,b₁,b₂}| by Th33;

theorem Th35: :: EUCLID_5:35

for b₁, b₂, b₃ being Point of (TOP-REAL 3) holds |{b₁,b₂,b₃}| = |((b₁ <X> b₂),b₃)|

proof end;