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	Could not format assertion : No typesetting found for |- 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 ) } } ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprjcrv	Could not format PrjCrv : No typesetting found for class PrjCrv with typecode class
1		vn	$$setvarn$$
2		cn0	$$class{\mathbb{N}}_0$$
3		vk	$$setvark$$
4		cfield	$$class\mathrm{Field}$$
5		vf	$$setvarf$$
6		cc0	$$class0$$
7		cfz	$$class\dots$$
8	1	cv	$$setvarn$$
9	6 8 7	co	$$class\left(0\dots n\right)$$
10		cmhp	$$class\mathrm{mHomP}$$
11	3	cv	$$setvark$$
12	9 11 10	co	$$class\left(\left(0\dots n\right)\mathrm{mHomP}k\right)$$
13	12	crn	$$class\mathrm{ran}\left(\left(0\dots n\right)\mathrm{mHomP}k\right)$$
14	13	cuni	$$class\bigcup \mathrm{ran}\left(\left(0\dots n\right)\mathrm{mHomP}k\right)$$
15		vp	$$setvarp$$
16		cprjspn	$$class{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_n$$
17	8 11 16	co	$$class\left(n{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_{n}k\right)$$
18		cevl	$$class\mathrm{eval}$$
19	9 11 18	co	$$class\left(\left(0\dots n\right)\mathrm{eval}k\right)$$
20	5	cv	$$setvarf$$
21	20 19	cfv	$$class\left(\left(0\dots n\right)\mathrm{eval}k\right)\left(f\right)$$
22	15	cv	$$setvarp$$
23	21 22	cima	$$class\left(\left(0\dots n\right)\mathrm{eval}k\right)\left(f\right)\left[p\right]$$
24		c0g	$$class{0}_{𝑔}$$
25	11 24	cfv	$$class{0}_k$$
26	25	csn	$$class\left\{0_k\right\}$$
27	23 26	wceq	$$wff\left(\left(0\dots n\right)\mathrm{eval}k\right)\left(f\right)\left[p\right]=\left\{0_k\right\}$$
28	27 15 17	crab	$$class\left\{p\in \left(n{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_{n}k\right)|\left(\left(0\dots n\right)\mathrm{eval}k\right)\left(f\right)\left[p\right]=\left\{0_k\right\}\right\}$$
29	5 14 28	cmpt	$$class\left(f\in \bigcup \mathrm{ran}\left(\left(0\dots n\right)\mathrm{mHomP}k\right)⟼\left\{p\in \left(n{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_{n}k\right)|\left(\left(0\dots n\right)\mathrm{eval}k\right)\left(f\right)\left[p\right]=\left\{0_k\right\}\right\}\right)$$
30	1 3 2 4 29	cmpo	$$class\left(n\in {\mathbb{N}}_0,k\in \mathrm{Field}⟼\left(f\in \bigcup \mathrm{ran}\left(\left(0\dots n\right)\mathrm{mHomP}k\right)⟼\left\{p\in \left(n{\mathrm{\mathbb{P}𝕣𝕠𝕛}}_{n}k\right)|\left(\left(0\dots n\right)\mathrm{eval}k\right)\left(f\right)\left[p\right]=\left\{0_k\right\}\right\}\right)\right)$$
31	0 30	wceq	Could not format 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 ) } } ) ) : No typesetting found for wff 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 ) } } ) ) with typecode wff