Metamath Proof Explorer

Theorem elntg

Description: The line definition in the Tarski structure for the Euclidean geometry. (Contributed by Thierry Arnoux, 7-Apr-2019)

Ref Expression
Hypotheses elntg.1 
|- P = ( Base ` ( EEG ` N ) )
elntg.2 
|- I = ( Itv ` ( EEG ` N ) )
Assertion elntg 
|- ( N e. NN -> ( LineG ` ( EEG ` N ) ) = ( x e. P , y e. ( P \ { x } ) |-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) )

Proof

Step Hyp Ref Expression
1 elntg.1 
 |-  P = ( Base ` ( EEG ` N ) )
2 elntg.2 
 |-  I = ( Itv ` ( EEG ` N ) )
3 lngid 
 |-  LineG = Slot ( LineG ` ndx )
4 fvex 
 |-  ( EEG ` N ) e. _V
5 4 a1i 
 |-  ( N e. NN -> ( EEG ` N ) e. _V )
6 eengstr 
 |-  ( N e. NN -> ( EEG ` N ) Struct <. 1 , ; 1 7 >. )
7 structn0fun 
 |-  ( ( EEG ` N ) Struct <. 1 , ; 1 7 >. -> Fun ( ( EEG ` N ) \ { (/) } ) )
8 6 7 syl 
 |-  ( N e. NN -> Fun ( ( EEG ` N ) \ { (/) } ) )
9 structcnvcnv 
 |-  ( ( EEG ` N ) Struct <. 1 , ; 1 7 >. -> `' `' ( EEG ` N ) = ( ( EEG ` N ) \ { (/) } ) )
10 6 9 syl 
 |-  ( N e. NN -> `' `' ( EEG ` N ) = ( ( EEG ` N ) \ { (/) } ) )
11 10 funeqd 
 |-  ( N e. NN -> ( Fun `' `' ( EEG ` N ) <-> Fun ( ( EEG ` N ) \ { (/) } ) ) )
12 8 11 mpbird 
 |-  ( N e. NN -> Fun `' `' ( EEG ` N ) )
13 opex 
 |-  <. ( 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 >. ) } ) >. e. _V
14 13 prid2 
 |-  <. ( 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 >. ) } ) >. e. { <. ( 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 >. ) } ) >. }
15 elun2 
 |-  ( <. ( 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 >. ) } ) >. e. { <. ( 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 >. ) } ) >. } -> <. ( 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 >. ) } ) >. 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 >. ) } ) >. } ) )
16 14 15 ax-mp 
 |-  <. ( 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 >. ) } ) >. 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 >. ) } ) >. } )
17 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 >. ) } ) >. } ) )
18 16 17 eleqtrrid 
 |-  ( N e. NN -> <. ( 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 >. ) } ) >. e. ( EEG ` N ) )
19 fvex 
 |-  ( EE ` N ) e. _V
20 19 difexi 
 |-  ( ( EE ` N ) \ { x } ) e. _V
21 19 20 mpoex 
 |-  ( 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 >. ) } ) e. _V
22 21 a1i 
 |-  ( N e. NN -> ( 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 >. ) } ) e. _V )
23 3 5 12 18 22 strfv2d 
 |-  ( N e. NN -> ( 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 >. ) } ) = ( LineG ` ( EEG ` N ) ) )
24 eengbas 
 |-  ( N e. NN -> ( EE ` N ) = ( Base ` ( EEG ` N ) ) )
25 24 1 eqtr4di 
 |-  ( N e. NN -> ( EE ` N ) = P )
26 25 difeq1d 
 |-  ( N e. NN -> ( ( EE ` N ) \ { x } ) = ( P \ { x } ) )
27 26 adantr 
 |-  ( ( N e. NN /\ x e. ( EE ` N ) ) -> ( ( EE ` N ) \ { x } ) = ( P \ { x } ) )
