elplnglnid

Description: The line A itself is a subset of a plane defined by the line A and a point R . (Contributed by Thierry Arnoux, 17-Jun-2026)

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

Step	Hyp	Ref	Expression
1		plngval.p	$⊢ P = {Base}_{G}$
2		plngval.i	$⊢ I = Itv (G)$
3		plngval.1	$⊢ L = {Line}_{𝒢} (G)$
4		plngval.e	Could not format E = ( PlnG ` G ) : No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
5		plngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		elplng.a	$⊢ φ \to A \in ran L$
7		elplng.r	$⊢ φ \to R \in (P ∖ A)$
8		simpr	$⊢ (φ \land z \in A) \to z \in A$
9	8	3mix1d	$⊢ (φ \land z \in A) \to (z \in A \lor z {hp}_{𝒢} (G) (A) R \lor z \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b))\} R)$
10	5	adantr	$⊢ (φ \land z \in A) \to G \in 𝒢_{Tarski}$
11	6	adantr	$⊢ (φ \land z \in A) \to A \in ran L$
12	7	adantr	$⊢ (φ \land z \in A) \to R \in (P ∖ A)$
13		eqid	$⊢ \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b))\} = \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b))\}$
14	1 3 2 10 11 8	tglnpt	$⊢ (φ \land z \in A) \to z \in P$
15	1 2 3 4 10 11 12 13 14	elplng	$⊢ (φ \land z \in A) \to (z \in (A E R) \leftrightarrow (z \in A \lor z {hp}_{𝒢} (G) (A) R \lor z \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b))\} R))$
16	9 15	mpbird	$⊢ (φ \land z \in A) \to z \in (A E R)$
17	16	ex	$⊢ φ \to (z \in A \to z \in (A E R))$
18	17	ssrdv	$⊢ φ \to A \subseteq A E R$

Metamath Proof Explorer