Theorem tglngne

Description: It takes two different points to form a line. (Contributed by Thierry Arnoux, 6-Aug-2019)

	Ref	Expression
Hypotheses	tglngval.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tglngval.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tglngval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tglngval.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tglngval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	tglngval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	tglngne.1	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) )
Assertion	tglngne	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		tglngval.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tglngval.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
3		tglngval.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		tglngval.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		tglngval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
6		tglngval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
7		tglngne.1	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) )
8		df-ov	⊢ ( 𝑋 𝐿 𝑌 ) = ( 𝐿 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
9	7 8	eleqtrdi	⊢ ( 𝜑 → 𝑍 ∈ ( 𝐿 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
10		elfvdm	⊢ ( 𝑍 ∈ ( 𝐿 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom 𝐿 )
11	9 10	syl	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom 𝐿 )
12	1 2 3	tglnfn	⊢ ( 𝐺 ∈ TarskiG → 𝐿 Fn ( ( 𝑃 × 𝑃 ) ∖ I ) )
13		fndm	⊢ ( 𝐿 Fn ( ( 𝑃 × 𝑃 ) ∖ I ) → dom 𝐿 = ( ( 𝑃 × 𝑃 ) ∖ I ) )
14	4 12 13	3syl	⊢ ( 𝜑 → dom 𝐿 = ( ( 𝑃 × 𝑃 ) ∖ I ) )
15	11 14	eleqtrd	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ( 𝑃 × 𝑃 ) ∖ I ) )
16	15	eldifbd	⊢ ( 𝜑 → ¬ ⟨ 𝑋 , 𝑌 ⟩ ∈ I )
17		df-br	⊢ ( 𝑋 I 𝑌 ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ I )
18		ideqg	⊢ ( 𝑌 ∈ 𝑃 → ( 𝑋 I 𝑌 ↔ 𝑋 = 𝑌 ) )
19	6 18	syl	⊢ ( 𝜑 → ( 𝑋 I 𝑌 ↔ 𝑋 = 𝑌 ) )
20	17 19	bitr3id	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ I ↔ 𝑋 = 𝑌 ) )
21	20	necon3bbid	⊢ ( 𝜑 → ( ¬ ⟨ 𝑋 , 𝑌 ⟩ ∈ I ↔ 𝑋 ≠ 𝑌 ) )
22	16 21	mpbid	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )