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 𝔼 𝒢 ⁡ N
elntg.2 ⊢ I = Itv ⁡ 𝔼 𝒢 ⁡ N
Assertion elntg ⊢ N ∈ ℕ → Line 𝒢 ⁡ 𝔼 𝒢 ⁡ N = x ∈ P , y ∈ P ∖ x ⟼ z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z

Proof

Step Hyp Ref Expression
1 elntg.1 ⊢ P = Base 𝔼 𝒢 ⁡ N
2 elntg.2 ⊢ I = Itv ⁡ 𝔼 𝒢 ⁡ N
3 lngid ⊢ Line 𝒢 = Slot Line 𝒢 ⁡ ndx
4 fvex ⊢ 𝔼 𝒢 ⁡ N ∈ V
5 4 a1i ⊢ N ∈ ℕ → 𝔼 𝒢 ⁡ N ∈ V
6 eengstr ⊢ N ∈ ℕ → 𝔼 𝒢 ⁡ N Struct 1 17
7 structn0fun ⊢ 𝔼 𝒢 ⁡ N Struct 1 17 → Fun ⁡ 𝔼 𝒢 ⁡ N ∖ ∅
8 6 7 syl ⊢ N ∈ ℕ → Fun ⁡ 𝔼 𝒢 ⁡ N ∖ ∅
9 structcnvcnv ⊢ 𝔼 𝒢 ⁡ N Struct 1 17 → 𝔼 𝒢 ⁡ N -1 -1 = 𝔼 𝒢 ⁡ N ∖ ∅
10 6 9 syl ⊢ N ∈ ℕ → 𝔼 𝒢 ⁡ N -1 -1 = 𝔼 𝒢 ⁡ N ∖ ∅
11 10 funeqd ⊢ N ∈ ℕ → Fun ⁡ 𝔼 𝒢 ⁡ N -1 -1 ↔ Fun ⁡ 𝔼 𝒢 ⁡ N ∖ ∅
12 8 11 mpbird ⊢ N ∈ ℕ → Fun ⁡ 𝔼 𝒢 ⁡ N -1 -1
13 opex ⊢ Line 𝒢 ⁡ ndx x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ∖ x ⟼ z ∈ 𝔼 ⁡ N | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z ∈ V
14 13 prid2 ⊢ 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 Line 𝒢 ⁡ ndx x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ∖ x ⟼ z ∈ 𝔼 ⁡ N | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z
15 elun2 ⊢ 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 Line 𝒢 ⁡ ndx x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ∖ x ⟼ z ∈ 𝔼 ⁡ N | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z → Line 𝒢 ⁡ ndx x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ∖ x ⟼ z ∈ 𝔼 ⁡ N | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z ∈ 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
16 14 15 ax-mp ⊢ Line 𝒢 ⁡ ndx x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ∖ x ⟼ z ∈ 𝔼 ⁡ N | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z ∈ 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
17 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
18 16 17 eleqtrrid ⊢ N ∈ ℕ → Line 𝒢 ⁡ ndx x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ∖ x ⟼ z ∈ 𝔼 ⁡ N | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z ∈ 𝔼 𝒢 ⁡ N
19 fvex ⊢ 𝔼 ⁡ N ∈ V
20 19 difexi ⊢ 𝔼 ⁡ N ∖ x ∈ V
21 19 20 mpoex ⊢ x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ∖ x ⟼ z ∈ 𝔼 ⁡ N | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z ∈ V
22 21 a1i ⊢ N ∈ ℕ → x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ∖ x ⟼ z ∈ 𝔼 ⁡ N | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z ∈ V
23 3 5 12 18 22 strfv2d ⊢ N ∈ ℕ → x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ∖ x ⟼ z ∈ 𝔼 ⁡ N | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z = Line 𝒢 ⁡ 𝔼 𝒢 ⁡ N
24 eengbas ⊢ N ∈ ℕ → 𝔼 ⁡ N = Base 𝔼 𝒢 ⁡ N
25 24 1 eqtr4di ⊢ N ∈ ℕ → 𝔼 ⁡ N = P
26 25 difeq1d ⊢ N ∈ ℕ → 𝔼 ⁡ N ∖ x = P ∖ x
27 26 adantr ⊢ N ∈ ℕ ∧ x ∈ 𝔼 ⁡ N → 𝔼 ⁡ N ∖ x = P ∖ x
28 25 adantr ⊢ N ∈ ℕ ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N ∖ x → 𝔼 ⁡ N = P
29 simpll ⊢ N ∈ ℕ ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N ∖ x ∧ z ∈ 𝔼 ⁡ N → N ∈ ℕ
30 simplrl ⊢ N ∈ ℕ ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N ∖ x ∧ z ∈ 𝔼 ⁡ N → x ∈ 𝔼 ⁡ N
31 29 25 syl ⊢ N ∈ ℕ ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N ∖ x ∧ z ∈ 𝔼 ⁡ N → 𝔼 ⁡ N = P
32 30 31 eleqtrd ⊢ N ∈ ℕ ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N ∖ x ∧ z ∈ 𝔼 ⁡ N → x ∈ P
33 simplrr ⊢ N ∈ ℕ ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N ∖ x ∧ z ∈ 𝔼 ⁡ N → y ∈ 𝔼 ⁡ N ∖ x
34 33 eldifad ⊢ N ∈ ℕ ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N ∖ x ∧ z ∈ 𝔼 ⁡ N → y ∈ 𝔼 ⁡ N
35 34 31 eleqtrd ⊢ N ∈ ℕ ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N ∖ x ∧ z ∈ 𝔼 ⁡ N → y ∈ P
36 simpr ⊢ N ∈ ℕ ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N ∖ x ∧ z ∈ 𝔼 ⁡ N → z ∈ 𝔼 ⁡ N
37 36 31 eleqtrd ⊢ N ∈ ℕ ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N ∖ x ∧ z ∈ 𝔼 ⁡ N → z ∈ P
38 29 1 2 32 35 37 ebtwntg ⊢ N ∈ ℕ ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N ∖ x ∧ z ∈ 𝔼 ⁡ N → z Btwn x y ↔ z ∈ x I y
39 29 1 2 37 35 32 ebtwntg ⊢ N ∈ ℕ ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N ∖ x ∧ z ∈ 𝔼 ⁡ N → x Btwn z y ↔ x ∈ z I y
40 29 1 2 32 37 35 ebtwntg ⊢ N ∈ ℕ ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N ∖ x ∧ z ∈ 𝔼 ⁡ N → y Btwn x z ↔ y ∈ x I z
41 38 39 40 3orbi123d ⊢ N ∈ ℕ ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N ∖ x ∧ z ∈ 𝔼 ⁡ N → z Btwn x y ∨ x Btwn z y ∨ y Btwn x z ↔ z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
42 28 41 rabeqbidva ⊢ N ∈ ℕ ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N ∖ x → z ∈ 𝔼 ⁡ N | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z = z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
43 25 27 42 mpoeq123dva ⊢ N ∈ ℕ → x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ∖ x ⟼ z ∈ 𝔼 ⁡ N | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z = x ∈ P , y ∈ P ∖ x ⟼ z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
44 23 43 eqtr3d ⊢ N ∈ ℕ → Line 𝒢 ⁡ 𝔼 𝒢 ⁡ N = x ∈ P , y ∈ P ∖ x ⟼ z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z