Definition df-plng

Description: Define the function building a plane from a line and a point not on that line. Definition 9.20 of Schwabhauser p. 74. (Contributed by Thierry Arnoux, 17-Jun-2026)

	Ref	Expression
Assertion	df-plng	Could not format assertion : No typesetting found for |- PlnG = ( g e. _V |-> ( a e. ran ( LineG ` g ) , r e. ( ( Base ` g ) \ a ) |-> { x e. ( Base ` g ) | ( x e. a \/ x ( ( hpG ` g ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` g ) r ) ) } ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cplng	Could not format PlnG : No typesetting found for class PlnG with typecode class
1		vg	$$setvarg$$
2		cvv	$$class\mathrm{V}$$
3		va	$$setvara$$
4		clng	$$class{Line}_{𝒢}$$
5	1	cv	$$setvarg$$
6	5 4	cfv	$$class{Line}_{𝒢}\left(g\right)$$
7	6	crn	$$class\mathrm{ran}{Line}_{𝒢}\left(g\right)$$
8		vr	$$setvarr$$
9		cbs	$$class\mathrm{Base}$$
10	5 9	cfv	$$class{\mathrm{Base}}_g$$
11	3	cv	$$setvara$$
12	10 11	cdif	$$class\left({\mathrm{Base}}_g\setminus a\right)$$
13		vx	$$setvarx$$
14	13	cv	$$setvarx$$
15	14 11	wcel	$$wffx\in a$$
16		chpg	$$class{hp}_{𝒢}$$
17	5 16	cfv	$$class{hp}_{𝒢}\left(g\right)$$
18	11 17	cfv	$$class{hp}_{𝒢}\left(g\right)\left(a\right)$$
19	8	cv	$$setvarr$$
20	14 19 18	wbr	$$wffx{hp}_{𝒢}\left(g\right)\left(a\right)r$$
21		vt	$$setvart$$
22	21	cv	$$setvart$$
23		citv	$$class\mathrm{Itv}$$
24	5 23	cfv	$$class\mathrm{Itv}\left(g\right)$$
25	14 19 24	co	$$class\left(x\mathrm{Itv}\left(g\right)r\right)$$
26	22 25	wcel	$$wfft\in \left(x\mathrm{Itv}\left(g\right)r\right)$$
27	26 21 11	wrex	$$wff\exists t\in at\in \left(x\mathrm{Itv}\left(g\right)r\right)$$
28	15 20 27	w3o	$$wff\left(x\in a\vee x{hp}_{𝒢}\left(g\right)\left(a\right)r\vee \exists t\in at\in \left(x\mathrm{Itv}\left(g\right)r\right)\right)$$
29	28 13 10	crab	$$class\left\{x\in {\mathrm{Base}}_g|\left(x\in a\vee x{hp}_{𝒢}\left(g\right)\left(a\right)r\vee \exists t\in at\in \left(x\mathrm{Itv}\left(g\right)r\right)\right)\right\}$$
30	3 8 7 12 29	cmpo	$$class\left(a\in \mathrm{ran}{Line}_{𝒢}\left(g\right),r\in \left({\mathrm{Base}}_g\setminus a\right)⟼\left\{x\in {\mathrm{Base}}_g|\left(x\in a\vee x{hp}_{𝒢}\left(g\right)\left(a\right)r\vee \exists t\in at\in \left(x\mathrm{Itv}\left(g\right)r\right)\right)\right\}\right)$$
31	1 2 30	cmpt	$$class\left(g\in \mathrm{V}⟼\left(a\in \mathrm{ran}{Line}_{𝒢}\left(g\right),r\in \left({\mathrm{Base}}_g\setminus a\right)⟼\left\{x\in {\mathrm{Base}}_g|\left(x\in a\vee x{hp}_{𝒢}\left(g\right)\left(a\right)r\vee \exists t\in at\in \left(x\mathrm{Itv}\left(g\right)r\right)\right)\right\}\right)\right)$$
32	0 31	wceq	Could not format PlnG = ( g e. _V |-> ( a e. ran ( LineG ` g ) , r e. ( ( Base ` g ) \ a ) |-> { x e. ( Base ` g ) | ( x e. a \/ x ( ( hpG ` g ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` g ) r ) ) } ) ) : No typesetting found for wff PlnG = ( g e. _V |-> ( a e. ran ( LineG ` g ) , r e. ( ( Base ` g ) \ a ) |-> { x e. ( Base ` g ) | ( x e. a \/ x ( ( hpG ` g ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` g ) r ) ) } ) ) with typecode wff