Metamath Proof Explorer

Theorem eengbas

Description: The Base of the Euclidean geometry. (Contributed by Thierry Arnoux, 15-Mar-2019)

Ref Expression
Assertion eengbas 
|- ( N e. NN -> ( EE ` N ) = ( Base ` ( EEG ` N ) ) )

Proof

Step Hyp Ref Expression
1 eengstr 
 |-  ( N e. NN -> ( EEG ` N ) Struct <. 1 , ; 1 7 >. )
2 fvexd 
 |-  ( N e. NN -> ( EE ` N ) e. _V )
3 opex 
 |-  <. ( Base ` ndx ) , ( EE ` N ) >. e. _V
4 3 prid1 
 |-  <. ( Base ` ndx ) , ( EE ` N ) >. e. { <. ( Base ` ndx ) , ( EE ` N ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. }
5 elun1 
 |-  ( <. ( Base ` ndx ) , ( EE ` N ) >. e. { <. ( Base ` ndx ) , ( EE ` N ) >. , <. ( dist ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> sum_ i e. ( 1 ... N ) ( ( ( x ` i ) - ( y ` i ) ) ^ 2 ) ) >. } -> <. ( Base ` ndx ) , ( EE ` N ) >. e. ( { <. ( 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 >. ) } ) >. } ) )
6 4 5 ax-mp 
 |-  <. ( Base ` ndx ) , ( EE ` N ) >. e. ( { <. ( 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 >. ) } ) >. } )
7 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 >. ) } ) >. } ) )
8 6 7 eleqtrrid 
 |-  ( N e. NN -> <. ( Base ` ndx ) , ( EE ` N ) >. e. ( EEG ` N ) )
9 1 2 8 opelstrbas 
 |-  ( N e. NN -> ( EE ` N ) = ( Base ` ( EEG ` N ) ) )