Metamath Proof Explorer

Theorem tgbtwnconnln2

Description: Derive colinearity from betweenness. (Contributed by Thierry Arnoux, 17-May-2019)

Ref Expression
Hypotheses tgbtwnconn.p 
|- P = ( Base ` G )
tgbtwnconn.i 
|- I = ( Itv ` G )
tgbtwnconn.g 
|- ( ph -> G e. TarskiG )
tgbtwnconn.a 
|- ( ph -> A e. P )
tgbtwnconn.b 
|- ( ph -> B e. P )
tgbtwnconn.c 
|- ( ph -> C e. P )
tgbtwnconn.d 
|- ( ph -> D e. P )
tgbtwnconnln1.l 
|- L = ( LineG ` G )
tgbtwnconnln1.1 
|- ( ph -> A =/= B )
tgbtwnconnln1.2 
|- ( ph -> B e. ( A I C ) )
tgbtwnconnln1.3 
|- ( ph -> B e. ( A I D ) )
Assertion tgbtwnconnln2 
|- ( ph -> ( B e. ( C L D ) \/ C = D ) )

Proof

Step Hyp Ref Expression
1 tgbtwnconn.p 
 |-  P = ( Base ` G )
2 tgbtwnconn.i 
 |-  I = ( Itv ` G )
3 tgbtwnconn.g 
 |-  ( ph -> G e. TarskiG )
4 tgbtwnconn.a 
 |-  ( ph -> A e. P )
5 tgbtwnconn.b 
 |-  ( ph -> B e. P )
6 tgbtwnconn.c 
 |-  ( ph -> C e. P )
7 tgbtwnconn.d 
 |-  ( ph -> D e. P )
8 tgbtwnconnln1.l 
 |-  L = ( LineG ` G )
9 tgbtwnconnln1.1 
 |-  ( ph -> A =/= B )
10 tgbtwnconnln1.2 
 |-  ( ph -> B e. ( A I C ) )
11 tgbtwnconnln1.3 
 |-  ( ph -> B e. ( A I D ) )
12 3 adantr 
 |-  ( ( ph /\ C e. ( B I D ) ) -> G e. TarskiG )
13 6 adantr 
 |-  ( ( ph /\ C e. ( B I D ) ) -> C e. P )
14 7 adantr 
 |-  ( ( ph /\ C e. ( B I D ) ) -> D e. P )
15 5 adantr 
 |-  ( ( ph /\ C e. ( B I D ) ) -> B e. P )
16 simpr 
 |-  ( ( ph /\ C e. ( B I D ) ) -> C e. ( B I D ) )
17 1 8 2 12 13 14 15 16 btwncolg2 
 |-  ( ( ph /\ C e. ( B I D ) ) -> ( B e. ( C L D ) \/ C = D ) )
18 3 adantr 
 |-  ( ( ph /\ D e. ( B I C ) ) -> G e. TarskiG )
19 6 adantr 
 |-  ( ( ph /\ D e. ( B I C ) ) -> C e. P )
20 7 adantr 
 |-  ( ( ph /\ D e. ( B I C ) ) -> D e. P )
21 5 adantr 
 |-  ( ( ph /\ D e. ( B I C ) ) -> B e. P )
22 eqid 
 |-  ( dist ` G ) = ( dist ` G )
23 simpr 
 |-  ( ( ph /\ D e. ( B I C ) ) -> D e. ( B I C ) )
24 1 22 2 18 21 20 19 23 tgbtwncom 
 |-  ( ( ph /\ D e. ( B I C ) ) -> D e. ( C I B ) )
25 1 8 2 18 19 20 21 24 btwncolg3 
 |-  ( ( ph /\ D e. ( B I C ) ) -> ( B e. ( C L D ) \/ C = D ) )
26 1 2 3 4 5 6 7 9 10 11 tgbtwnconn2 
 |-  ( ph -> ( C e. ( B I D ) \/ D e. ( B I C ) ) )
27 17 25 26 mpjaodan 
 |-  ( ph -> ( B e. ( C L D ) \/ C = D ) )