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 = ( 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 )
btwnhl.1 
|- ( ph -> A ( K ` D ) B )
btwnhl.3 
|- ( ph -> D e. ( A I C ) )
Assertion btwnhl 
|- ( ph -> D e. ( B I 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 btwnhl.1 
 |-  ( ph -> A ( K ` D ) B )
10 btwnhl.3 
 |-  ( ph -> D e. ( A I C ) )
11 eqid 
 |-  ( dist ` G ) = ( dist ` G )
12 7 adantr 
 |-  ( ( ph /\ A e. ( D I B ) ) -> G e. TarskiG )
13 6 adantr 
 |-  ( ( ph /\ A e. ( D I B ) ) -> C e. P )
14 8 adantr 
 |-  ( ( ph /\ A e. ( D I B ) ) -> D e. P )
15 5 adantr 
 |-  ( ( ph /\ A e. ( D I B ) ) -> B e. P )
16 4 adantr 
 |-  ( ( ph /\ A e. ( D I B ) ) -> A e. P )
17 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 ) ) ) ) )
18 9 17 mpbid 
 |-  ( ph -> ( A =/= D /\ B =/= D /\ ( A e. ( D I B ) \/ B e. ( D I A ) ) ) )
19 18 simp1d 
 |-  ( ph -> A =/= D )
20 19 necomd 
 |-  ( ph -> D =/= A )
21 20 adantr 
 |-  ( ( ph /\ A e. ( D I B ) ) -> D =/= A )
22 10 adantr 
 |-  ( ( ph /\ A e. ( D I B ) ) -> D e. ( A I C ) )
23 1 11 2 12 16 14 13 22 tgbtwncom 
 |-  ( ( ph /\ A e. ( D I B ) ) -> D e. ( C I A ) )
24 simpr 
 |-  ( ( ph /\ A e. ( D I B ) ) -> A e. ( D I B ) )
25 1 11 2 12 13 14 16 15 21 23 24 tgbtwnouttr 
 |-  ( ( ph /\ A e. ( D I B ) ) -> D e. ( C I B ) )
26 1 11 2 12 13 14 15 25 tgbtwncom 
 |-  ( ( ph /\ A e. ( D I B ) ) -> D e. ( B I C ) )
27 7 adantr 
 |-  ( ( ph /\ B e. ( D I A ) ) -> G e. TarskiG )
28 4 adantr 
 |-  ( ( ph /\ B e. ( D I A ) ) -> A e. P )
29 5 adantr 
 |-  ( ( ph /\ B e. ( D I A ) ) -> B e. P )
30 8 adantr 
 |-  ( ( ph /\ B e. ( D I A ) ) -> D e. P )
31 6 adantr 
 |-  ( ( ph /\ B e. ( D I A ) ) -> C e. P )
32 simpr 
 |-  ( ( ph /\ B e. ( D I A ) ) -> B e. ( D I A ) )
33 1 11 2 27 30 29 28 32 tgbtwncom 
 |-  ( ( ph /\ B e. ( D I A ) ) -> B e. ( A I D ) )
34 10 adantr 
 |-  ( ( ph /\ B e. ( D I A ) ) -> D e. ( A I C ) )
35 1 11 2 27 28 29 30 31 33 34 tgbtwnexch3 
 |-  ( ( ph /\ B e. ( D I A ) ) -> D e. ( B I C ) )
36 18 simp3d 
 |-  ( ph -> ( A e. ( D I B ) \/ B e. ( D I A ) ) )
37 26 35 36 mpjaodan 
 |-  ( ph -> D e. ( B I C ) )