Metamath Proof Explorer

Theorem hltr

Description: The half-line relation is transitive. Theorem 6.7 of Schwabhauser p. 44. (Contributed by Thierry Arnoux, 23-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
hltr.d ⊢ φ → D ∈ P
hltr.1 ⊢ φ → A K ⁡ D B
hltr.2 ⊢ φ → B K ⁡ D C
Assertion hltr ⊢ φ → A K ⁡ D 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 hltr.1 ⊢ φ → A K ⁡ D B
10 hltr.2 ⊢ φ → B K ⁡ D C
11 1 2 3 4 5 8 7 9 hlne1 ⊢ φ → A ≠ D
12 1 2 3 5 6 8 7 10 hlne2 ⊢ φ → C ≠ D
13 eqid ⊢ dist ⁡ G = dist ⁡ G
14 7 ad2antrr ⊢ φ ∧ A ∈ D I B ∧ B ∈ D I C → G ∈ 𝒢 Tarski
15 8 ad2antrr ⊢ φ ∧ A ∈ D I B ∧ B ∈ D I C → D ∈ P
16 4 ad2antrr ⊢ φ ∧ A ∈ D I B ∧ B ∈ D I C → A ∈ P
17 5 ad2antrr ⊢ φ ∧ A ∈ D I B ∧ B ∈ D I C → B ∈ P
18 6 ad2antrr ⊢ φ ∧ A ∈ D I B ∧ B ∈ D I C → C ∈ P
19 simplr ⊢ φ ∧ A ∈ D I B ∧ B ∈ D I C → A ∈ D I B
20 simpr ⊢ φ ∧ A ∈ D I B ∧ B ∈ D I C → B ∈ D I C
21 1 13 2 14 15 16 17 18 19 20 tgbtwnexch ⊢ φ ∧ A ∈ D I B ∧ B ∈ D I C → A ∈ D I C
22 21 orcd ⊢ φ ∧ A ∈ D I B ∧ B ∈ D I C → A ∈ D I C ∨ C ∈ D I A
23 7 ad2antrr ⊢ φ ∧ A ∈ D I B ∧ C ∈ D I B → G ∈ 𝒢 Tarski
24 8 ad2antrr ⊢ φ ∧ A ∈ D I B ∧ C ∈ D I B → D ∈ P
25 4 ad2antrr ⊢ φ ∧ A ∈ D I B ∧ C ∈ D I B → A ∈ P
26 6 ad2antrr ⊢ φ ∧ A ∈ D I B ∧ C ∈ D I B → C ∈ P
27 5 ad2antrr ⊢ φ ∧ A ∈ D I B ∧ C ∈ D I B → B ∈ P
28 simplr ⊢ φ ∧ A ∈ D I B ∧ C ∈ D I B → A ∈ D I B
29 simpr ⊢ φ ∧ A ∈ D I B ∧ C ∈ D I B → C ∈ D I B
30 1 2 23 24 25 26 27 28 29 tgbtwnconn3 ⊢ φ ∧ A ∈ D I B ∧ C ∈ D I B → A ∈ D I C ∨ C ∈ D I A
31 1 2 3 5 6 8 7 ishlg ⊢ φ → B K ⁡ D C ↔ B ≠ D ∧ C ≠ D ∧ B ∈ D I C ∨ C ∈ D I B
32 10 31 mpbid ⊢ φ → B ≠ D ∧ C ≠ D ∧ B ∈ D I C ∨ C ∈ D I B
33 32 simp3d ⊢ φ → B ∈ D I C ∨ C ∈ D I B
34 33 adantr ⊢ φ ∧ A ∈ D I B → B ∈ D I C ∨ C ∈ D I B
35 22 30 34 mpjaodan ⊢ φ ∧ A ∈ D I B → A ∈ D I C ∨ C ∈ D I A
36 7 ad2antrr ⊢ φ ∧ B ∈ D I A ∧ B ∈ D I C → G ∈ 𝒢 Tarski
37 8 ad2antrr ⊢ φ ∧ B ∈ D I A ∧ B ∈ D I C → D ∈ P
38 5 ad2antrr ⊢ φ ∧ B ∈ D I A ∧ B ∈ D I C → B ∈ P
39 4 ad2antrr ⊢ φ ∧ B ∈ D I A ∧ B ∈ D I C → A ∈ P
40 6 ad2antrr ⊢ φ ∧ B ∈ D I A ∧ B ∈ D I C → C ∈ P
41 32 simp1d ⊢ φ → B ≠ D
42 41 necomd ⊢ φ → D ≠ B
43 42 ad2antrr ⊢ φ ∧ B ∈ D I A ∧ B ∈ D I C → D ≠ B
44 simplr ⊢ φ ∧ B ∈ D I A ∧ B ∈ D I C → B ∈ D I A
45 simpr ⊢ φ ∧ B ∈ D I A ∧ B ∈ D I C → B ∈ D I C
46 1 2 36 37 38 39 40 43 44 45 tgbtwnconn1 ⊢ φ ∧ B ∈ D I A ∧ B ∈ D I C → A ∈ D I C ∨ C ∈ D I A
47 7 ad2antrr ⊢ φ ∧ B ∈ D I A ∧ C ∈ D I B → G ∈ 𝒢 Tarski
48 8 ad2antrr ⊢ φ ∧ B ∈ D I A ∧ C ∈ D I B → D ∈ P
49 6 ad2antrr ⊢ φ ∧ B ∈ D I A ∧ C ∈ D I B → C ∈ P
50 5 ad2antrr ⊢ φ ∧ B ∈ D I A ∧ C ∈ D I B → B ∈ P
51 4 ad2antrr ⊢ φ ∧ B ∈ D I A ∧ C ∈ D I B → A ∈ P
52 simpr ⊢ φ ∧ B ∈ D I A ∧ C ∈ D I B → C ∈ D I B
53 simplr ⊢ φ ∧ B ∈ D I A ∧ C ∈ D I B → B ∈ D I A
54 1 13 2 47 48 49 50 51 52 53 tgbtwnexch ⊢ φ ∧ B ∈ D I A ∧ C ∈ D I B → C ∈ D I A
55 54 olcd ⊢ φ ∧ B ∈ D I A ∧ C ∈ D I B → A ∈ D I C ∨ C ∈ D I A
56 33 adantr ⊢ φ ∧ B ∈ D I A → B ∈ D I C ∨ C ∈ D I B
57 46 55 56 mpjaodan ⊢ φ ∧ B ∈ D I A → A ∈ D I C ∨ C ∈ D I A
58 1 2 3 4 5 8 7 ishlg ⊢ φ → A K ⁡ D B ↔ A ≠ D ∧ B ≠ D ∧ A ∈ D I B ∨ B ∈ D I A
59 9 58 mpbid ⊢ φ → A ≠ D ∧ B ≠ D ∧ A ∈ D I B ∨ B ∈ D I A
60 59 simp3d ⊢ φ → A ∈ D I B ∨ B ∈ D I A
61 35 57 60 mpjaodan ⊢ φ → A ∈ D I C ∨ C ∈ D I A
62 1 2 3 4 6 8 7 ishlg ⊢ φ → A K ⁡ D C ↔ A ≠ D ∧ C ≠ D ∧ A ∈ D I C ∨ C ∈ D I A
63 11 12 61 62 mpbir3and ⊢ φ → A K ⁡ D C