Metamath Proof Explorer

Definition df-prjcrv

Description: Define the projective curve function. This takes a homogeneous polynomial and outputs the homogeneous coordinates where the polynomial evaluates to zero (the "zero set"). (In other words, scalar multiples are collapsed into the same projective point. See mhphf4 and prjspvs ). (Contributed by SN, 23-Nov-2024)

Ref Expression
Assertion df-prjcrv 
|- PrjCrv = ( n e. NN0 , k e. Field |-> ( f e. U. ran ( ( 0 ... n ) mHomP k ) |-> { p e. ( n PrjSpn k ) | ( ( ( ( 0 ... n ) eval k ) ` f ) " p ) = { ( 0g ` k ) } } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cprjcrv 
 |-  PrjCrv
1 vn 
 |-  n
2 cn0 
 |-  NN0
3 vk 
 |-  k
4 cfield 
 |-  Field
5 vf 
 |-  f
6 cc0 
 |-  0
7 cfz 
 |-  ...
8 1 cv 
 |-  n
9 6 8 7 co 
 |-  ( 0 ... n )
10 cmhp 
 |-  mHomP
11 3 cv 
 |-  k
12 9 11 10 co 
 |-  ( ( 0 ... n ) mHomP k )
13 12 crn 
 |-  ran ( ( 0 ... n ) mHomP k )
14 13 cuni 
 |-  U. ran ( ( 0 ... n ) mHomP k )
15 vp 
 |-  p
16 cprjspn 
 |-  PrjSpn
17 8 11 16 co 
 |-  ( n PrjSpn k )
18 cevl 
 |-  eval
19 9 11 18 co 
 |-  ( ( 0 ... n ) eval k )
20 5 cv 
 |-  f
21 20 19 cfv 
 |-  ( ( ( 0 ... n ) eval k ) ` f )
22 15 cv 
 |-  p
23 21 22 cima 
 |-  ( ( ( ( 0 ... n ) eval k ) ` f ) " p )
24 c0g 
 |-  0g
25 11 24 cfv 
 |-  ( 0g ` k )
26 25 csn 
 |-  { ( 0g ` k ) }
27 23 26 wceq 
 |-  ( ( ( ( 0 ... n ) eval k ) ` f ) " p ) = { ( 0g ` k ) }
28 27 15 17 crab 
 |-  { p e. ( n PrjSpn k ) | ( ( ( ( 0 ... n ) eval k ) ` f ) " p ) = { ( 0g ` k ) } }
29 5 14 28 cmpt 
 |-  ( f e. U. ran ( ( 0 ... n ) mHomP k ) |-> { p e. ( n PrjSpn k ) | ( ( ( ( 0 ... n ) eval k ) ` f ) " p ) = { ( 0g ` k ) } } )
30 1 3 2 4 29 cmpo 
 |-  ( n e. NN0 , k e. Field |-> ( f e. U. ran ( ( 0 ... n ) mHomP k ) |-> { p e. ( n PrjSpn k ) | ( ( ( ( 0 ... n ) eval k ) ` f ) " p ) = { ( 0g ` k ) } } ) )
31 0 30 wceq 
 |-  PrjCrv = ( n e. NN0 , k e. Field |-> ( f e. U. ran ( ( 0 ... n ) mHomP k ) |-> { p e. ( n PrjSpn k ) | ( ( ( ( 0 ... n ) eval k ) ` f ) " p ) = { ( 0g ` k ) } } ) )