Theorem 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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tgplnfn.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tgplnfn.i	⊢ 𝐸 = ( hlG ‘ 𝐺 )
	tgplnfn.1	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
	tgelrnpln.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
	tgelrnpln.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑃 ∖ 𝐴 ) )
Assertion	tgelrnpln	⊢ ( 𝜑 → ( 𝐴 𝐸 𝑅 ) ∈ ran 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		tgplnfn.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tgplnfn.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
3		tgplnfn.i	⊢ 𝐸 = ( hlG ‘ 𝐺 )
4		tgplnfn.1	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
5		tgelrnpln.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
6		tgelrnpln.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑃 ∖ 𝐴 ) )
7		df-ov	⊢ ( 𝐴 𝐸 𝑅 ) = ( 𝐸 ‘ ⟨ 𝐴 , 𝑅 ⟩ )
8	1 2 3 4	tgplnfn	⊢ ( 𝜑 → 𝐸 Fn ( ( ran 𝐿 × 𝑃 ) ∖ ◡ E ) )
9	6	eldifad	⊢ ( 𝜑 → 𝑅 ∈ 𝑃 )
10	5 9	opelxpd	⊢ ( 𝜑 → ⟨ 𝐴 , 𝑅 ⟩ ∈ ( ran 𝐿 × 𝑃 ) )
11	6	eldifbd	⊢ ( 𝜑 → ¬ 𝑅 ∈ 𝐴 )
12		df-br	⊢ ( 𝐴 ◡ E 𝑅 ↔ ⟨ 𝐴 , 𝑅 ⟩ ∈ ◡ E )
13		brcnvg	⊢ ( ( 𝐴 ∈ ran 𝐿 ∧ 𝑅 ∈ 𝑃 ) → ( 𝐴 ◡ E 𝑅 ↔ 𝑅 E 𝐴 ) )
14	5 9 13	syl2anc	⊢ ( 𝜑 → ( 𝐴 ◡ E 𝑅 ↔ 𝑅 E 𝐴 ) )
15		epelg	⊢ ( 𝐴 ∈ ran 𝐿 → ( 𝑅 E 𝐴 ↔ 𝑅 ∈ 𝐴 ) )
16	5 15	syl	⊢ ( 𝜑 → ( 𝑅 E 𝐴 ↔ 𝑅 ∈ 𝐴 ) )
17	14 16	bitrd	⊢ ( 𝜑 → ( 𝐴 ◡ E 𝑅 ↔ 𝑅 ∈ 𝐴 ) )
18	12 17	bitr3id	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝑅 ⟩ ∈ ◡ E ↔ 𝑅 ∈ 𝐴 ) )
19	11 18	mtbird	⊢ ( 𝜑 → ¬ ⟨ 𝐴 , 𝑅 ⟩ ∈ ◡ E )
20	10 19	eldifd	⊢ ( 𝜑 → ⟨ 𝐴 , 𝑅 ⟩ ∈ ( ( ran 𝐿 × 𝑃 ) ∖ ◡ E ) )
21	8 20	fnfvelrnd	⊢ ( 𝜑 → ( 𝐸 ‘ ⟨ 𝐴 , 𝑅 ⟩ ) ∈ ran 𝐸 )
22	7 21	eqeltrid	⊢ ( 𝜑 → ( 𝐴 𝐸 𝑅 ) ∈ ran 𝐸 )