Metamath Proof Explorer

Theorem lnhl

Description: Either a point C on the line AB is on the same side as A or on the opposite side. (Contributed by Thierry Arnoux, 21-Sep-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
hltr.d ⊢ φ → D ∈ P
lnhl.l ⊢ L = Line 𝒢 ⁡ G
lnhl.1 ⊢ φ → C ∈ A L B
Assertion lnhl ⊢ φ → C K ⁡ B A ∨ B ∈ A I 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 hltr.d ⊢ φ → D ∈ P
9 lnhl.l ⊢ L = Line 𝒢 ⁡ G
10 lnhl.1 ⊢ φ → C ∈ A L B
11 simpr ⊢ φ ∧ C = B → C = B
12 eqid ⊢ dist ⁡ G = dist ⁡ G
13 1 12 2 7 4 6 tgbtwntriv2 ⊢ φ → C ∈ A I C
14 13 adantr ⊢ φ ∧ C = B → C ∈ A I C
15 11 14 eqeltrrd ⊢ φ ∧ C = B → B ∈ A I C
16 15 olcd ⊢ φ ∧ C = B → C K ⁡ B A ∨ B ∈ A I C
17 1 9 2 7 4 5 10 tglngne ⊢ φ → A ≠ B
18 1 9 2 7 4 5 17 6 tgellng ⊢ φ → C ∈ A L B ↔ C ∈ A I B ∨ A ∈ C I B ∨ B ∈ A I C
19 10 18 mpbid ⊢ φ → C ∈ A I B ∨ A ∈ C I B ∨ B ∈ A I C
20 df-3or ⊢ C ∈ A I B ∨ A ∈ C I B ∨ B ∈ A I C ↔ C ∈ A I B ∨ A ∈ C I B ∨ B ∈ A I C
21 19 20 sylib ⊢ φ → C ∈ A I B ∨ A ∈ C I B ∨ B ∈ A I C
22 21 adantr ⊢ φ ∧ C ≠ B → C ∈ A I B ∨ A ∈ C I B ∨ B ∈ A I C
23 1 2 3 6 4 5 7 ishlg ⊢ φ → C K ⁡ B A ↔ C ≠ B ∧ A ≠ B ∧ C ∈ B I A ∨ A ∈ B I C
24 23 adantr ⊢ φ ∧ C ≠ B → C K ⁡ B A ↔ C ≠ B ∧ A ≠ B ∧ C ∈ B I A ∨ A ∈ B I C
25 df-3an ⊢ C ≠ B ∧ A ≠ B ∧ C ∈ B I A ∨ A ∈ B I C ↔ C ≠ B ∧ A ≠ B ∧ C ∈ B I A ∨ A ∈ B I C
26 24 25 bitrdi ⊢ φ ∧ C ≠ B → C K ⁡ B A ↔ C ≠ B ∧ A ≠ B ∧ C ∈ B I A ∨ A ∈ B I C
27 17 anim1ci ⊢ φ ∧ C ≠ B → C ≠ B ∧ A ≠ B
28 27 biantrurd ⊢ φ ∧ C ≠ B → C ∈ B I A ∨ A ∈ B I C ↔ C ≠ B ∧ A ≠ B ∧ C ∈ B I A ∨ A ∈ B I C
29 7 adantr ⊢ φ ∧ C ≠ B → G ∈ 𝒢 Tarski
30 5 adantr ⊢ φ ∧ C ≠ B → B ∈ P
31 6 adantr ⊢ φ ∧ C ≠ B → C ∈ P
32 4 adantr ⊢ φ ∧ C ≠ B → A ∈ P
33 1 12 2 29 30 31 32 tgbtwncomb ⊢ φ ∧ C ≠ B → C ∈ B I A ↔ C ∈ A I B
34 1 12 2 29 30 32 31 tgbtwncomb ⊢ φ ∧ C ≠ B → A ∈ B I C ↔ A ∈ C I B
35 33 34 orbi12d ⊢ φ ∧ C ≠ B → C ∈ B I A ∨ A ∈ B I C ↔ C ∈ A I B ∨ A ∈ C I B
36 26 28 35 3bitr2d ⊢ φ ∧ C ≠ B → C K ⁡ B A ↔ C ∈ A I B ∨ A ∈ C I B
37 36 orbi1d ⊢ φ ∧ C ≠ B → C K ⁡ B A ∨ B ∈ A I C ↔ C ∈ A I B ∨ A ∈ C I B ∨ B ∈ A I C
38 22 37 mpbird ⊢ φ ∧ C ≠ B → C K ⁡ B A ∨ B ∈ A I C
39 16 38 pm2.61dane ⊢ φ → C K ⁡ B A ∨ B ∈ A I C