Metamath Proof Explorer


Theorem tgbtwnconnln1

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 tgbtwnconnln1
|- ( ph -> ( A 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. ( A I D ) ) -> G e. TarskiG )
13 6 adantr
 |-  ( ( ph /\ C e. ( A I D ) ) -> C e. P )
14 7 adantr
 |-  ( ( ph /\ C e. ( A I D ) ) -> D e. P )
15 4 adantr
 |-  ( ( ph /\ C e. ( A I D ) ) -> A e. P )
16 simpr
 |-  ( ( ph /\ C e. ( A I D ) ) -> C e. ( A I D ) )
17 1 8 2 12 13 14 15 16 btwncolg2
 |-  ( ( ph /\ C e. ( A I D ) ) -> ( A e. ( C L D ) \/ C = D ) )
18 3 adantr
 |-  ( ( ph /\ D e. ( A I C ) ) -> G e. TarskiG )
19 6 adantr
 |-  ( ( ph /\ D e. ( A I C ) ) -> C e. P )
20 7 adantr
 |-  ( ( ph /\ D e. ( A I C ) ) -> D e. P )
21 4 adantr
 |-  ( ( ph /\ D e. ( A I C ) ) -> A e. P )
22 eqid
 |-  ( dist ` G ) = ( dist ` G )
23 simpr
 |-  ( ( ph /\ D e. ( A I C ) ) -> D e. ( A I C ) )
24 1 22 2 18 21 20 19 23 tgbtwncom
 |-  ( ( ph /\ D e. ( A I C ) ) -> D e. ( C I A ) )
25 1 8 2 18 19 20 21 24 btwncolg3
 |-  ( ( ph /\ D e. ( A I C ) ) -> ( A e. ( C L D ) \/ C = D ) )
26 1 2 3 4 5 6 7 9 10 11 tgbtwnconn1
 |-  ( ph -> ( C e. ( A I D ) \/ D e. ( A I C ) ) )
27 17 25 26 mpjaodan
 |-  ( ph -> ( A e. ( C L D ) \/ C = D ) )