# Metamath Proof Explorer

## Theorem ncolne1

Description: Non-colinear points are different. (Contributed by Thierry Arnoux, 8-Aug-2019)

Ref Expression
Hypotheses tglineelsb2.p ${⊢}{B}={\mathrm{Base}}_{{G}}$
tglineelsb2.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
tglineelsb2.l ${⊢}{L}={Line}_{𝒢}\left({G}\right)$
tglineelsb2.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
ncolne.x ${⊢}{\phi }\to {X}\in {B}$
ncolne.y ${⊢}{\phi }\to {Y}\in {B}$
ncolne.z ${⊢}{\phi }\to {Z}\in {B}$
ncolne.2 ${⊢}{\phi }\to ¬\left({X}\in \left({Y}{L}{Z}\right)\vee {Y}={Z}\right)$
Assertion ncolne1 ${⊢}{\phi }\to {X}\ne {Y}$

### Proof

Step Hyp Ref Expression
1 tglineelsb2.p ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 tglineelsb2.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
3 tglineelsb2.l ${⊢}{L}={Line}_{𝒢}\left({G}\right)$
4 tglineelsb2.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
5 ncolne.x ${⊢}{\phi }\to {X}\in {B}$
6 ncolne.y ${⊢}{\phi }\to {Y}\in {B}$
7 ncolne.z ${⊢}{\phi }\to {Z}\in {B}$
8 ncolne.2 ${⊢}{\phi }\to ¬\left({X}\in \left({Y}{L}{Z}\right)\vee {Y}={Z}\right)$
9 4 adantr ${⊢}\left({\phi }\wedge {X}={Y}\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
10 6 adantr ${⊢}\left({\phi }\wedge {X}={Y}\right)\to {Y}\in {B}$
11 7 adantr ${⊢}\left({\phi }\wedge {X}={Y}\right)\to {Z}\in {B}$
12 5 adantr ${⊢}\left({\phi }\wedge {X}={Y}\right)\to {X}\in {B}$
13 eqid ${⊢}\mathrm{dist}\left({G}\right)=\mathrm{dist}\left({G}\right)$
14 1 13 2 9 12 11 tgbtwntriv1 ${⊢}\left({\phi }\wedge {X}={Y}\right)\to {X}\in \left({X}{I}{Z}\right)$
15 simpr ${⊢}\left({\phi }\wedge {X}={Y}\right)\to {X}={Y}$
16 15 oveq1d ${⊢}\left({\phi }\wedge {X}={Y}\right)\to {X}{I}{Z}={Y}{I}{Z}$
17 14 16 eleqtrd ${⊢}\left({\phi }\wedge {X}={Y}\right)\to {X}\in \left({Y}{I}{Z}\right)$
18 1 3 2 9 10 11 12 17 btwncolg1 ${⊢}\left({\phi }\wedge {X}={Y}\right)\to \left({X}\in \left({Y}{L}{Z}\right)\vee {Y}={Z}\right)$
19 8 18 mtand ${⊢}{\phi }\to ¬{X}={Y}$
20 19 neqned ${⊢}{\phi }\to {X}\ne {Y}$