tglnpt2

Description: Find a second point on a line. (Contributed by Thierry Arnoux, 18-Oct-2019)

	Ref	Expression
Hypotheses	tglnpt2.p	$⊢ P = {Base}_{G}$
	tglnpt2.i	$⊢ I = Itv (G)$
	tglnpt2.l	$⊢ L = {Line}_{𝒢} (G)$
	tglnpt2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tglnpt2.a	$⊢ φ \to A \in ran L$
	tglnpt2.x	$⊢ φ \to X \in A$
Assertion	tglnpt2	$⊢ φ \to \exists y \in A X \neq y$

Proof

Step	Hyp	Ref	Expression
1		tglnpt2.p	$⊢ P = {Base}_{G}$
2		tglnpt2.i	$⊢ I = Itv (G)$
3		tglnpt2.l	$⊢ L = {Line}_{𝒢} (G)$
4		tglnpt2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tglnpt2.a	$⊢ φ \to A \in ran L$
6		tglnpt2.x	$⊢ φ \to X \in A$
7		neeq2	$⊢ y = z \to (X \neq y \leftrightarrow X \neq z)$
8	4	ad4antr	$⊢ ((((φ \land x \in P) \land z \in P) \land (A = x L z \land x \neq z)) \land X = x) \to G \in 𝒢_{Tarski}$
9		simp-4r	$⊢ ((((φ \land x \in P) \land z \in P) \land (A = x L z \land x \neq z)) \land X = x) \to x \in P$
10		simpllr	$⊢ ((((φ \land x \in P) \land z \in P) \land (A = x L z \land x \neq z)) \land X = x) \to z \in P$
11		simplrr	$⊢ ((((φ \land x \in P) \land z \in P) \land (A = x L z \land x \neq z)) \land X = x) \to x \neq z$
12	1 2 3 8 9 10 11	tglinerflx2	$⊢ ((((φ \land x \in P) \land z \in P) \land (A = x L z \land x \neq z)) \land X = x) \to z \in (x L z)$
13		simplrl	$⊢ ((((φ \land x \in P) \land z \in P) \land (A = x L z \land x \neq z)) \land X = x) \to A = x L z$
14	12 13	eleqtrrd	$⊢ ((((φ \land x \in P) \land z \in P) \land (A = x L z \land x \neq z)) \land X = x) \to z \in A$
15		simpr	$⊢ ((((φ \land x \in P) \land z \in P) \land (A = x L z \land x \neq z)) \land X = x) \to X = x$
16	15 11	eqnetrd	$⊢ ((((φ \land x \in P) \land z \in P) \land (A = x L z \land x \neq z)) \land X = x) \to X \neq z$
17	7 14 16	rspcedvdw	$⊢ ((((φ \land x \in P) \land z \in P) \land (A = x L z \land x \neq z)) \land X = x) \to \exists y \in A X \neq y$
18		neeq2	$⊢ y = x \to (X \neq y \leftrightarrow X \neq x)$
19	4	ad4antr	$⊢ ((((φ \land x \in P) \land z \in P) \land (A = x L z \land x \neq z)) \land X \neq x) \to G \in 𝒢_{Tarski}$
20		simp-4r	$⊢ ((((φ \land x \in P) \land z \in P) \land (A = x L z \land x \neq z)) \land X \neq x) \to x \in P$
21		simpllr	$⊢ ((((φ \land x \in P) \land z \in P) \land (A = x L z \land x \neq z)) \land X \neq x) \to z \in P$
22		simplrr	$⊢ ((((φ \land x \in P) \land z \in P) \land (A = x L z \land x \neq z)) \land X \neq x) \to x \neq z$
23	1 2 3 19 20 21 22	tglinerflx1	$⊢ ((((φ \land x \in P) \land z \in P) \land (A = x L z \land x \neq z)) \land X \neq x) \to x \in (x L z)$
24		simplrl	$⊢ ((((φ \land x \in P) \land z \in P) \land (A = x L z \land x \neq z)) \land X \neq x) \to A = x L z$
25	23 24	eleqtrrd	$⊢ ((((φ \land x \in P) \land z \in P) \land (A = x L z \land x \neq z)) \land X \neq x) \to x \in A$
26		simpr	$⊢ ((((φ \land x \in P) \land z \in P) \land (A = x L z \land x \neq z)) \land X \neq x) \to X \neq x$
27	18 25 26	rspcedvdw	$⊢ ((((φ \land x \in P) \land z \in P) \land (A = x L z \land x \neq z)) \land X \neq x) \to \exists y \in A X \neq y$
28	17 27	pm2.61dane	$⊢ (((φ \land x \in P) \land z \in P) \land (A = x L z \land x \neq z)) \to \exists y \in A X \neq y$
29	1 2 3 4 5	tgisline	$⊢ φ \to \exists x \in P \exists z \in P (A = x L z \land x \neq z)$
30	28 29	r19.29vva	$⊢ φ \to \exists y \in A X \neq y$

Metamath Proof Explorer

Theorem tglnpt2

Proof