Metamath Proof Explorer

Theorem hlln

Description: The half-line relation implies colinearity, part of Theorem 6.4 of Schwabhauser p. 44. (Contributed by Thierry Arnoux, 22-Feb-2020)

Ref Expression
Hypotheses ishlg.p ⊢ P = Base G
ishlg.i ⊢ I = Itv ⁡ G
ishlg.k ⊢ K = hl 𝒢 ⁡ G
ishlg.a ⊢ φ → A ∈ P
ishlg.b ⊢ φ → B ∈ P
ishlg.c ⊢ φ → C ∈ P
hlln.1 ⊢ φ → G ∈ 𝒢 Tarski
hlln.l ⊢ L = Line 𝒢 ⁡ G
hlln.2 ⊢ φ → A K ⁡ C B
Assertion hlln ⊢ φ → A ∈ B L C

Proof

Step Hyp Ref Expression
1 ishlg.p ⊢ P = Base G
2 ishlg.i ⊢ I = Itv ⁡ G
3 ishlg.k ⊢ K = hl 𝒢 ⁡ G
4 ishlg.a ⊢ φ → A ∈ P
5 ishlg.b ⊢ φ → B ∈ P
6 ishlg.c ⊢ φ → C ∈ P
7 hlln.1 ⊢ φ → G ∈ 𝒢 Tarski
8 hlln.l ⊢ L = Line 𝒢 ⁡ G
9 hlln.2 ⊢ φ → A K ⁡ C B
10 eqid ⊢ dist ⁡ G = dist ⁡ G
11 7 adantr ⊢ φ ∧ A ∈ C I B → G ∈ 𝒢 Tarski
12 6 adantr ⊢ φ ∧ A ∈ C I B → C ∈ P
13 4 adantr ⊢ φ ∧ A ∈ C I B → A ∈ P
14 5 adantr ⊢ φ ∧ A ∈ C I B → B ∈ P
15 simpr ⊢ φ ∧ A ∈ C I B → A ∈ C I B
16 1 10 2 11 12 13 14 15 tgbtwncom ⊢ φ ∧ A ∈ C I B → A ∈ B I C
17 16 3mix1d ⊢ φ ∧ A ∈ C I B → A ∈ B I C ∨ B ∈ A I C ∨ C ∈ B I A
18 7 adantr ⊢ φ ∧ B ∈ C I A → G ∈ 𝒢 Tarski
19 6 adantr ⊢ φ ∧ B ∈ C I A → C ∈ P
20 5 adantr ⊢ φ ∧ B ∈ C I A → B ∈ P
21 4 adantr ⊢ φ ∧ B ∈ C I A → A ∈ P
22 simpr ⊢ φ ∧ B ∈ C I A → B ∈ C I A
23 1 10 2 18 19 20 21 22 tgbtwncom ⊢ φ ∧ B ∈ C I A → B ∈ A I C
24 23 3mix2d ⊢ φ ∧ B ∈ C I A → A ∈ B I C ∨ B ∈ A I C ∨ C ∈ B I A
25 1 2 3 4 5 6 7 ishlg ⊢ φ → A K ⁡ C B ↔ A ≠ C ∧ B ≠ C ∧ A ∈ C I B ∨ B ∈ C I A
26 9 25 mpbid ⊢ φ → A ≠ C ∧ B ≠ C ∧ A ∈ C I B ∨ B ∈ C I A
27 26 simp3d ⊢ φ → A ∈ C I B ∨ B ∈ C I A
28 17 24 27 mpjaodan ⊢ φ → A ∈ B I C ∨ B ∈ A I C ∨ C ∈ B I A
29 26 simp2d ⊢ φ → B ≠ C
30 1 8 2 7 5 6 29 4 tgellng ⊢ φ → A ∈ B L C ↔ A ∈ B I C ∨ B ∈ A I C ∨ C ∈ B I A
31 28 30 mpbird ⊢ φ → A ∈ B L C