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	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}$
8		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$
9		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$
10		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$
11	1 2 3 7 8 9 10	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)$
12		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$
13	11 12	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$
14		simpr	$⊢ ((((φ \land x \in P) \land z \in P) \land (A = x L z \land x \neq z)) \land X = x) \to X = x$
15	14 10	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$
16		neeq2	$⊢ y = z \to (X \neq y \leftrightarrow X \neq z)$
17	16	rspcev	$⊢ (z \in A \land X \neq z) \to \exists y \in A X \neq y$
18	13 15 17	syl2anc	$⊢ ((((φ \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$
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		neeq2	$⊢ y = x \to (X \neq y \leftrightarrow X \neq x)$
28	27	rspcev	$⊢ (x \in A \land X \neq x) \to \exists y \in A X \neq y$
29	25 26 28	syl2anc	$⊢ ((((φ \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$
30	18 29	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$
31	1 2 3 4 5	tgisline	$⊢ φ \to \exists x \in P \exists z \in P (A = x L z \land x \neq z)$
32	30 31	r19.29vva	$⊢ φ \to \exists y \in A X \neq y$

Metamath Proof Explorer

Theorem tglnpt2

Proof