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	⊢ hlG = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) , 𝑟 ∈ ( ( Base ‘ 𝑔 ) ∖ 𝑎 ) ↦ { 𝑥 ∈ ( Base ‘ 𝑔 ) ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cplng	⊢ hlG
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		va	⊢ 𝑎
4		clng	⊢ LineG
5	1	cv	⊢ 𝑔
6	5 4	cfv	⊢ ( LineG ‘ 𝑔 )
7	6	crn	⊢ ran ( LineG ‘ 𝑔 )
8		vr	⊢ 𝑟
9		cbs	⊢ Base
10	5 9	cfv	⊢ ( Base ‘ 𝑔 )
11	3	cv	⊢ 𝑎
12	10 11	cdif	⊢ ( ( Base ‘ 𝑔 ) ∖ 𝑎 )
13		vx	⊢ 𝑥
14	13	cv	⊢ 𝑥
15	14 11	wcel	⊢ 𝑥 ∈ 𝑎
16		chpg	⊢ hpG
17	5 16	cfv	⊢ ( hpG ‘ 𝑔 )
18	11 17	cfv	⊢ ( ( hpG ‘ 𝑔 ) ‘ 𝑎 )
19	8	cv	⊢ 𝑟
20	14 19 18	wbr	⊢ 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟
21		vt	⊢ 𝑡
22	21	cv	⊢ 𝑡
23		citv	⊢ Itv
24	5 23	cfv	⊢ ( Itv ‘ 𝑔 )
25	14 19 24	co	⊢ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 )
26	22 25	wcel	⊢ 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 )
27	26 21 11	wrex	⊢ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 )
28	15 20 27	w3o	⊢ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) )
29	28 13 10	crab	⊢ { 𝑥 ∈ ( Base ‘ 𝑔 ) ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ) }
30	3 8 7 12 29	cmpo	⊢ ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) , 𝑟 ∈ ( ( Base ‘ 𝑔 ) ∖ 𝑎 ) ↦ { 𝑥 ∈ ( Base ‘ 𝑔 ) ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ) } )
31	1 2 30	cmpt	⊢ ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) , 𝑟 ∈ ( ( Base ‘ 𝑔 ) ∖ 𝑎 ) ↦ { 𝑥 ∈ ( Base ‘ 𝑔 ) ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ) } ) )
32	0 31	wceq	⊢ hlG = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) , 𝑟 ∈ ( ( Base ‘ 𝑔 ) ∖ 𝑎 ) ↦ { 𝑥 ∈ ( Base ‘ 𝑔 ) ∣ ( 𝑥 ∈ 𝑎 ∨ 𝑥 ( ( hpG ‘ 𝑔 ) ‘ 𝑎 ) 𝑟 ∨ ∃ 𝑡 ∈ 𝑎 𝑡 ∈ ( 𝑥 ( Itv ‘ 𝑔 ) 𝑟 ) ) } ) )