Metamath Proof Explorer

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cplng 
 |-  PlnG
1 vg 
 |-  g
2 cvv 
 |-  _V
3 va 
 |-  a
4 clng 
 |-  LineG
5 1 cv 
 |-  g
6 5 4 cfv 
 |-  ( LineG ` g )
7 6 crn 
 |-  ran ( LineG ` g )
8 vr 
 |-  r
9 cbs 
 |-  Base
10 5 9 cfv 
 |-  ( Base ` g )
11 3 cv 
 |-  a
12 10 11 cdif 
 |-  ( ( Base ` g ) \ a )
13 vx 
 |-  x
14 13 cv 
 |-  x
15 14 11 wcel 
 |-  x e. a
16 chpg 
 |-  hpG
17 5 16 cfv 
 |-  ( hpG ` g )
18 11 17 cfv 
 |-  ( ( hpG ` g ) ` a )
19 8 cv 
 |-  r
20 14 19 18 wbr 
 |-  x ( ( hpG ` g ) ` a ) r
21 vt 
 |-  t
22 21 cv 
 |-  t
23 citv 
 |-  Itv
24 5 23 cfv 
 |-  ( Itv ` g )
25 14 19 24 co 
 |-  ( x ( Itv ` g ) r )
26 22 25 wcel 
 |-  t e. ( x ( Itv ` g ) r )
27 26 21 11 wrex 
 |-  E. t e. a t e. ( x ( Itv ` g ) r )
28 15 20 27 w3o 
 |-  ( x e. a \/ x ( ( hpG ` g ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` g ) r ) )
29 28 13 10 crab 
 |-  { x e. ( Base ` g ) | ( x e. a \/ x ( ( hpG ` g ) ` a ) r \/ E. t e. a t e. ( x ( Itv ` g ) r ) ) }
30 3 8 7 12 29 cmpo 
 |-  ( 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 ) ) } )
31 1 2 30 cmpt 
 |-  ( 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 ) ) } ) )
32 0 31 wceq 
 |-  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 ) ) } ) )