Metamath Proof Explorer


Theorem tgbtwnconnln3

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

Ref Expression
Hypotheses tgbtwnconn.p P=BaseG
tgbtwnconn.i I=ItvG
tgbtwnconn.g φG𝒢Tarski
tgbtwnconn.a φAP
tgbtwnconn.b φBP
tgbtwnconn.c φCP
tgbtwnconn.d φDP
tgbtwnconn3.1 φBAID
tgbtwnconn3.2 φCAID
tgbtwnconnln3.l L=Line𝒢G
Assertion tgbtwnconnln3 φBALCA=C

Proof

Step Hyp Ref Expression
1 tgbtwnconn.p P=BaseG
2 tgbtwnconn.i I=ItvG
3 tgbtwnconn.g φG𝒢Tarski
4 tgbtwnconn.a φAP
5 tgbtwnconn.b φBP
6 tgbtwnconn.c φCP
7 tgbtwnconn.d φDP
8 tgbtwnconn3.1 φBAID
9 tgbtwnconn3.2 φCAID
10 tgbtwnconnln3.l L=Line𝒢G
11 3 adantr φBAICG𝒢Tarski
12 4 adantr φBAICAP
13 6 adantr φBAICCP
14 5 adantr φBAICBP
15 simpr φBAICBAIC
16 1 10 2 11 12 13 14 15 btwncolg1 φBAICBALCA=C
17 3 adantr φCAIBG𝒢Tarski
18 4 adantr φCAIBAP
19 6 adantr φCAIBCP
20 5 adantr φCAIBBP
21 simpr φCAIBCAIB
22 1 10 2 17 18 19 20 21 btwncolg3 φCAIBBALCA=C
23 1 2 3 4 5 6 7 8 9 tgbtwnconn3 φBAICCAIB
24 16 22 23 mpjaodan φBALCA=C