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 ( 𝜑𝑁 ∈ ℕ )
ebtwntg.2 𝑃 = ( Base ‘ ( EEG ‘ 𝑁 ) )
ebtwntg.3 𝐼 = ( Itv ‘ ( EEG ‘ 𝑁 ) )
ebtwntg.x ( 𝜑𝑋𝑃 )
ebtwntg.y ( 𝜑𝑌𝑃 )
ebtwntg.z ( 𝜑𝑍𝑃 )
Assertion ebtwntg ( 𝜑 → ( 𝑍 Btwn ⟨ 𝑋 , 𝑌 ⟩ ↔ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 ebtwntg.1 ( 𝜑𝑁 ∈ ℕ )
2 ebtwntg.2 𝑃 = ( Base ‘ ( EEG ‘ 𝑁 ) )
3 ebtwntg.3 𝐼 = ( Itv ‘ ( EEG ‘ 𝑁 ) )
4 ebtwntg.x ( 𝜑𝑋𝑃 )
5 ebtwntg.y ( 𝜑𝑌𝑃 )
6 ebtwntg.z ( 𝜑𝑍𝑃 )
7 itvid Itv = Slot ( Itv ‘ ndx )
8 fvexd ( 𝜑 → ( EEG ‘ 𝑁 ) ∈ V )
9 eengstr ( 𝑁 ∈ ℕ → ( EEG ‘ 𝑁 ) Struct ⟨ 1 , 1 7 ⟩ )
10 1 9 syl ( 𝜑 → ( EEG ‘ 𝑁 ) Struct ⟨ 1 , 1 7 ⟩ )
11 structn0fun ( ( EEG ‘ 𝑁 ) Struct ⟨ 1 , 1 7 ⟩ → Fun ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) )
12 10 11 syl ( 𝜑 → Fun ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) )
13 structcnvcnv ( ( EEG ‘ 𝑁 ) Struct ⟨ 1 , 1 7 ⟩ → ( EEG ‘ 𝑁 ) = ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) )
14 10 13 syl ( 𝜑 ( EEG ‘ 𝑁 ) = ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) )
15 14 funeqd ( 𝜑 → ( Fun ( EEG ‘ 𝑁 ) ↔ Fun ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) ) )
16 12 15 mpbird ( 𝜑 → Fun ( EEG ‘ 𝑁 ) )
17 opex ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ ∈ V
18 17 prid1 ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ ∈ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ }
19 elun2 ( ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ ∈ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } → ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ ∈ ( { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥𝑖 ) − ( 𝑦𝑖 ) ) ↑ 2 ) ) ⟩ } ∪ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } ) )
20 18 19 ax-mp ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ ∈ ( { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥𝑖 ) − ( 𝑦𝑖 ) ) ↑ 2 ) ) ⟩ } ∪ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } )
21 eengv ( 𝑁 ∈ ℕ → ( EEG ‘ 𝑁 ) = ( { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥𝑖 ) − ( 𝑦𝑖 ) ) ↑ 2 ) ) ⟩ } ∪ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } ) )
22 1 21 syl ( 𝜑 → ( EEG ‘ 𝑁 ) = ( { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥𝑖 ) − ( 𝑦𝑖 ) ) ↑ 2 ) ) ⟩ } ∪ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } ) )
23 20 22 eleqtrrid ( 𝜑 → ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ ∈ ( EEG ‘ 𝑁 ) )
24 fvex ( 𝔼 ‘ 𝑁 ) ∈ V
25 24 24 mpoex ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ∈ V
26 25 a1i ( 𝜑 → ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ∈ V )
27 7 8 16 23 26 strfv2d ( 𝜑 → ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) = ( Itv ‘ ( EEG ‘ 𝑁 ) ) )
28 3 27 eqtr4id ( 𝜑𝐼 = ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) )
29 simprl ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → 𝑥 = 𝑋 )
30 simprr ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → 𝑦 = 𝑌 )
31 29 30 opeq12d ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑋 , 𝑌 ⟩ )
32 31 breq2d ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑧 Btwn ⟨ 𝑋 , 𝑌 ⟩ ) )
33 32 rabbidv ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } = { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑋 , 𝑌 ⟩ } )
34 4 2 eleqtrdi ( 𝜑𝑋 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) )
35 eengbas ( 𝑁 ∈ ℕ → ( 𝔼 ‘ 𝑁 ) = ( Base ‘ ( EEG ‘ 𝑁 ) ) )
36 1 35 syl ( 𝜑 → ( 𝔼 ‘ 𝑁 ) = ( Base ‘ ( EEG ‘ 𝑁 ) ) )
37 34 36 eleqtrrd ( 𝜑𝑋 ∈ ( 𝔼 ‘ 𝑁 ) )
38 5 2 eleqtrdi ( 𝜑𝑌 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) )
39 38 36 eleqtrrd ( 𝜑𝑌 ∈ ( 𝔼 ‘ 𝑁 ) )
40 24 rabex { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑋 , 𝑌 ⟩ } ∈ V
41 40 a1i ( 𝜑 → { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑋 , 𝑌 ⟩ } ∈ V )
42 28 33 37 39 41 ovmpod ( 𝜑 → ( 𝑋 𝐼 𝑌 ) = { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑋 , 𝑌 ⟩ } )
43 42 eleq2d ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ↔ 𝑍 ∈ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑋 , 𝑌 ⟩ } ) )
44 6 2 eleqtrdi ( 𝜑𝑍 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) )
45 44 36 eleqtrrd ( 𝜑𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
46 breq1 ( 𝑧 = 𝑍 → ( 𝑧 Btwn ⟨ 𝑋 , 𝑌 ⟩ ↔ 𝑍 Btwn ⟨ 𝑋 , 𝑌 ⟩ ) )
47 46 elrab3 ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) → ( 𝑍 ∈ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑋 , 𝑌 ⟩ } ↔ 𝑍 Btwn ⟨ 𝑋 , 𝑌 ⟩ ) )
48 45 47 syl ( 𝜑 → ( 𝑍 ∈ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑋 , 𝑌 ⟩ } ↔ 𝑍 Btwn ⟨ 𝑋 , 𝑌 ⟩ ) )
49 43 48 bitr2d ( 𝜑 → ( 𝑍 Btwn ⟨ 𝑋 , 𝑌 ⟩ ↔ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) )