tglnpt3

Description: Find a third point on a line. (Contributed by Thierry Arnoux, 17-Jun-2026)

	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$
	tglnpt3.x	$⊢ φ \to X \in A$
	tglnpt3.y	$⊢ φ \to Y \in A$
	tglnpt3.1	$⊢ φ \to X \neq Y$
Assertion	tglnpt3	$⊢ φ \to \exists z \in A (z \neq X \land z \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		tglnpt3.x	$⊢ φ \to X \in A$
7		tglnpt3.y	$⊢ φ \to Y \in A$
8		tglnpt3.1	$⊢ φ \to X \neq Y$
9		eqid	$⊢ dist (G) = dist (G)$
10	4	ad2antrr	$⊢ ((φ \land t \in A) \land X \neq t) \to G \in 𝒢_{Tarski}$
11	1 3 2 4 5 7	tglnpt	$⊢ φ \to Y \in P$
12	11	ad2antrr	$⊢ ((φ \land t \in A) \land X \neq t) \to Y \in P$
13	1 3 2 4 5 6	tglnpt	$⊢ φ \to X \in P$
14	13	ad2antrr	$⊢ ((φ \land t \in A) \land X \neq t) \to X \in P$
15	1	fvexi	$⊢ P \in V$
16	15	a1i	$⊢ φ \to P \in V$
17	16 13 11 8	nehash2	$⊢ φ \to 2 \leq \|P\|$
18	17	ad2antrr	$⊢ ((φ \land t \in A) \land X \neq t) \to 2 \leq \|P\|$
19	1 9 2 10 12 14 18	tgbtwndiff	$⊢ ((φ \land t \in A) \land X \neq t) \to \exists z \in P (X \in (Y I z) \land X \neq z)$
20	4	ad5antr	$⊢ (((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \to G \in 𝒢_{Tarski}$
21	13	ad5antr	$⊢ (((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \to X \in P$
22	11	ad5antr	$⊢ (((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \to Y \in P$
23		simpllr	$⊢ (((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \to z \in P$
24	8	ad5antr	$⊢ (((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \to X \neq Y$
25		simpr	$⊢ (((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \to X \neq z$
26	20	adantr	$⊢ ((((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \land Y = z) \to G \in 𝒢_{Tarski}$
27	23	adantr	$⊢ ((((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \land Y = z) \to z \in P$
28	21	adantr	$⊢ ((((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \land Y = z) \to X \in P$
29		simpllr	$⊢ ((((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \land Y = z) \to X \in (Y I z)$
30		simpr	$⊢ ((((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \land Y = z) \to Y = z$
31	30	oveq1d	$⊢ ((((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \land Y = z) \to Y I z = z I z$
32	29 31	eleqtrd	$⊢ ((((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \land Y = z) \to X \in (z I z)$
33	1 9 2 26 27 28 32	axtgbtwnid	$⊢ ((((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \land Y = z) \to z = X$
34	33	eqcomd	$⊢ ((((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \land Y = z) \to X = z$
35	25 34	mteqand	$⊢ (((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \to Y \neq z$
36		simplr	$⊢ (((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \to X \in (Y I z)$
37	1 2 3 20 22 23 21 35 36	btwnlng1	$⊢ (((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \to X \in (Y L z)$
38	1 2 3 20 21 22 23 24 37 35	lnrot2	$⊢ (((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \to z \in (X L Y)$
39	1 2 3 4 13 11 8 8 5 6 7	tglinethru	$⊢ φ \to A = X L Y$
40	39	ad5antr	$⊢ (((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \to A = X L Y$
41	38 40	eleqtrrd	$⊢ (((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \to z \in A$
42	25	necomd	$⊢ (((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \to z \neq X$
43	35	necomd	$⊢ (((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \to z \neq Y$
44	41 42 43	jca32	$⊢ (((((φ \land t \in A) \land X \neq t) \land z \in P) \land X \in (Y I z)) \land X \neq z) \to (z \in A \land (z \neq X \land z \neq Y))$
45	44	anasss	$⊢ ((((φ \land t \in A) \land X \neq t) \land z \in P) \land (X \in (Y I z) \land X \neq z)) \to (z \in A \land (z \neq X \land z \neq Y))$
46	45	expl	$⊢ ((φ \land t \in A) \land X \neq t) \to ((z \in P \land (X \in (Y I z) \land X \neq z)) \to (z \in A \land (z \neq X \land z \neq Y)))$
47	46	reximdv2	$⊢ ((φ \land t \in A) \land X \neq t) \to (\exists z \in P (X \in (Y I z) \land X \neq z) \to \exists z \in A (z \neq X \land z \neq Y))$
48	19 47	mpd	$⊢ ((φ \land t \in A) \land X \neq t) \to \exists z \in A (z \neq X \land z \neq Y)$
49	1 2 3 4 5 6	tglnpt2	$⊢ φ \to \exists t \in A X \neq t$
50	48 49	r19.29a	$⊢ φ \to \exists z \in A (z \neq X \land z \neq Y)$

Metamath Proof Explorer

Theorem tglnpt3

Proof