Metamath Proof Explorer

Theorem hlln

Description: The half-line relation implies colinearity, part of Theorem 6.4 of Schwabhauser p. 44. (Contributed by Thierry Arnoux, 22-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 )
hlln.l 
|- L = ( LineG ` G )
hlln.2 
|- ( ph -> A ( K ` C ) B )
Assertion hlln 
|- ( ph -> A e. ( B L 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 hlln.l 
 |-  L = ( LineG ` G )
9 hlln.2 
 |-  ( ph -> A ( K ` C ) B )
10 eqid 
 |-  ( dist ` G ) = ( dist ` G )
11 7 adantr 
 |-  ( ( ph /\ A e. ( C I B ) ) -> G e. TarskiG )
12 6 adantr 
 |-  ( ( ph /\ A e. ( C I B ) ) -> C e. P )
13 4 adantr 
 |-  ( ( ph /\ A e. ( C I B ) ) -> A e. P )
14 5 adantr 
 |-  ( ( ph /\ A e. ( C I B ) ) -> B e. P )
15 simpr 
 |-  ( ( ph /\ A e. ( C I B ) ) -> A e. ( C I B ) )
16 1 10 2 11 12 13 14 15 tgbtwncom 
 |-  ( ( ph /\ A e. ( C I B ) ) -> A e. ( B I C ) )
17 16 3mix1d 
 |-  ( ( ph /\ A e. ( C I B ) ) -> ( A e. ( B I C ) \/ B e. ( A I C ) \/ C e. ( B I A ) ) )
18 7 adantr 
 |-  ( ( ph /\ B e. ( C I A ) ) -> G e. TarskiG )
19 6 adantr 
 |-  ( ( ph /\ B e. ( C I A ) ) -> C e. P )
20 5 adantr 
 |-  ( ( ph /\ B e. ( C I A ) ) -> B e. P )
21 4 adantr 
 |-  ( ( ph /\ B e. ( C I A ) ) -> A e. P )
22 simpr 
 |-  ( ( ph /\ B e. ( C I A ) ) -> B e. ( C I A ) )
23 1 10 2 18 19 20 21 22 tgbtwncom 
 |-  ( ( ph /\ B e. ( C I A ) ) -> B e. ( A I C ) )
24 23 3mix2d 
 |-  ( ( ph /\ B e. ( C I A ) ) -> ( A e. ( B I C ) \/ B e. ( A I C ) \/ C e. ( B I A ) ) )
25 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 ) ) ) ) )
26 9 25 mpbid 
 |-  ( ph -> ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) )
27 26 simp3d 
 |-  ( ph -> ( A e. ( C I B ) \/ B e. ( C I A ) ) )
28 17 24 27 mpjaodan 
 |-  ( ph -> ( A e. ( B I C ) \/ B e. ( A I C ) \/ C e. ( B I A ) ) )
29 26 simp2d 
 |-  ( ph -> B =/= C )
30 1 8 2 7 5 6 29 4 tgellng 
 |-  ( ph -> ( A e. ( B L C ) <-> ( A e. ( B I C ) \/ B e. ( A I C ) \/ C e. ( B I A ) ) ) )
31 28 30 mpbird 
 |-  ( ph -> A e. ( B L C ) )