Metamath Proof Explorer

Theorem hlbtwn

Description: Betweenness is a sufficient condition to swap half-lines. (Contributed by Thierry Arnoux, 21-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 )
hlbtwn.1 
|- ( ph -> D e. ( C I B ) )
hlbtwn.2 
|- ( ph -> B =/= C )
hlbtwn.3 
|- ( ph -> D =/= C )
Assertion hlbtwn 
|- ( ph -> ( A ( K ` C ) B <-> A ( K ` C ) D ) )

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 hlbtwn.1 
 |-  ( ph -> D e. ( C I B ) )
10 hlbtwn.2 
 |-  ( ph -> B =/= C )
11 hlbtwn.3 
 |-  ( ph -> D =/= C )
12 10 11 2thd 
 |-  ( ph -> ( B =/= C <-> D =/= C ) )
13 7 adantr 
 |-  ( ( ph /\ A e. ( C I B ) ) -> G e. TarskiG )
14 6 adantr 
 |-  ( ( ph /\ A e. ( C I B ) ) -> C e. P )
15 4 adantr 
 |-  ( ( ph /\ A e. ( C I B ) ) -> A e. P )
16 8 adantr 
 |-  ( ( ph /\ A e. ( C I B ) ) -> D e. P )
17 5 adantr 
 |-  ( ( ph /\ A e. ( C I B ) ) -> B e. P )
18 simpr 
 |-  ( ( ph /\ A e. ( C I B ) ) -> A e. ( C I B ) )
19 9 adantr 
 |-  ( ( ph /\ A e. ( C I B ) ) -> D e. ( C I B ) )
20 1 2 13 14 15 16 17 18 19 tgbtwnconn3 
 |-  ( ( ph /\ A e. ( C I B ) ) -> ( A e. ( C I D ) \/ D e. ( C I A ) ) )
21 eqid 
 |-  ( dist ` G ) = ( dist ` G )
22 7 adantr 
 |-  ( ( ph /\ B e. ( C I A ) ) -> G e. TarskiG )
23 6 adantr 
 |-  ( ( ph /\ B e. ( C I A ) ) -> C e. P )
24 8 adantr 
 |-  ( ( ph /\ B e. ( C I A ) ) -> D e. P )
25 5 adantr 
 |-  ( ( ph /\ B e. ( C I A ) ) -> B e. P )
26 4 adantr 
 |-  ( ( ph /\ B e. ( C I A ) ) -> A e. P )
27 9 adantr 
 |-  ( ( ph /\ B e. ( C I A ) ) -> D e. ( C I B ) )
28 simpr 
 |-  ( ( ph /\ B e. ( C I A ) ) -> B e. ( C I A ) )
29 1 21 2 22 23 24 25 26 27 28 tgbtwnexch 
 |-  ( ( ph /\ B e. ( C I A ) ) -> D e. ( C I A ) )
30 29 olcd 
 |-  ( ( ph /\ B e. ( C I A ) ) -> ( A e. ( C I D ) \/ D e. ( C I A ) ) )
31 20 30 jaodan 
 |-  ( ( ph /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) -> ( A e. ( C I D ) \/ D e. ( C I A ) ) )
32 7 adantr 
 |-  ( ( ph /\ A e. ( C I D ) ) -> G e. TarskiG )
33 6 adantr 
 |-  ( ( ph /\ A e. ( C I D ) ) -> C e. P )
34 4 adantr 
 |-  ( ( ph /\ A e. ( C I D ) ) -> A e. P )
35 8 adantr 
 |-  ( ( ph /\ A e. ( C I D ) ) -> D e. P )
36 5 adantr 
 |-  ( ( ph /\ A e. ( C I D ) ) -> B e. P )
37 simpr 
 |-  ( ( ph /\ A e. ( C I D ) ) -> A e. ( C I D ) )
38 9 adantr 
 |-  ( ( ph /\ A e. ( C I D ) ) -> D e. ( C I B ) )
39 1 21 2 32 33 34 35 36 37 38 tgbtwnexch 
 |-  ( ( ph /\ A e. ( C I D ) ) -> A e. ( C I B ) )
40 39 orcd 
 |-  ( ( ph /\ A e. ( C I D ) ) -> ( A e. ( C I B ) \/ B e. ( C I A ) ) )
41 7 adantr 
 |-  ( ( ph /\ D e. ( C I A ) ) -> G e. TarskiG )
42 6 adantr 
 |-  ( ( ph /\ D e. ( C I A ) ) -> C e. P )
43 8 adantr 
 |-  ( ( ph /\ D e. ( C I A ) ) -> D e. P )
44 4 adantr 
 |-  ( ( ph /\ D e. ( C I A ) ) -> A e. P )
45 5 adantr 
 |-  ( ( ph /\ D e. ( C I A ) ) -> B e. P )
46 11 necomd 
 |-  ( ph -> C =/= D )
47 46 adantr 
 |-  ( ( ph /\ D e. ( C I A ) ) -> C =/= D )
48 simpr 
 |-  ( ( ph /\ D e. ( C I A ) ) -> D e. ( C I A ) )
49 9 adantr 
 |-  ( ( ph /\ D e. ( C I A ) ) -> D e. ( C I B ) )
50 1 2 41 42 43 44 45 47 48 49 tgbtwnconn1 
 |-  ( ( ph /\ D e. ( C I A ) ) -> ( A e. ( C I B ) \/ B e. ( C I A ) ) )
51 40 50 jaodan 
 |-  ( ( ph /\ ( A e. ( C I D ) \/ D e. ( C I A ) ) ) -> ( A e. ( C I B ) \/ B e. ( C I A ) ) )
52 31 51 impbida 
 |-  ( ph -> ( ( A e. ( C I B ) \/ B e. ( C I A ) ) <-> ( A e. ( C I D ) \/ D e. ( C I A ) ) ) )
53 12 52 3anbi23d 
 |-  ( ph -> ( ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) <-> ( A =/= C /\ D =/= C /\ ( A e. ( C I D ) \/ D e. ( C I A ) ) ) ) )
54 1 2 3 4 5 6 7 ishlg 
 |-  ( ph -> ( A ( K ` C ) B <-> ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) ) )
55 1 2 3 4 8 6 7 ishlg 
 |-  ( ph -> ( A ( K ` C ) D <-> ( A =/= C /\ D =/= C /\ ( A e. ( C I D ) \/ D e. ( C I A ) ) ) ) )
56 53 54 55 3bitr4d 
 |-  ( ph -> ( A ( K ` C ) B <-> A ( K ` C ) D ) )