Metamath Proof Explorer

Theorem eengstr

Description: The Euclidean geometry as a structure. (Contributed by Thierry Arnoux, 15-Mar-2019)

Ref Expression
Assertion eengstr 
|- ( N e. NN -> ( EEG ` N ) Struct <. 1 , ; 1 7 >. )

Proof

Step Hyp Ref Expression
1 eengv 
 |-  ( N e. NN -> ( EEG ` N ) = ( { <. ( Base ` ndx ) , ( EE ` N ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } u. { <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` N ) , y e. ( ( EE ` N ) \ { x } ) |-> { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } ) )
2 1nn 
 |-  1 e. NN
3 basendx 
 |-  ( Base ` ndx ) = 1
4 2nn0 
 |-  2 e. NN0
5 1nn0 
 |-  1 e. NN0
6 1lt10 
 |-  1 < ; 1 0
7 2 4 5 6 declti 
 |-  1 < ; 1 2
8 2nn 
 |-  2 e. NN
9 5 8 decnncl 
 |-  ; 1 2 e. NN
10 dsndx 
 |-  ( dist ` ndx ) = ; 1 2
11 2 3 7 9 10 strle2 
 |-  { <. ( Base ` ndx ) , ( EE ` N ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } Struct <. 1 , ; 1 2 >.
12 6nn 
 |-  6 e. NN
13 5 12 decnncl 
 |-  ; 1 6 e. NN
14 itvndx 
 |-  ( Itv ` ndx ) = ; 1 6
15 6nn0 
 |-  6 e. NN0
16 7nn 
 |-  7 e. NN
17 6lt7 
 |-  6 < 7
18 5 15 16 17 declt 
 |-  ; 1 6 < ; 1 7
19 5 16 decnncl 
 |-  ; 1 7 e. NN
20 lngndx 
 |-  ( LineG ` ndx ) = ; 1 7
21 13 14 18 19 20 strle2 
 |-  { <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` N ) , y e. ( ( EE ` N ) \ { x } ) |-> { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } Struct <. ; 1 6 , ; 1 7 >.
22 2lt6 
 |-  2 < 6
23 5 4 12 22 declt 
 |-  ; 1 2 < ; 1 6
24 11 21 23 strleun 
 |-  ( { <. ( Base ` ndx ) , ( EE ` N ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } u. { <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. , <. ( LineG ` ndx ) , ( x e. ( EE ` N ) , y e. ( ( EE ` N ) \ { x } ) |-> { z e. ( EE ` N ) | ( z Btwn <. x , y >. \/ x Btwn <. z , y >. \/ y Btwn <. x , z >. ) } ) >. } ) Struct <. 1 , ; 1 7 >.
25 1 24 eqbrtrdi 
 |-  ( N e. NN -> ( EEG ` N ) Struct <. 1 , ; 1 7 >. )