Metamath Proof Explorer

Theorem btwnhl

Description: Swap betweenness for a half-line. (Contributed by Thierry Arnoux, 2-Mar-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
btwnhl.1 ⊢ φ → A K ⁡ D B
btwnhl.3 ⊢ φ → D ∈ A I C
Assertion btwnhl ⊢ φ → D ∈ B 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 btwnhl.1 ⊢ φ → A K ⁡ D B
10 btwnhl.3 ⊢ φ → D ∈ A I C
11 eqid ⊢ dist ⁡ G = dist ⁡ G
12 7 adantr ⊢ φ ∧ A ∈ D I B → G ∈ 𝒢 Tarski
13 6 adantr ⊢ φ ∧ A ∈ D I B → C ∈ P
14 8 adantr ⊢ φ ∧ A ∈ D I B → D ∈ P
15 5 adantr ⊢ φ ∧ A ∈ D I B → B ∈ P
16 4 adantr ⊢ φ ∧ A ∈ D I B → A ∈ P
17 1 2 3 4 5 8 7 ishlg ⊢ φ → A K ⁡ D B ↔ A ≠ D ∧ B ≠ D ∧ A ∈ D I B ∨ B ∈ D I A
18 9 17 mpbid ⊢ φ → A ≠ D ∧ B ≠ D ∧ A ∈ D I B ∨ B ∈ D I A
19 18 simp1d ⊢ φ → A ≠ D
20 19 necomd ⊢ φ → D ≠ A
21 20 adantr ⊢ φ ∧ A ∈ D I B → D ≠ A
22 10 adantr ⊢ φ ∧ A ∈ D I B → D ∈ A I C
23 1 11 2 12 16 14 13 22 tgbtwncom ⊢ φ ∧ A ∈ D I B → D ∈ C I A
24 simpr ⊢ φ ∧ A ∈ D I B → A ∈ D I B
25 1 11 2 12 13 14 16 15 21 23 24 tgbtwnouttr ⊢ φ ∧ A ∈ D I B → D ∈ C I B
26 1 11 2 12 13 14 15 25 tgbtwncom ⊢ φ ∧ A ∈ D I B → D ∈ B I C
27 7 adantr ⊢ φ ∧ B ∈ D I A → G ∈ 𝒢 Tarski
28 4 adantr ⊢ φ ∧ B ∈ D I A → A ∈ P
29 5 adantr ⊢ φ ∧ B ∈ D I A → B ∈ P
30 8 adantr ⊢ φ ∧ B ∈ D I A → D ∈ P
31 6 adantr ⊢ φ ∧ B ∈ D I A → C ∈ P
32 simpr ⊢ φ ∧ B ∈ D I A → B ∈ D I A
33 1 11 2 27 30 29 28 32 tgbtwncom ⊢ φ ∧ B ∈ D I A → B ∈ A I D
34 10 adantr ⊢ φ ∧ B ∈ D I A → D ∈ A I C
35 1 11 2 27 28 29 30 31 33 34 tgbtwnexch3 ⊢ φ ∧ B ∈ D I A → D ∈ B I C
36 18 simp3d ⊢ φ → A ∈ D I B ∨ B ∈ D I A
37 26 35 36 mpjaodan ⊢ φ → D ∈ B I C