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	|- P = ( Base ` G )
	tgplnfn.l	|- L = ( LineG ` G )
	tgplnfn.i	|- E = ( PlnG ` G )
	tgplnfn.1	|- ( ph -> G e. V )
	tgelrnpln.a	|- ( ph -> A e. ran L )
	tgelrnpln.r	|- ( ph -> R e. ( P \ A ) )
Assertion	tgelrnpln	|- ( ph -> ( A E R ) e. ran E )

Proof

Step	Hyp	Ref	Expression
1		tgplnfn.p	|- P = ( Base ` G )
2		tgplnfn.l	|- L = ( LineG ` G )
3		tgplnfn.i	|- E = ( PlnG ` G )
4		tgplnfn.1	|- ( ph -> G e. V )
5		tgelrnpln.a	|- ( ph -> A e. ran L )
6		tgelrnpln.r	|- ( ph -> R e. ( P \ A ) )
7		df-ov	|- ( A E R ) = ( E ` <. A , R >. )
8	1 2 3 4	tgplnfn	|- ( ph -> E Fn ( ( ran L X. P ) \ `' _E ) )
9	6	eldifad	|- ( ph -> R e. P )
10	5 9	opelxpd	|- ( ph -> <. A , R >. e. ( ran L X. P ) )
11	6	eldifbd	|- ( ph -> -. R e. A )
12		df-br	|- ( A `' _E R <-> <. A , R >. e. `' _E )
13		brcnvg	|- ( ( A e. ran L /\ R e. P ) -> ( A `' _E R <-> R _E A ) )
14	5 9 13	syl2anc	|- ( ph -> ( A `' _E R <-> R _E A ) )
15		epelg	|- ( A e. ran L -> ( R _E A <-> R e. A ) )
16	5 15	syl	|- ( ph -> ( R _E A <-> R e. A ) )
17	14 16	bitrd	|- ( ph -> ( A `' _E R <-> R e. A ) )
18	12 17	bitr3id	|- ( ph -> ( <. A , R >. e. `' _E <-> R e. A ) )
19	11 18	mtbird	|- ( ph -> -. <. A , R >. e. `' _E )
20	10 19	eldifd	|- ( ph -> <. A , R >. e. ( ( ran L X. P ) \ `' _E ) )
21	8 20	fnfvelrnd	|- ( ph -> ( E ` <. A , R >. ) e. ran E )
22	7 21	eqeltrid	|- ( ph -> ( A E R ) e. ran E )