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 = ( hlG ` G )
ishlg.a 
|- ( ph -> A e. P )
ishlg.b 
|- ( ph -> B e. P )
ishlg.c 
|- ( ph -> C e. P )
hlln.1 
|- ( ph -> G e. TarskiG )
hltr.d 
|- ( ph -> D e. P )
hltr.1 
|- ( ph -> A ( K ` D ) B )
hltr.2 
|- ( ph -> B ( K ` D ) C )
Assertion hltr 
|- ( ph -> 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 = ( hlG ` G )
4 ishlg.a 
 |-  ( ph -> A e. P )
5 ishlg.b 
 |-  ( ph -> B e. P )
6 ishlg.c 
 |-  ( ph -> C e. P )
7 hlln.1 
 |-  ( ph -> G e. TarskiG )
8 hltr.d 
 |-  ( ph -> D e. P )
9 hltr.1 
 |-  ( ph -> A ( K ` D ) B )
10 hltr.2 
 |-  ( ph -> B ( K ` D ) C )
11 1 2 3 4 5 8 7 9 hlne1 
 |-  ( ph -> A =/= D )
12 1 2 3 5 6 8 7 10 hlne2 
 |-  ( ph -> C =/= D )
13 eqid 
 |-  ( dist ` G ) = ( dist ` G )
14 7 ad2antrr 
 |-  ( ( ( ph /\ A e. ( D I B ) ) /\ B e. ( D I C ) ) -> G e. TarskiG )
15 8 ad2antrr 
 |-  ( ( ( ph /\ A e. ( D I B ) ) /\ B e. ( D I C ) ) -> D e. P )
16 4 ad2antrr 
 |-  ( ( ( ph /\ A e. ( D I B ) ) /\ B e. ( D I C ) ) -> A e. P )
17 5 ad2antrr 
 |-  ( ( ( ph /\ A e. ( D I B ) ) /\ B e. ( D I C ) ) -> B e. P )
18 6 ad2antrr 
 |-  ( ( ( ph /\ A e. ( D I B ) ) /\ B e. ( D I C ) ) -> C e. P )
19 simplr 
 |-  ( ( ( ph /\ A e. ( D I B ) ) /\ B e. ( D I C ) ) -> A e. ( D I B ) )
20 simpr 
 |-  ( ( ( ph /\ A e. ( D I B ) ) /\ B e. ( D I C ) ) -> B e. ( D I C ) )
21 1 13 2 14 15 16 17 18 19 20 tgbtwnexch 
 |-  ( ( ( ph /\ A e. ( D I B ) ) /\ B e. ( D I C ) ) -> A e. ( D I C ) )
22 21 orcd 
 |-  ( ( ( ph /\ A e. ( D I B ) ) /\ B e. ( D I C ) ) -> ( A e. ( D I C ) \/ C e. ( D I A ) ) )
23 7 ad2antrr 
 |-  ( ( ( ph /\ A e. ( D I B ) ) /\ C e. ( D I B ) ) -> G e. TarskiG )
24 8 ad2antrr 
 |-  ( ( ( ph /\ A e. ( D I B ) ) /\ C e. ( D I B ) ) -> D e. P )
25 4 ad2antrr 
 |-  ( ( ( ph /\ A e. ( D I B ) ) /\ C e. ( D I B ) ) -> A e. P )
26 6 ad2antrr 
 |-  ( ( ( ph /\ A e. ( D I B ) ) /\ C e. ( D I B ) ) -> C e. P )
27 5 ad2antrr 
 |-  ( ( ( ph /\ A e. ( D I B ) ) /\ C e. ( D I B ) ) -> B e. P )
28 simplr 
 |-  ( ( ( ph /\ A e. ( D I B ) ) /\ C e. ( D I B ) ) -> A e. ( D I B ) )
29 simpr 
 |-  ( ( ( ph /\ A e. ( D I B ) ) /\ C e. ( D I B ) ) -> C e. ( D I B ) )
30 1 2 23 24 25 26 27 28 29 tgbtwnconn3 
 |-  ( ( ( ph /\ A e. ( D I B ) ) /\ C e. ( D I B ) ) -> ( A e. ( D I C ) \/ C e. ( D I A ) ) )
31 1 2 3 5 6 8 7 ishlg 
 |-  ( ph -> ( B ( K ` D ) C <-> ( B =/= D /\ C =/= D /\ ( B e. ( D I C ) \/ C e. ( D I B ) ) ) ) )
32 10 31 mpbid 
 |-  ( ph -> ( B =/= D /\ C =/= D /\ ( B e. ( D I C ) \/ C e. ( D I B ) ) ) )
33 32 simp3d 
 |-  ( ph -> ( B e. ( D I C ) \/ C e. ( D I B ) ) )
34 33 adantr 
 |-  ( ( ph /\ A e. ( D I B ) ) -> ( B e. ( D I C ) \/ C e. ( D I B ) ) )
35 22 30 34 mpjaodan 
 |-  ( ( ph /\ A e. ( D I B ) ) -> ( A e. ( D I C ) \/ C e. ( D I A ) ) )
36 7 ad2antrr 
 |-  ( ( ( ph /\ B e. ( D I A ) ) /\ B e. ( D I C ) ) -> G e. TarskiG )
37 8 ad2antrr 
 |-  ( ( ( ph /\ B e. ( D I A ) ) /\ B e. ( D I C ) ) -> D e. P )
38 5 ad2antrr 
 |-  ( ( ( ph /\ B e. ( D I A ) ) /\ B e. ( D I C ) ) -> B e. P )
39 4 ad2antrr 
 |-  ( ( ( ph /\ B e. ( D I A ) ) /\ B e. ( D I C ) ) -> A e. P )
40 6 ad2antrr 
 |-  ( ( ( ph /\ B e. ( D I A ) ) /\ B e. ( D I C ) ) -> C e. P )
41 32 simp1d 
 |-  ( ph -> B =/= D )
42 41 necomd 
 |-  ( ph -> D =/= B )
43 42 ad2antrr 
 |-  ( ( ( ph /\ B e. ( D I A ) ) /\ B e. ( D I C ) ) -> D =/= B )
44 simplr 
 |-  ( ( ( ph /\ B e. ( D I A ) ) /\ B e. ( D I C ) ) -> B e. ( D I A ) )
45 simpr 
 |-  ( ( ( ph /\ B e. ( D I A ) ) /\ B e. ( D I C ) ) -> B e. ( D I C ) )
46 1 2 36 37 38 39 40 43 44 45 tgbtwnconn1 
 |-  ( ( ( ph /\ B e. ( D I A ) ) /\ B e. ( D I C ) ) -> ( A e. ( D I C ) \/ C e. ( D I A ) ) )
47 7 ad2antrr 
 |-  ( ( ( ph /\ B e. ( D I A ) ) /\ C e. ( D I B ) ) -> G e. TarskiG )
48 8 ad2antrr 
 |-  ( ( ( ph /\ B e. ( D I A ) ) /\ C e. ( D I B ) ) -> D e. P )
49 6 ad2antrr 
 |-  ( ( ( ph /\ B e. ( D I A ) ) /\ C e. ( D I B ) ) -> C e. P )
50 5 ad2antrr 
 |-  ( ( ( ph /\ B e. ( D I A ) ) /\ C e. ( D I B ) ) -> B e. P )
51 4 ad2antrr 
 |-  ( ( ( ph /\ B e. ( D I A ) ) /\ C e. ( D I B ) ) -> A e. P )
52 simpr 
 |-  ( ( ( ph /\ B e. ( D I A ) ) /\ C e. ( D I B ) ) -> C e. ( D I B ) )
53 simplr 
 |-  ( ( ( ph /\ B e. ( D I A ) ) /\ C e. ( D I B ) ) -> B e. ( D I A ) )
54 1 13 2 47 48 49 50 51 52 53 tgbtwnexch 
 |-  ( ( ( ph /\ B e. ( D I A ) ) /\ C e. ( D I B ) ) -> C e. ( D I A ) )
55 54 olcd 
 |-  ( ( ( ph /\ B e. ( D I A ) ) /\ C e. ( D I B ) ) -> ( A e. ( D I C ) \/ C e. ( D I A ) ) )
56 33 adantr 
 |-  ( ( ph /\ B e. ( D I A ) ) -> ( B e. ( D I C ) \/ C e. ( D I B ) ) )
57 46 55 56 mpjaodan 
 |-  ( ( ph /\ B e. ( D I A ) ) -> ( A e. ( D I C ) \/ C e. ( D I A ) ) )
58 1 2 3 4 5 8 7 ishlg 
 |-  ( ph -> ( A ( K ` D ) B <-> ( A =/= D /\ B =/= D /\ ( A e. ( D I B ) \/ B e. ( D I A ) ) ) ) )
59 9 58 mpbid 
 |-  ( ph -> ( A =/= D /\ B =/= D /\ ( A e. ( D I B ) \/ B e. ( D I A ) ) ) )
60 59 simp3d 
 |-  ( ph -> ( A e. ( D I B ) \/ B e. ( D I A ) ) )
61 35 57 60 mpjaodan 
 |-  ( ph -> ( A e. ( D I C ) \/ C e. ( D I A ) ) )
62 1 2 3 4 6 8 7 ishlg 
 |-  ( ph -> ( A ( K ` D ) C <-> ( A =/= D /\ C =/= D /\ ( A e. ( D I C ) \/ C e. ( D I A ) ) ) ) )
63 11 12 61 62 mpbir3and 
 |-  ( ph -> A ( K ` D ) C )