Theorem ncolne1

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

	Ref	Expression
Hypotheses	tglineelsb2.p	|- B = ( Base ` G )
	tglineelsb2.i	|- I = ( Itv ` G )
	tglineelsb2.l	|- L = ( LineG ` G )
	tglineelsb2.g	|- ( ph -> G e. TarskiG )
	ncolne.x	|- ( ph -> X e. B )
	ncolne.y	|- ( ph -> Y e. B )
	ncolne.z	|- ( ph -> Z e. B )
	ncolne.2	|- ( ph -> -. ( X e. ( Y L Z ) \/ Y = Z ) )
Assertion	ncolne1	|- ( ph -> X =/= Y )

Proof

Step	Hyp	Ref	Expression
1		tglineelsb2.p	|- B = ( Base ` G )
2		tglineelsb2.i	|- I = ( Itv ` G )
3		tglineelsb2.l	|- L = ( LineG ` G )
4		tglineelsb2.g	|- ( ph -> G e. TarskiG )
5		ncolne.x	|- ( ph -> X e. B )
6		ncolne.y	|- ( ph -> Y e. B )
7		ncolne.z	|- ( ph -> Z e. B )
8		ncolne.2	|- ( ph -> -. ( X e. ( Y L Z ) \/ Y = Z ) )
9	4	adantr	|- ( ( ph /\ X = Y ) -> G e. TarskiG )
10	6	adantr	|- ( ( ph /\ X = Y ) -> Y e. B )
11	7	adantr	|- ( ( ph /\ X = Y ) -> Z e. B )
12	5	adantr	|- ( ( ph /\ X = Y ) -> X e. B )
13		eqid	|- ( dist ` G ) = ( dist ` G )
14	1 13 2 9 12 11	tgbtwntriv1	|- ( ( ph /\ X = Y ) -> X e. ( X I Z ) )
15		simpr	|- ( ( ph /\ X = Y ) -> X = Y )
16	15	oveq1d	|- ( ( ph /\ X = Y ) -> ( X I Z ) = ( Y I Z ) )
17	14 16	eleqtrd	|- ( ( ph /\ X = Y ) -> X e. ( Y I Z ) )
18	1 3 2 9 10 11 12 17	btwncolg1	|- ( ( ph /\ X = Y ) -> ( X e. ( Y L Z ) \/ Y = Z ) )
19	8 18	mtand	|- ( ph -> -. X = Y )
20	19	neqned	|- ( ph -> X =/= Y )