plng3p

Description: If H is a plane containing a line A and a point R not on A , then H is the plane defined by A and R . Theorem 9.26 of Schwabhauser p. 76. See tglinethru for the 2-point line equivalent. (Contributed by Thierry Arnoux, 17-Jun-2026)

	Ref	Expression
Hypotheses	plng3p.p	$⊢ P = {Base}_{G}$
	plng3p.l	$⊢ L = {Line}_{𝒢} (G)$
	plng3p.e	No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
	plng3p.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	plng3p.h	$⊢ φ \to H \in ran E$
	plng3p.a	$⊢ φ \to A \in ran L$
	plng3p.r	$⊢ φ \to R \in (H ∖ A)$
	plng3p.1	$⊢ φ \to A \subseteq H$
Assertion	plng3p	$⊢ φ \to H = A E R$

Proof

Step	Hyp	Ref	Expression
1		plng3p.p	$⊢ P = {Base}_{G}$
2		plng3p.l	$⊢ L = {Line}_{𝒢} (G)$
3		plng3p.e	Could not format E = ( PlnG ` G ) : No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
4		plng3p.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		plng3p.h	$⊢ φ \to H \in ran E$
6		plng3p.a	$⊢ φ \to A \in ran L$
7		plng3p.r	$⊢ φ \to R \in (H ∖ A)$
8		plng3p.1	$⊢ φ \to A \subseteq H$
9		simpr	$⊢ ((((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \land s \in (P ∖ (x L y))) \land H = (x L y) E s) \to H = (x L y) E s$
10		simp-4r	$⊢ ((((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \land s \in (P ∖ (x L y))) \land H = (x L y) E s) \to A = x L y$
11	10	oveq1d	$⊢ ((((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \land s \in (P ∖ (x L y))) \land H = (x L y) E s) \to A E s = (x L y) E s$
12		eqid	$⊢ Itv (G) = Itv (G)$
13	4	ad6antr	$⊢ ((((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \land s \in (P ∖ (x L y))) \land H = (x L y) E s) \to G \in 𝒢_{Tarski}$
14	6	ad6antr	$⊢ ((((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \land s \in (P ∖ (x L y))) \land H = (x L y) E s) \to A \in ran L$
15		simplr	$⊢ ((((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \land s \in (P ∖ (x L y))) \land H = (x L y) E s) \to s \in (P ∖ (x L y))$
16	10	difeq2d	$⊢ ((((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \land s \in (P ∖ (x L y))) \land H = (x L y) E s) \to P ∖ A = P ∖ (x L y)$
17	15 16	eleqtrrd	$⊢ ((((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \land s \in (P ∖ (x L y))) \land H = (x L y) E s) \to s \in (P ∖ A)$
18	7	ad6antr	$⊢ ((((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \land s \in (P ∖ (x L y))) \land H = (x L y) E s) \to R \in (H ∖ A)$
19	11 9	eqtr4d	$⊢ ((((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \land s \in (P ∖ (x L y))) \land H = (x L y) E s) \to A E s = H$
20	19	difeq1d	$⊢ ((((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \land s \in (P ∖ (x L y))) \land H = (x L y) E s) \to (A E s) ∖ A = H ∖ A$
21	18 20	eleqtrrd	$⊢ ((((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \land s \in (P ∖ (x L y))) \land H = (x L y) E s) \to R \in ((A E s) ∖ A)$
22	1 12 2 3 13 14 17 21	plngcp	$⊢ ((((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \land s \in (P ∖ (x L y))) \land H = (x L y) E s) \to A E s = A E R$
23	9 11 22	3eqtr2d	$⊢ ((((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \land s \in (P ∖ (x L y))) \land H = (x L y) E s) \to H = A E R$
24	4	ad4antr	$⊢ ((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \to G \in 𝒢_{Tarski}$
25	5	ad4antr	$⊢ ((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \to H \in ran E$
26	8	ad4antr	$⊢ ((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \to A \subseteq H$
27		simp-4r	$⊢ ((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \to x \in P$
28		simpllr	$⊢ ((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \to y \in P$
29		simpr	$⊢ ((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \to x \neq y$
30	1 12 2 24 27 28 29	tglinerflx1	$⊢ ((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \to x \in (x L y)$
31		simplr	$⊢ ((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \to A = x L y$
32	30 31	eleqtrrd	$⊢ ((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \to x \in A$
33	26 32	sseldd	$⊢ ((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \to x \in H$
34	1 12 2 24 27 28 29	tglinerflx2	$⊢ ((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \to y \in (x L y)$
35	34 31	eleqtrrd	$⊢ ((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \to y \in A$
36	26 35	sseldd	$⊢ ((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \to y \in H$
37	1 12 2 3 24 25 33 36 29	lnssplng	$⊢ ((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \to (x L y \subseteq H \land \exists s \in (P ∖ (x L y)) H = (x L y) E s)$
38	37	simprd	$⊢ ((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \to \exists s \in (P ∖ (x L y)) H = (x L y) E s$
39	23 38	r19.29a	$⊢ ((((φ \land x \in P) \land y \in P) \land A = x L y) \land x \neq y) \to H = A E R$
40	39	anasss	$⊢ (((φ \land x \in P) \land y \in P) \land (A = x L y \land x \neq y)) \to H = A E R$
41	1 12 2 4 6	tgisline	$⊢ φ \to \exists x \in P \exists y \in P (A = x L y \land x \neq y)$
42	40 41	r19.29vva	$⊢ φ \to H = A E R$

Metamath Proof Explorer

Theorem plng3p

Proof