28 25 adantr 
 |-  ( ( N e. NN /\ ( x e. ( EE ` N ) /\ y e. ( ( EE ` N ) \ { x } ) ) ) -> ( EE ` N ) = P )
29 simpll 
 |-  ( ( ( N e. NN /\ ( x e. ( EE ` N ) /\ y e. ( ( EE ` N ) \ { x } ) ) ) /\ z e. ( EE ` N ) ) -> N e. NN )
30 simplrl 
 |-  ( ( ( N e. NN /\ ( x e. ( EE ` N ) /\ y e. ( ( EE ` N ) \ { x } ) ) ) /\ z e. ( EE ` N ) ) -> x e. ( EE ` N ) )
31 29 25 syl 
 |-  ( ( ( N e. NN /\ ( x e. ( EE ` N ) /\ y e. ( ( EE ` N ) \ { x } ) ) ) /\ z e. ( EE ` N ) ) -> ( EE ` N ) = P )
32 30 31 eleqtrd 
 |-  ( ( ( N e. NN /\ ( x e. ( EE ` N ) /\ y e. ( ( EE ` N ) \ { x } ) ) ) /\ z e. ( EE ` N ) ) -> x e. P )
33 simplrr 
 |-  ( ( ( N e. NN /\ ( x e. ( EE ` N ) /\ y e. ( ( EE ` N ) \ { x } ) ) ) /\ z e. ( EE ` N ) ) -> y e. ( ( EE ` N ) \ { x } ) )
34 33 eldifad 
 |-  ( ( ( N e. NN /\ ( x e. ( EE ` N ) /\ y e. ( ( EE ` N ) \ { x } ) ) ) /\ z e. ( EE ` N ) ) -> y e. ( EE ` N ) )
35 34 31 eleqtrd 
 |-  ( ( ( N e. NN /\ ( x e. ( EE ` N ) /\ y e. ( ( EE ` N ) \ { x } ) ) ) /\ z e. ( EE ` N ) ) -> y e. P )
36 simpr 
 |-  ( ( ( N e. NN /\ ( x e. ( EE ` N ) /\ y e. ( ( EE ` N ) \ { x } ) ) ) /\ z e. ( EE ` N ) ) -> z e. ( EE ` N ) )
37 36 31 eleqtrd 
 |-  ( ( ( N e. NN /\ ( x e. ( EE ` N ) /\ y e. ( ( EE ` N ) \ { x } ) ) ) /\ z e. ( EE ` N ) ) -> z e. P )
38 29 1 2 32 35 37 ebtwntg 
 |-  ( ( ( N e. NN /\ ( x e. ( EE ` N ) /\ y e. ( ( EE ` N ) \ { x } ) ) ) /\ z e. ( EE ` N ) ) -> ( z Btwn <. x , y >. <-> z e. ( x I y ) ) )
39 29 1 2 37 35 32 ebtwntg 
 |-  ( ( ( N e. NN /\ ( x e. ( EE ` N ) /\ y e. ( ( EE ` N ) \ { x } ) ) ) /\ z e. ( EE ` N ) ) -> ( x Btwn <. z , y >. <-> x e. ( z I y ) ) )
40 29 1 2 32 37 35 ebtwntg 
 |-  ( ( ( N e. NN /\ ( x e. ( EE ` N ) /\ y e. ( ( EE ` N ) \ { x } ) ) ) /\ z e. ( EE ` N ) ) -> ( y Btwn <. x , z >. <-> y e. ( x I z ) ) )
41 38 39 40 3orbi123d 
 |-  ( ( ( N e. NN /\ ( 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 >. ) <-> ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) )
42 28 41 rabeqbidva 
 |-  ( ( N e. NN /\ ( 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 >. ) } = { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } )
43 25 27 42 mpoeq123dva 
 |-  ( N e. NN -> ( 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 >. ) } ) = ( x e. P , y e. ( P \ { x } ) |-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) )
44 23 43 eqtr3d 
 |-  ( N e. NN -> ( LineG ` ( EEG ` N ) ) = ( x e. P , y e. ( P \ { x } ) |-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) )