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 \neg \left(X\in \left(YLZ\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 \neg \left(X\in \left(YLZ\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(XIZ\right)$$
15		simpr	$$⊢\left(\phi \wedge X=Y\right)\to X=Y$$
16	15	oveq1d	$$⊢\left(\phi \wedge X=Y\right)\to XIZ=YIZ$$
17	14 16	eleqtrd	$$⊢\left(\phi \wedge X=Y\right)\to X\in \left(YIZ\right)$$
18	1 3 2 9 10 11 12 17	btwncolg1	$$⊢\left(\phi \wedge X=Y\right)\to \left(X\in \left(YLZ\right)\vee Y=Z\right)$$
19	8 18	mtand	$$⊢\phi \to \neg X=Y$$
20	19	neqned	$$⊢\phi \to X\ne Y$$