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 φ N
ebtwntg.2 P = Base 𝔼 𝒢 N
ebtwntg.3 I = Itv 𝔼 𝒢 N
ebtwntg.x φ X P
ebtwntg.y φ Y P
ebtwntg.z φ Z P
Assertion ebtwntg φ Z Btwn X Y Z X I Y

Proof

Step Hyp Ref Expression
1 ebtwntg.1 φ N
2 ebtwntg.2 P = Base 𝔼 𝒢 N
3 ebtwntg.3 I = Itv 𝔼 𝒢 N
4 ebtwntg.x φ X P
5 ebtwntg.y φ Y P
6 ebtwntg.z φ Z P
7 itvid Itv = Slot Itv ndx
8 fvexd φ 𝔼 𝒢 N V
9 eengstr N 𝔼 𝒢 N Struct 1 17
10 1 9 syl φ 𝔼 𝒢 N Struct 1 17
11 structn0fun 𝔼 𝒢 N Struct 1 17 Fun 𝔼 𝒢 N
12 10 11 syl φ Fun 𝔼 𝒢 N
13 structcnvcnv 𝔼 𝒢 N Struct 1 17 𝔼 𝒢 N -1 -1 = 𝔼 𝒢 N
14 10 13 syl φ 𝔼 𝒢 N -1 -1 = 𝔼 𝒢 N
15 14 funeqd φ Fun 𝔼 𝒢 N -1 -1 Fun 𝔼 𝒢 N
16 12 15 mpbird φ Fun 𝔼 𝒢 N -1 -1
17 opex Itv ndx x 𝔼 N , y 𝔼 N z 𝔼 N | z Btwn x y V
18 17 prid1 Itv ndx x 𝔼 N , y 𝔼 N z 𝔼 N | z Btwn x y Itv ndx x 𝔼 N , y 𝔼 N z 𝔼 N | z Btwn x y Line 𝒢 ndx x 𝔼 N , y 𝔼 N x z 𝔼 N | z Btwn x y x Btwn z y y Btwn x z
19 elun2 Itv ndx x 𝔼 N , y 𝔼 N z 𝔼 N | z Btwn x y Itv ndx x 𝔼 N , y 𝔼 N z 𝔼 N | z Btwn x y Line 𝒢 ndx x 𝔼 N , y 𝔼 N x z 𝔼 N | z Btwn x y x Btwn z y y Btwn x z Itv ndx x 𝔼 N , y 𝔼 N z 𝔼 N | z Btwn x y Base ndx 𝔼 N dist ndx x 𝔼 N , y 𝔼 N i = 1 N x i y i 2 Itv ndx x 𝔼 N , y 𝔼 N z 𝔼 N | z Btwn x y Line 𝒢 ndx x 𝔼 N , y 𝔼 N x z 𝔼 N | z Btwn x y x Btwn z y y Btwn x z
20 18 19 ax-mp Itv ndx x 𝔼 N , y 𝔼 N z 𝔼 N | z Btwn x y Base ndx 𝔼 N dist ndx x 𝔼 N , y 𝔼 N i = 1 N x i y i 2 Itv ndx x 𝔼 N , y 𝔼 N z 𝔼 N | z Btwn x y Line 𝒢 ndx x 𝔼 N , y 𝔼 N x z 𝔼 N | z Btwn x y x Btwn z y y Btwn x z
21 eengv N 𝔼 𝒢 N = Base ndx 𝔼 N dist ndx x 𝔼 N , y 𝔼 N i = 1 N x i y i 2 Itv ndx x 𝔼 N , y 𝔼 N z 𝔼 N | z Btwn x y Line 𝒢 ndx x 𝔼 N , y 𝔼 N x z 𝔼 N | z Btwn x y x Btwn z y y Btwn x z
22 1 21 syl φ 𝔼 𝒢 N = Base ndx 𝔼 N dist ndx x 𝔼 N , y 𝔼 N i = 1 N x i y i 2 Itv ndx x 𝔼 N , y 𝔼 N z 𝔼 N | z Btwn x y Line 𝒢 ndx x 𝔼 N , y 𝔼 N x z 𝔼 N | z Btwn x y x Btwn z y y Btwn x z
23 20 22 eleqtrrid φ Itv ndx x 𝔼 N , y 𝔼 N z 𝔼 N | z Btwn x y 𝔼 𝒢 N
24 fvex 𝔼 N V
25 24 24 mpoex x 𝔼 N , y 𝔼 N z 𝔼 N | z Btwn x y V
26 25 a1i φ x 𝔼 N , y 𝔼 N z 𝔼 N | z Btwn x y V
27 7 8 16 23 26 strfv2d φ x 𝔼 N , y 𝔼 N z 𝔼 N | z Btwn x y = Itv 𝔼 𝒢 N
28 3 27 eqtr4id φ I = x 𝔼 N , y 𝔼 N z 𝔼 N | z Btwn x y
29 simprl φ x = X y = Y x = X
30 simprr φ x = X y = Y y = Y
31 29 30 opeq12d φ x = X y = Y x y = X Y
32 31 breq2d φ x = X y = Y z Btwn x y z Btwn X Y
33 32 rabbidv φ x = X y = Y z 𝔼 N | z Btwn x y = z 𝔼 N | z Btwn X Y
34 4 2 eleqtrdi φ X Base 𝔼 𝒢 N
35 eengbas N 𝔼 N = Base 𝔼 𝒢 N
36 1 35 syl φ 𝔼 N = Base 𝔼 𝒢 N
37 34 36 eleqtrrd φ X 𝔼 N
38 5 2 eleqtrdi φ Y Base 𝔼 𝒢 N
39 38 36 eleqtrrd φ Y 𝔼 N
40 24 rabex z 𝔼 N | z Btwn X Y V
41 40 a1i φ z 𝔼 N | z Btwn X Y V
42 28 33 37 39 41 ovmpod φ X I Y = z 𝔼 N | z Btwn X Y
43 42 eleq2d φ Z X I Y Z z 𝔼 N | z Btwn X Y
44 6 2 eleqtrdi φ Z Base 𝔼 𝒢 N
45 44 36 eleqtrrd φ Z 𝔼 N
46 breq1 z = Z z Btwn X Y Z Btwn X Y
47 46 elrab3 Z 𝔼 N Z z 𝔼 N | z Btwn X Y Z Btwn X Y
48 45 47 syl φ Z z 𝔼 N | z Btwn X Y Z Btwn X Y
49 43 48 bitr2d φ Z Btwn X Y Z X I Y