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 φ G 𝒢 Tarski
tgbtwnconn.a φ A P
tgbtwnconn.b φ B P
tgbtwnconn.c φ C P
tgbtwnconn.d φ D P
tgbtwnconnln1.l L = Line 𝒢 G
tgbtwnconnln1.1 φ A B
tgbtwnconnln1.2 φ B A I C
tgbtwnconnln1.3 φ B A I D
Assertion tgbtwnconnln1 φ A 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 φ G 𝒢 Tarski
4 tgbtwnconn.a φ A P
5 tgbtwnconn.b φ B P
6 tgbtwnconn.c φ C P
7 tgbtwnconn.d φ D P
8 tgbtwnconnln1.l L = Line 𝒢 G
9 tgbtwnconnln1.1 φ A B
10 tgbtwnconnln1.2 φ B A I C
11 tgbtwnconnln1.3 φ B A I D
12 3 adantr φ C A I D G 𝒢 Tarski
13 6 adantr φ C A I D C P
14 7 adantr φ C A I D D P
15 4 adantr φ C A I D A P
16 simpr φ C A I D C A I D
17 1 8 2 12 13 14 15 16 btwncolg2 φ C A I D A C L D C = D
18 3 adantr φ D A I C G 𝒢 Tarski
19 6 adantr φ D A I C C P
20 7 adantr φ D A I C D P
21 4 adantr φ D A I C A P
22 eqid dist G = dist G
23 simpr φ D A I C D A I C
24 1 22 2 18 21 20 19 23 tgbtwncom φ D A I C D C I A
25 1 8 2 18 19 20 21 24 btwncolg3 φ D A I C A C L D C = D
26 1 2 3 4 5 6 7 9 10 11 tgbtwnconn1 φ C A I D D A I C
27 17 25 26 mpjaodan φ A C L D C = D