# Metamath Proof Explorer

## Theorem coltr3

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

Ref Expression
Hypotheses tglineintmo.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
tglineintmo.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
tglineintmo.l ${⊢}{L}={Line}_{𝒢}\left({G}\right)$
tglineintmo.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
coltr.a ${⊢}{\phi }\to {A}\in {P}$
coltr.b ${⊢}{\phi }\to {B}\in {P}$
coltr.c ${⊢}{\phi }\to {C}\in {P}$
coltr.d ${⊢}{\phi }\to {D}\in {P}$
coltr.1 ${⊢}{\phi }\to {A}\in \left({B}{L}{C}\right)$
coltr3.2 ${⊢}{\phi }\to {D}\in \left({A}{I}{C}\right)$
Assertion coltr3 ${⊢}{\phi }\to {D}\in \left({B}{L}{C}\right)$

### Proof

Step Hyp Ref Expression
1 tglineintmo.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
2 tglineintmo.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
3 tglineintmo.l ${⊢}{L}={Line}_{𝒢}\left({G}\right)$
4 tglineintmo.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
5 coltr.a ${⊢}{\phi }\to {A}\in {P}$
6 coltr.b ${⊢}{\phi }\to {B}\in {P}$
7 coltr.c ${⊢}{\phi }\to {C}\in {P}$
8 coltr.d ${⊢}{\phi }\to {D}\in {P}$
9 coltr.1 ${⊢}{\phi }\to {A}\in \left({B}{L}{C}\right)$
10 coltr3.2 ${⊢}{\phi }\to {D}\in \left({A}{I}{C}\right)$
11 eqid ${⊢}\mathrm{dist}\left({G}\right)=\mathrm{dist}\left({G}\right)$
12 4 adantr ${⊢}\left({\phi }\wedge {A}={C}\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
13 5 adantr ${⊢}\left({\phi }\wedge {A}={C}\right)\to {A}\in {P}$
14 8 adantr ${⊢}\left({\phi }\wedge {A}={C}\right)\to {D}\in {P}$
15 10 adantr ${⊢}\left({\phi }\wedge {A}={C}\right)\to {D}\in \left({A}{I}{C}\right)$
16 simpr ${⊢}\left({\phi }\wedge {A}={C}\right)\to {A}={C}$
17 16 oveq2d ${⊢}\left({\phi }\wedge {A}={C}\right)\to {A}{I}{A}={A}{I}{C}$
18 15 17 eleqtrrd ${⊢}\left({\phi }\wedge {A}={C}\right)\to {D}\in \left({A}{I}{A}\right)$
19 1 11 2 12 13 14 18 axtgbtwnid ${⊢}\left({\phi }\wedge {A}={C}\right)\to {A}={D}$
20 9 adantr ${⊢}\left({\phi }\wedge {A}={C}\right)\to {A}\in \left({B}{L}{C}\right)$
21 19 20 eqeltrrd ${⊢}\left({\phi }\wedge {A}={C}\right)\to {D}\in \left({B}{L}{C}\right)$
22 4 adantr ${⊢}\left({\phi }\wedge {A}\ne {C}\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
23 5 adantr ${⊢}\left({\phi }\wedge {A}\ne {C}\right)\to {A}\in {P}$
24 7 adantr ${⊢}\left({\phi }\wedge {A}\ne {C}\right)\to {C}\in {P}$
25 8 adantr ${⊢}\left({\phi }\wedge {A}\ne {C}\right)\to {D}\in {P}$
26 simpr ${⊢}\left({\phi }\wedge {A}\ne {C}\right)\to {A}\ne {C}$
27 10 adantr ${⊢}\left({\phi }\wedge {A}\ne {C}\right)\to {D}\in \left({A}{I}{C}\right)$
28 1 2 3 22 23 24 25 26 27 btwnlng1 ${⊢}\left({\phi }\wedge {A}\ne {C}\right)\to {D}\in \left({A}{L}{C}\right)$
29 26 necomd ${⊢}\left({\phi }\wedge {A}\ne {C}\right)\to {C}\ne {A}$
30 6 adantr ${⊢}\left({\phi }\wedge {A}\ne {C}\right)\to {B}\in {P}$
31 1 3 2 4 6 7 9 tglngne ${⊢}{\phi }\to {B}\ne {C}$
32 31 adantr ${⊢}\left({\phi }\wedge {A}\ne {C}\right)\to {B}\ne {C}$
33 9 adantr ${⊢}\left({\phi }\wedge {A}\ne {C}\right)\to {A}\in \left({B}{L}{C}\right)$
34 1 2 3 22 24 23 30 29 33 32 lnrot1 ${⊢}\left({\phi }\wedge {A}\ne {C}\right)\to {B}\in \left({C}{L}{A}\right)$
35 1 2 3 22 24 23 29 30 32 34 tglineelsb2 ${⊢}\left({\phi }\wedge {A}\ne {C}\right)\to {C}{L}{A}={C}{L}{B}$
36 1 2 3 22 23 24 26 tglinecom ${⊢}\left({\phi }\wedge {A}\ne {C}\right)\to {A}{L}{C}={C}{L}{A}$
37 1 2 3 4 6 7 31 tglinecom ${⊢}{\phi }\to {B}{L}{C}={C}{L}{B}$
38 37 adantr ${⊢}\left({\phi }\wedge {A}\ne {C}\right)\to {B}{L}{C}={C}{L}{B}$
39 35 36 38 3eqtr4d ${⊢}\left({\phi }\wedge {A}\ne {C}\right)\to {A}{L}{C}={B}{L}{C}$
40 28 39 eleqtrd ${⊢}\left({\phi }\wedge {A}\ne {C}\right)\to {D}\in \left({B}{L}{C}\right)$
41 21 40 pm2.61dane ${⊢}{\phi }\to {D}\in \left({B}{L}{C}\right)$