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 ) ) )