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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
ishlg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
ishlg.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
ishlg.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
ishlg.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
ishlg.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
hlln.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
hltr.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
hltr.1 ⊢ ( 𝜑 → 𝐴 ( 𝐾 ‘ 𝐷 ) 𝐵 )
hltr.2 ⊢ ( 𝜑 → 𝐵 ( 𝐾 ‘ 𝐷 ) 𝐶 )
Assertion hltr ( 𝜑 → 𝐴 ( 𝐾 ‘ 𝐷 ) 𝐶 )

Proof

Step Hyp Ref Expression
1 ishlg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 ishlg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 ishlg.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 ishlg.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
5 ishlg.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
6 ishlg.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
7 hlln.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8 hltr.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9 hltr.1 ⊢ ( 𝜑 → 𝐴 ( 𝐾 ‘ 𝐷 ) 𝐵 )
10 hltr.2 ⊢ ( 𝜑 → 𝐵 ( 𝐾 ‘ 𝐷 ) 𝐶 )
11 1 2 3 4 5 8 7 9 hlne1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐷 )
12 1 2 3 5 6 8 7 10 hlne2 ⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )
13 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
14 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ) → 𝐺 ∈ TarskiG )
15 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ) → 𝐷 ∈ 𝑃 )
16 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ) → 𝐴 ∈ 𝑃 )
17 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ) → 𝐵 ∈ 𝑃 )
18 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ) → 𝐶 ∈ 𝑃 )
19 simplr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ) → 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) )
20 simpr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ) → 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) )
21 1 13 2 14 15 16 17 18 19 20 tgbtwnexch ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ) → 𝐴 ∈ ( 𝐷 𝐼 𝐶 ) )
22 21 orcd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ) → ( 𝐴 ∈ ( 𝐷 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐷 𝐼 𝐴 ) ) )
23 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐺 ∈ TarskiG )
24 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐷 ∈ 𝑃 )
25 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐴 ∈ 𝑃 )
26 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐶 ∈ 𝑃 )
27 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐵 ∈ 𝑃 )
28 simplr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) )
29 simpr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) )
30 1 2 23 24 25 26 27 28 29 tgbtwnconn3 ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) → ( 𝐴 ∈ ( 𝐷 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐷 𝐼 𝐴 ) ) )
31 1 2 3 5 6 8 7 ishlg ⊢ ( 𝜑 → ( 𝐵 ( 𝐾 ‘ 𝐷 ) 𝐶 ↔ ( 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ∧ ( 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) ) ) )
32 10 31 mpbid ⊢ ( 𝜑 → ( 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ∧ ( 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) ) )
33 32 simp3d ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) → ( 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) )
35 22 30 34 mpjaodan ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ) → ( 𝐴 ∈ ( 𝐷 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐷 𝐼 𝐴 ) ) )
36 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ) → 𝐺 ∈ TarskiG )
37 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ) → 𝐷 ∈ 𝑃 )
38 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ) → 𝐵 ∈ 𝑃 )
39 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ) → 𝐴 ∈ 𝑃 )
40 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ) → 𝐶 ∈ 𝑃 )
41 32 simp1d ⊢ ( 𝜑 → 𝐵 ≠ 𝐷 )
42 41 necomd ⊢ ( 𝜑 → 𝐷 ≠ 𝐵 )
43 42 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ) → 𝐷 ≠ 𝐵 )
44 simplr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ) → 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) )
45 simpr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ) → 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) )
46 1 2 36 37 38 39 40 43 44 45 tgbtwnconn1 ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ) → ( 𝐴 ∈ ( 𝐷 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐷 𝐼 𝐴 ) ) )
47 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐺 ∈ TarskiG )
48 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐷 ∈ 𝑃 )
49 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐶 ∈ 𝑃 )
50 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐵 ∈ 𝑃 )
51 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐴 ∈ 𝑃 )
52 simpr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) )
53 simplr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) )
54 1 13 2 47 48 49 50 51 52 53 tgbtwnexch ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) → 𝐶 ∈ ( 𝐷 𝐼 𝐴 ) )
55 54 olcd ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ∧ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) → ( 𝐴 ∈ ( 𝐷 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐷 𝐼 𝐴 ) ) )
56 33 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) → ( 𝐵 ∈ ( 𝐷 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) ) )
57 46 55 56 mpjaodan ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) → ( 𝐴 ∈ ( 𝐷 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐷 𝐼 𝐴 ) ) )
58 1 2 3 4 5 8 7 ishlg ⊢ ( 𝜑 → ( 𝐴 ( 𝐾 ‘ 𝐷 ) 𝐵 ↔ ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ) ) )
59 9 58 mpbid ⊢ ( 𝜑 → ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) ) )
60 59 simp3d ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐷 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐷 𝐼 𝐴 ) ) )
61 35 57 60 mpjaodan ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐷 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐷 𝐼 𝐴 ) ) )
62 1 2 3 4 6 8 7 ishlg ⊢ ( 𝜑 → ( 𝐴 ( 𝐾 ‘ 𝐷 ) 𝐶 ↔ ( 𝐴 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐷 𝐼 𝐴 ) ) ) ) )
63 11 12 61 62 mpbir3and ⊢ ( 𝜑 → 𝐴 ( 𝐾 ‘ 𝐷 ) 𝐶 )