Theorem ncolne1

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

	Ref	Expression
Hypotheses	tglineelsb2.p	⊢ 𝐵 = ( Base ‘ 𝐺 )
	tglineelsb2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tglineelsb2.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tglineelsb2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	ncolne.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	ncolne.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	ncolne.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	ncolne.2	⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
Assertion	ncolne1	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		tglineelsb2.p	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		tglineelsb2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		tglineelsb2.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		tglineelsb2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		ncolne.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		ncolne.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		ncolne.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8		ncolne.2	⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
9	4	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝐺 ∈ TarskiG )
10	6	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑌 ∈ 𝐵 )
11	7	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑍 ∈ 𝐵 )
12	5	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 ∈ 𝐵 )
13		eqid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
14	1 13 2 9 12 11	tgbtwntriv1	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 ∈ ( 𝑋 𝐼 𝑍 ) )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 = 𝑌 )
16	15	oveq1d	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝑋 𝐼 𝑍 ) = ( 𝑌 𝐼 𝑍 ) )
17	14 16	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) )
18	1 3 2 9 10 11 12 17	btwncolg1	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
19	8 18	mtand	⊢ ( 𝜑 → ¬ 𝑋 = 𝑌 )
20	19	neqned	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )