Definition df-plng 28978

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.)

Assertion

Ref	Expression
df-plng	⊢ hlG = (𝑔 ∈ V ↦ (𝑎 ∈ ran (LineG‘𝑔), 𝑟 ∈ ((Base‘𝑔) ∖ 𝑎) ↦ {𝑥 ∈ (Base‘𝑔) ∣ (𝑥 ∈ 𝑎 ∨ 𝑥((hpG‘𝑔)‘𝑎)𝑟 ∨ ∃𝑡 ∈ 𝑎 𝑡 ∈ (𝑥(Itv‘𝑔)𝑟))}))

Distinct variable group:   𝑔,𝑎,𝑟,𝑡,𝑥

Detailed syntax breakdown of Definition df-plng

Step	Hyp	Ref	Expression
1		cplng 28977	. 2 class hlG
2		vg	. . 3 setvar 𝑔
3		cvv 3454	. . 3 class V
4		va	. . . 4 setvar 𝑎
5		vr	. . . 4 setvar 𝑟
6	2	cv 1559	. . . . . 6 class 𝑔
7		clng 28600	. . . . . 6 class LineG
8	6, 7	cfv 6521	. . . . 5 class (LineG‘𝑔)
9	8	crn 5648	. . . 4 class ran (LineG‘𝑔)
10		cbs 17245	. . . . . 6 class Base
11	6, 10	cfv 6521	. . . . 5 class (Base‘𝑔)
12	4	cv 1559	. . . . 5 class 𝑎
13	11, 12	cdif 3901	. . . 4 class ((Base‘𝑔) ∖ 𝑎)
14		vx	. . . . . . 7 setvar 𝑥
15	14, 4	wel 2143	. . . . . 6 wff 𝑥 ∈ 𝑎
16	14	cv 1559	. . . . . . 7 class 𝑥
17	5	cv 1559	. . . . . . 7 class 𝑟
18		chpg 28927	. . . . . . . . 9 class hpG
19	6, 18	cfv 6521	. . . . . . . 8 class (hpG‘𝑔)
20	12, 19	cfv 6521	. . . . . . 7 class ((hpG‘𝑔)‘𝑎)
21	16, 17, 20	wbr 5100	. . . . . 6 wff 𝑥((hpG‘𝑔)‘𝑎)𝑟
22		vt	. . . . . . . . 9 setvar 𝑡
23	22	cv 1559	. . . . . . . 8 class 𝑡
24		citv 28599	. . . . . . . . . 10 class Itv
25	6, 24	cfv 6521	. . . . . . . . 9 class (Itv‘𝑔)
26	16, 17, 25	co 7396	. . . . . . . 8 class (𝑥(Itv‘𝑔)𝑟)
27	23, 26	wcel 2142	. . . . . . 7 wff 𝑡 ∈ (𝑥(Itv‘𝑔)𝑟)
28	27, 22, 12	wrex 3086	. . . . . 6 wff ∃𝑡 ∈ 𝑎 𝑡 ∈ (𝑥(Itv‘𝑔)𝑟)
29	15, 21, 28	w3o 1097	. . . . 5 wff (𝑥 ∈ 𝑎 ∨ 𝑥((hpG‘𝑔)‘𝑎)𝑟 ∨ ∃𝑡 ∈ 𝑎 𝑡 ∈ (𝑥(Itv‘𝑔)𝑟))
30	29, 14, 11	crab 3414	. . . 4 class {𝑥 ∈ (Base‘𝑔) ∣ (𝑥 ∈ 𝑎 ∨ 𝑥((hpG‘𝑔)‘𝑎)𝑟 ∨ ∃𝑡 ∈ 𝑎 𝑡 ∈ (𝑥(Itv‘𝑔)𝑟))}
31	4, 5, 9, 13, 30	cmpo 7398	. . 3 class (𝑎 ∈ ran (LineG‘𝑔), 𝑟 ∈ ((Base‘𝑔) ∖ 𝑎) ↦ {𝑥 ∈ (Base‘𝑔) ∣ (𝑥 ∈ 𝑎 ∨ 𝑥((hpG‘𝑔)‘𝑎)𝑟 ∨ ∃𝑡 ∈ 𝑎 𝑡 ∈ (𝑥(Itv‘𝑔)𝑟))})
32	2, 3, 31	cmpt 5181	. 2 class (𝑔 ∈ V ↦ (𝑎 ∈ ran (LineG‘𝑔), 𝑟 ∈ ((Base‘𝑔) ∖ 𝑎) ↦ {𝑥 ∈ (Base‘𝑔) ∣ (𝑥 ∈ 𝑎 ∨ 𝑥((hpG‘𝑔)‘𝑎)𝑟 ∨ ∃𝑡 ∈ 𝑎 𝑡 ∈ (𝑥(Itv‘𝑔)𝑟))}))
33	1, 32	wceq 1560	1 wff hlG = (𝑔 ∈ V ↦ (𝑎 ∈ ran (LineG‘𝑔), 𝑟 ∈ ((Base‘𝑔) ∖ 𝑎) ↦ {𝑥 ∈ (Base‘𝑔) ∣ (𝑥 ∈ 𝑎 ∨ 𝑥((hpG‘𝑔)‘𝑎)𝑟 ∨ ∃𝑡 ∈ 𝑎 𝑡 ∈ (𝑥(Itv‘𝑔)𝑟))}))

This definition is referenced by:  tgplnfn  28979  plngval  28981  isplng  28982