Theorem ncolne2

Description: Non-colinear points are different. (Contributed by Thierry Arnoux, 8-Aug-2019) TODO (NM): maybe ncolne2 could be simplified out and deleted, replaced by ncolcom .

	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	ncolne2	$$⊢\phi \to X\ne Z$$

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	1 3 2 4 6 7 5 8	ncolcom	$$⊢\phi \to \neg \left(X\in \left(ZLY\right)\vee Z=Y\right)$$
10	1 2 3 4 5 7 6 9	ncolne1	$$⊢\phi \to X\ne Z$$