tglnne

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

	Ref	Expression
Hypotheses	tglineelsb2.p	$⊢ B = {Base}_{G}$
	tglineelsb2.i	$⊢ I = Itv (G)$
	tglineelsb2.l	$⊢ L = {Line}_{𝒢} (G)$
	tglineelsb2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tglnne.x	$⊢ φ \to X \in B$
	tglnne.y	$⊢ φ \to Y \in B$
	tglnne.1	$⊢ φ \to X L Y \in ran L$
Assertion	tglnne	$⊢ φ \to X \neq Y$

Proof

Step	Hyp	Ref	Expression
1		tglineelsb2.p	$⊢ B = {Base}_{G}$
2		tglineelsb2.i	$⊢ I = Itv (G)$
3		tglineelsb2.l	$⊢ L = {Line}_{𝒢} (G)$
4		tglineelsb2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tglnne.x	$⊢ φ \to X \in B$
6		tglnne.y	$⊢ φ \to Y \in B$
7		tglnne.1	$⊢ φ \to X L Y \in ran L$
8	4	ad3antrrr	$⊢ (((φ \land x \in B) \land y \in B) \land (X L Y = x L y \land x \neq y)) \to G \in 𝒢_{Tarski}$
9	5	ad3antrrr	$⊢ (((φ \land x \in B) \land y \in B) \land (X L Y = x L y \land x \neq y)) \to X \in B$
10	6	ad3antrrr	$⊢ (((φ \land x \in B) \land y \in B) \land (X L Y = x L y \land x \neq y)) \to Y \in B$
11		simpllr	$⊢ (((φ \land x \in B) \land y \in B) \land (X L Y = x L y \land x \neq y)) \to x \in B$
12		simplr	$⊢ (((φ \land x \in B) \land y \in B) \land (X L Y = x L y \land x \neq y)) \to y \in B$
13		simprr	$⊢ (((φ \land x \in B) \land y \in B) \land (X L Y = x L y \land x \neq y)) \to x \neq y$
14		eqid	$⊢ dist (G) = dist (G)$
15	1 14 2 8 11 12	tgbtwntriv1	$⊢ (((φ \land x \in B) \land y \in B) \land (X L Y = x L y \land x \neq y)) \to x \in (x I y)$
16	1 2 3 8 11 12 11 13 15	btwnlng1	$⊢ (((φ \land x \in B) \land y \in B) \land (X L Y = x L y \land x \neq y)) \to x \in (x L y)$
17		simprl	$⊢ (((φ \land x \in B) \land y \in B) \land (X L Y = x L y \land x \neq y)) \to X L Y = x L y$
18	16 17	eleqtrrd	$⊢ (((φ \land x \in B) \land y \in B) \land (X L Y = x L y \land x \neq y)) \to x \in (X L Y)$
19	1 3 2 8 9 10 18	tglngne	$⊢ (((φ \land x \in B) \land y \in B) \land (X L Y = x L y \land x \neq y)) \to X \neq Y$
20	1 2 3 4 7	tgisline	$⊢ φ \to \exists x \in B \exists y \in B (X L Y = x L y \land x \neq y)$
21	19 20	r19.29vva	$⊢ φ \to X \neq Y$

Metamath Proof Explorer

Theorem tglnne

Proof