Metamath Proof Explorer


Theorem coltr3

Description: A transitivity law for colinearity. (Contributed by Thierry Arnoux, 27-Nov-2019)

Ref Expression
Hypotheses tglineintmo.p P=BaseG
tglineintmo.i I=ItvG
tglineintmo.l L=Line𝒢G
tglineintmo.g φG𝒢Tarski
coltr.a φAP
coltr.b φBP
coltr.c φCP
coltr.d φDP
coltr.1 φABLC
coltr3.2 φDAIC
Assertion coltr3 φDBLC

Proof

Step Hyp Ref Expression
1 tglineintmo.p P=BaseG
2 tglineintmo.i I=ItvG
3 tglineintmo.l L=Line𝒢G
4 tglineintmo.g φG𝒢Tarski
5 coltr.a φAP
6 coltr.b φBP
7 coltr.c φCP
8 coltr.d φDP
9 coltr.1 φABLC
10 coltr3.2 φDAIC
11 eqid distG=distG
12 4 adantr φA=CG𝒢Tarski
13 5 adantr φA=CAP
14 8 adantr φA=CDP
15 10 adantr φA=CDAIC
16 simpr φA=CA=C
17 16 oveq2d φA=CAIA=AIC
18 15 17 eleqtrrd φA=CDAIA
19 1 11 2 12 13 14 18 axtgbtwnid φA=CA=D
20 9 adantr φA=CABLC
21 19 20 eqeltrrd φA=CDBLC
22 4 adantr φACG𝒢Tarski
23 5 adantr φACAP
24 7 adantr φACCP
25 8 adantr φACDP
26 simpr φACAC
27 10 adantr φACDAIC
28 1 2 3 22 23 24 25 26 27 btwnlng1 φACDALC
29 26 necomd φACCA
30 6 adantr φACBP
31 1 3 2 4 6 7 9 tglngne φBC
32 31 adantr φACBC
33 9 adantr φACABLC
34 1 2 3 22 24 23 30 29 33 32 lnrot1 φACBCLA
35 1 2 3 22 24 23 29 30 32 34 tglineelsb2 φACCLA=CLB
36 1 2 3 22 23 24 26 tglinecom φACALC=CLA
37 1 2 3 4 6 7 31 tglinecom φBLC=CLB
38 37 adantr φACBLC=CLB
39 35 36 38 3eqtr4d φACALC=BLC
40 28 39 eleqtrd φACDBLC
41 21 40 pm2.61dane φDBLC