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=BaseG
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∈ALB
Assertion lnhl ⊢φ→CK⁡BA∨B∈AIC

Proof

Step Hyp Ref Expression
1 ishlg.p ⊢P=BaseG
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∈ALB
11 simpr ⊢φ∧C=B→C=B
12 eqid ⊢dist⁡G=dist⁡G
13 1 12 2 7 4 6 tgbtwntriv2 ⊢φ→C∈AIC
14 13 adantr ⊢φ∧C=B→C∈AIC
15 11 14 eqeltrrd ⊢φ∧C=B→B∈AIC
16 15 olcd ⊢φ∧C=B→CK⁡BA∨B∈AIC
17 1 9 2 7 4 5 10 tglngne ⊢φ→A≠B
18 1 9 2 7 4 5 17 6 tgellng ⊢φ→C∈ALB↔C∈AIB∨A∈CIB∨B∈AIC
19 10 18 mpbid ⊢φ→C∈AIB∨A∈CIB∨B∈AIC
20 df-3or ⊢C∈AIB∨A∈CIB∨B∈AIC↔C∈AIB∨A∈CIB∨B∈AIC
21 19 20 sylib ⊢φ→C∈AIB∨A∈CIB∨B∈AIC
22 21 adantr ⊢φ∧C≠B→C∈AIB∨A∈CIB∨B∈AIC
23 1 2 3 6 4 5 7 ishlg ⊢φ→CK⁡BA↔C≠B∧A≠B∧C∈BIA∨A∈BIC
24 23 adantr ⊢φ∧C≠B→CK⁡BA↔C≠B∧A≠B∧C∈BIA∨A∈BIC
25 df-3an ⊢C≠B∧A≠B∧C∈BIA∨A∈BIC↔C≠B∧A≠B∧C∈BIA∨A∈BIC
26 24 25 bitrdi ⊢φ∧C≠B→CK⁡BA↔C≠B∧A≠B∧C∈BIA∨A∈BIC
27 17 anim1ci ⊢φ∧C≠B→C≠B∧A≠B
28 27 biantrurd ⊢φ∧C≠B→C∈BIA∨A∈BIC↔C≠B∧A≠B∧C∈BIA∨A∈BIC
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∈BIA↔C∈AIB
34 1 12 2 29 30 32 31 tgbtwncomb ⊢φ∧C≠B→A∈BIC↔A∈CIB
35 33 34 orbi12d ⊢φ∧C≠B→C∈BIA∨A∈BIC↔C∈AIB∨A∈CIB
36 26 28 35 3bitr2d ⊢φ∧C≠B→CK⁡BA↔C∈AIB∨A∈CIB
37 36 orbi1d ⊢φ∧C≠B→CK⁡BA∨B∈AIC↔C∈AIB∨A∈CIB∨B∈AIC
38 22 37 mpbird ⊢φ∧C≠B→CK⁡BA∨B∈AIC
39 16 38 pm2.61dane ⊢φ→CK⁡BA∨B∈AIC