tgelrnpln

Description: The property of being a plane, generated by a line and a point. (Contributed by Thierry Arnoux, 17-Jun-2026)

	Ref	Expression
Hypotheses	tgplnfn.p	$⊢ P = {Base}_{G}$
	tgplnfn.l	$⊢ L = {Line}_{𝒢} (G)$
	tgplnfn.i	No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
	tgplnfn.1	$⊢ φ \to G \in V$
	tgelrnpln.a	$⊢ φ \to A \in ran L$
	tgelrnpln.r	$⊢ φ \to R \in (P ∖ A)$
Assertion	tgelrnpln	$⊢ φ \to A E R \in ran E$

Step	Hyp	Ref	Expression
1		tgplnfn.p	$⊢ P = {Base}_{G}$
2		tgplnfn.l	$⊢ L = {Line}_{𝒢} (G)$
3		tgplnfn.i	Could not format E = ( PlnG ` G ) : No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
4		tgplnfn.1	$⊢ φ \to G \in V$
5		tgelrnpln.a	$⊢ φ \to A \in ran L$
6		tgelrnpln.r	$⊢ φ \to R \in (P ∖ A)$
7		df-ov	$⊢ A E R = E (⟨A, R⟩)$
8	1 2 3 4	tgplnfn	$⊢ φ \to E Fn ((ran L \times P) ∖ E^{-1})$
9	6	eldifad	$⊢ φ \to R \in P$
10	5 9	opelxpd	$⊢ φ \to ⟨A, R⟩ \in (ran L \times P)$
11	6	eldifbd	$⊢ φ \to \neg R \in A$
12		df-br	$⊢ A E^{-1} R \leftrightarrow ⟨A, R⟩ \in E^{-1}$
13		brcnvg	$⊢ (A \in ran L \land R \in P) \to (A E^{-1} R \leftrightarrow R E A)$
14	5 9 13	syl2anc	$⊢ φ \to (A E^{-1} R \leftrightarrow R E A)$
15		epelg	$⊢ A \in ran L \to (R E A \leftrightarrow R \in A)$
16	5 15	syl	$⊢ φ \to (R E A \leftrightarrow R \in A)$
17	14 16	bitrd	$⊢ φ \to (A E^{-1} R \leftrightarrow R \in A)$
18	12 17	bitr3id	$⊢ φ \to (⟨A, R⟩ \in E^{-1} \leftrightarrow R \in A)$
19	11 18	mtbird	$⊢ φ \to \neg ⟨A, R⟩ \in E^{-1}$
20	10 19	eldifd	$⊢ φ \to ⟨A, R⟩ \in ((ran L \times P) ∖ E^{-1})$
21	8 20	fnfvelrnd	$⊢ φ \to E (⟨A, R⟩) \in ran E$
22	7 21	eqeltrid	$⊢ φ \to A E R \in ran E$

Metamath Proof Explorer