Theorem tglnne

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

	Ref	Expression
Hypotheses	tglineelsb2.p	⊢ 𝐵 = ( Base ‘ 𝐺 )
	tglineelsb2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tglineelsb2.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tglineelsb2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tglnne.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	tglnne.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	tglnne.1	⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
Assertion	tglnne	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		tglineelsb2.p	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		tglineelsb2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		tglineelsb2.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		tglineelsb2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		tglnne.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		tglnne.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		tglnne.1	⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
8	4	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 𝑋 𝐿 𝑌 ) = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝐺 ∈ TarskiG )
9	5	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 𝑋 𝐿 𝑌 ) = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑋 ∈ 𝐵 )
10	6	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 𝑋 𝐿 𝑌 ) = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑌 ∈ 𝐵 )
11		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 𝑋 𝐿 𝑌 ) = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ∈ 𝐵 )
12		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 𝑋 𝐿 𝑌 ) = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑦 ∈ 𝐵 )
13		simprr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 𝑋 𝐿 𝑌 ) = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ≠ 𝑦 )
14		eqid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
15	1 14 2 8 11 12	tgbtwntriv1	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 𝑋 𝐿 𝑌 ) = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ∈ ( 𝑥 𝐼 𝑦 ) )
16	1 2 3 8 11 12 11 13 15	btwnlng1	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 𝑋 𝐿 𝑌 ) = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ∈ ( 𝑥 𝐿 𝑦 ) )
17		simprl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 𝑋 𝐿 𝑌 ) = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝑋 𝐿 𝑌 ) = ( 𝑥 𝐿 𝑦 ) )
18	16 17	eleqtrrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 𝑋 𝐿 𝑌 ) = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ∈ ( 𝑋 𝐿 𝑌 ) )
19	1 3 2 8 9 10 18	tglngne	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( 𝑋 𝐿 𝑌 ) = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑋 ≠ 𝑌 )
20	1 2 3 4 7	tgisline	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑋 𝐿 𝑌 ) = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )
21	19 20	r19.29vva	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )