Metamath Proof Explorer

Theorem ebtwntg

Description: The betweenness relation used in the Tarski structure for the Euclidean geometry is the same as Btwn . (Contributed by Thierry Arnoux, 15-Mar-2019)

Ref Expression
Hypotheses ebtwntg.1 
|- ( ph -> N e. NN )
ebtwntg.2 
|- P = ( Base ` ( EEG ` N ) )
ebtwntg.3 
|- I = ( Itv ` ( EEG ` N ) )
ebtwntg.x 
|- ( ph -> X e. P )
ebtwntg.y 
|- ( ph -> Y e. P )
ebtwntg.z 
|- ( ph -> Z e. P )
Assertion ebtwntg 
|- ( ph -> ( Z Btwn <. X , Y >. <-> Z e. ( X I Y ) ) )

Proof

Step Hyp Ref Expression
1 ebtwntg.1 
 |-  ( ph -> N e. NN )
2 ebtwntg.2 
 |-  P = ( Base ` ( EEG ` N ) )
3 ebtwntg.3 
 |-  I = ( Itv ` ( EEG ` N ) )
4 ebtwntg.x 
 |-  ( ph -> X e. P )
5 ebtwntg.y 
 |-  ( ph -> Y e. P )
6 ebtwntg.z 
 |-  ( ph -> Z e. P )
7 itvid 
 |-  Itv = Slot ( Itv ` ndx )
8 fvexd 
 |-  ( ph -> ( EEG ` N ) e. _V )
9 eengstr 
 |-  ( N e. NN -> ( EEG ` N ) Struct <. 1 , ; 1 7 >. )
10 1 9 syl 
 |-  ( ph -> ( EEG ` N ) Struct <. 1 , ; 1 7 >. )
11 structn0fun 
 |-  ( ( EEG ` N ) Struct <. 1 , ; 1 7 >. -> Fun ( ( EEG ` N ) \ { (/) } ) )
12 10 11 syl 
 |-  ( ph -> Fun ( ( EEG ` N ) \ { (/) } ) )
13 structcnvcnv 
 |-  ( ( EEG ` N ) Struct <. 1 , ; 1 7 >. -> `' `' ( EEG ` N ) = ( ( EEG ` N ) \ { (/) } ) )
14 10 13 syl 
 |-  ( ph -> `' `' ( EEG ` N ) = ( ( EEG ` N ) \ { (/) } ) )
15 14 funeqd 
 |-  ( ph -> ( Fun `' `' ( EEG ` N ) <-> Fun ( ( EEG ` N ) \ { (/) } ) ) )
16 12 15 mpbird 
 |-  ( ph -> Fun `' `' ( EEG ` N ) )
17 opex 
 |-  <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. e. _V
18 17 prid1 
 |-  <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. 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 >. ) } ) >. }
19 elun2 
 |-  ( <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. 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 >. ) } ) >. } -> <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. 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 >. ) } ) >. } ) )
20 18 19 ax-mp 
 |-  <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. 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 >. ) } ) >. } )
21 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 >. ) } ) >. } ) )
22 1 21 syl 
 |-  ( ph -> ( 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 >. ) } ) >. } ) )
23 20 22 eleqtrrid 
 |-  ( ph -> <. ( Itv ` ndx ) , ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) >. e. ( EEG ` N ) )
24 fvex 
 |-  ( EE ` N ) e. _V
25 24 24 mpoex 
 |-  ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) e. _V
26 25 a1i 
 |-  ( ph -> ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) e. _V )
27 7 8 16 23 26 strfv2d 
 |-  ( ph -> ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) = ( Itv ` ( EEG ` N ) ) )
28 3 27 eqtr4id 
 |-  ( ph -> I = ( x e. ( EE ` N ) , y e. ( EE ` N ) |-> { z e. ( EE ` N ) | z Btwn <. x , y >. } ) )
29 simprl 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> x = X )
30 simprr 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> y = Y )
31 29 30 opeq12d 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> <. x , y >. = <. X , Y >. )
32 31 breq2d 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( z Btwn <. x , y >. <-> z Btwn <. X , Y >. ) )
33 32 rabbidv 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> { z e. ( EE ` N ) | z Btwn <. x , y >. } = { z e. ( EE ` N ) | z Btwn <. X , Y >. } )
34 4 2 eleqtrdi 
 |-  ( ph -> X e. ( Base ` ( EEG ` N ) ) )
35 eengbas 
 |-  ( N e. NN -> ( EE ` N ) = ( Base ` ( EEG ` N ) ) )
36 1 35 syl 
 |-  ( ph -> ( EE ` N ) = ( Base ` ( EEG ` N ) ) )
37 34 36 eleqtrrd 
 |-  ( ph -> X e. ( EE ` N ) )
38 5 2 eleqtrdi 
 |-  ( ph -> Y e. ( Base ` ( EEG ` N ) ) )
39 38 36 eleqtrrd 
 |-  ( ph -> Y e. ( EE ` N ) )
40 24 rabex 
 |-  { z e. ( EE ` N ) | z Btwn <. X , Y >. } e. _V
41 40 a1i 
 |-  ( ph -> { z e. ( EE ` N ) | z Btwn <. X , Y >. } e. _V )
42 28 33 37 39 41 ovmpod 
 |-  ( ph -> ( X I Y ) = { z e. ( EE ` N ) | z Btwn <. X , Y >. } )
43 42 eleq2d 
 |-  ( ph -> ( Z e. ( X I Y ) <-> Z e. { z e. ( EE ` N ) | z Btwn <. X , Y >. } ) )
44 6 2 eleqtrdi 
 |-  ( ph -> Z e. ( Base ` ( EEG ` N ) ) )
45 44 36 eleqtrrd 
 |-  ( ph -> Z e. ( EE ` N ) )
46 breq1 
 |-  ( z = Z -> ( z Btwn <. X , Y >. <-> Z Btwn <. X , Y >. ) )
47 46 elrab3 
 |-  ( Z e. ( EE ` N ) -> ( Z e. { z e. ( EE ` N ) | z Btwn <. X , Y >. } <-> Z Btwn <. X , Y >. ) )
48 45 47 syl 
 |-  ( ph -> ( Z e. { z e. ( EE ` N ) | z Btwn <. X , Y >. } <-> Z Btwn <. X , Y >. ) )
49 43 48 bitr2d 
 |-  ( ph -> ( Z Btwn <. X , Y >. <-> Z e. ( X I Y ) ) )