Metamath Proof Explorer

Theorem lnhl

Description: Either a point C on the line AB is on the same side as A or on the opposite side. (Contributed by Thierry Arnoux, 21-Sep-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 )
lnhl.l 
|- L = ( LineG ` G )
lnhl.1 
|- ( ph -> C e. ( A L B ) )
Assertion lnhl 
|- ( ph -> ( C ( K ` B ) A \/ B e. ( A 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 lnhl.l 
 |-  L = ( LineG ` G )
10 lnhl.1 
 |-  ( ph -> C e. ( A L B ) )
11 simpr 
 |-  ( ( ph /\ C = B ) -> C = B )
12 eqid 
 |-  ( dist ` G ) = ( dist ` G )
13 1 12 2 7 4 6 tgbtwntriv2 
 |-  ( ph -> C e. ( A I C ) )
14 13 adantr 
 |-  ( ( ph /\ C = B ) -> C e. ( A I C ) )
15 11 14 eqeltrrd 
 |-  ( ( ph /\ C = B ) -> B e. ( A I C ) )
16 15 olcd 
 |-  ( ( ph /\ C = B ) -> ( C ( K ` B ) A \/ B e. ( A I C ) ) )
17 1 9 2 7 4 5 10 tglngne 
 |-  ( ph -> A =/= B )
18 1 9 2 7 4 5 17 6 tgellng 
 |-  ( ph -> ( C e. ( A L B ) <-> ( C e. ( A I B ) \/ A e. ( C I B ) \/ B e. ( A I C ) ) ) )
19 10 18 mpbid 
 |-  ( ph -> ( C e. ( A I B ) \/ A e. ( C I B ) \/ B e. ( A I C ) ) )
20 df-3or 
 |-  ( ( C e. ( A I B ) \/ A e. ( C I B ) \/ B e. ( A I C ) ) <-> ( ( C e. ( A I B ) \/ A e. ( C I B ) ) \/ B e. ( A I C ) ) )
21 19 20 sylib 
 |-  ( ph -> ( ( C e. ( A I B ) \/ A e. ( C I B ) ) \/ B e. ( A I C ) ) )
22 21 adantr 
 |-  ( ( ph /\ C =/= B ) -> ( ( C e. ( A I B ) \/ A e. ( C I B ) ) \/ B e. ( A I C ) ) )
23 1 2 3 6 4 5 7 ishlg 
 |-  ( ph -> ( C ( K ` B ) A <-> ( C =/= B /\ A =/= B /\ ( C e. ( B I A ) \/ A e. ( B I C ) ) ) ) )
24 23 adantr 
 |-  ( ( ph /\ C =/= B ) -> ( C ( K ` B ) A <-> ( C =/= B /\ A =/= B /\ ( C e. ( B I A ) \/ A e. ( B I C ) ) ) ) )
25 df-3an 
 |-  ( ( C =/= B /\ A =/= B /\ ( C e. ( B I A ) \/ A e. ( B I C ) ) ) <-> ( ( C =/= B /\ A =/= B ) /\ ( C e. ( B I A ) \/ A e. ( B I C ) ) ) )
26 24 25 bitrdi 
 |-  ( ( ph /\ C =/= B ) -> ( C ( K ` B ) A <-> ( ( C =/= B /\ A =/= B ) /\ ( C e. ( B I A ) \/ A e. ( B I C ) ) ) ) )
27 17 anim1ci 
 |-  ( ( ph /\ C =/= B ) -> ( C =/= B /\ A =/= B ) )
28 27 biantrurd 
 |-  ( ( ph /\ C =/= B ) -> ( ( C e. ( B I A ) \/ A e. ( B I C ) ) <-> ( ( C =/= B /\ A =/= B ) /\ ( C e. ( B I A ) \/ A e. ( B I C ) ) ) ) )
29 7 adantr 
 |-  ( ( ph /\ C =/= B ) -> G e. TarskiG )
30 5 adantr 
 |-  ( ( ph /\ C =/= B ) -> B e. P )
31 6 adantr 
 |-  ( ( ph /\ C =/= B ) -> C e. P )
32 4 adantr 
 |-  ( ( ph /\ C =/= B ) -> A e. P )
33 1 12 2 29 30 31 32 tgbtwncomb 
 |-  ( ( ph /\ C =/= B ) -> ( C e. ( B I A ) <-> C e. ( A I B ) ) )
34 1 12 2 29 30 32 31 tgbtwncomb 
 |-  ( ( ph /\ C =/= B ) -> ( A e. ( B I C ) <-> A e. ( C I B ) ) )
35 33 34 orbi12d 
 |-  ( ( ph /\ C =/= B ) -> ( ( C e. ( B I A ) \/ A e. ( B I C ) ) <-> ( C e. ( A I B ) \/ A e. ( C I B ) ) ) )
36 26 28 35 3bitr2d 
 |-  ( ( ph /\ C =/= B ) -> ( C ( K ` B ) A <-> ( C e. ( A I B ) \/ A e. ( C I B ) ) ) )
37 36 orbi1d 
 |-  ( ( ph /\ C =/= B ) -> ( ( C ( K ` B ) A \/ B e. ( A I C ) ) <-> ( ( C e. ( A I B ) \/ A e. ( C I B ) ) \/ B e. ( A I C ) ) ) )
38 22 37 mpbird 
 |-  ( ( ph /\ C =/= B ) -> ( C ( K ` B ) A \/ B e. ( A I C ) ) )
39 16 38 pm2.61dane 
 |-  ( ph -> ( C ( K ` B ) A \/ B e. ( A I C ) ) )