Definition df-prjcrv 43087

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 43057 and prjspvs 43067). (Contributed by SN, 23-Nov-2024.)

Assertion

Ref	Expression
df-prjcrv	⊢ ℙ𝕣𝕠𝕛Crv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))

Distinct variable group:   𝑘,𝑛,𝑓,𝑝

Detailed syntax breakdown of Definition df-prjcrv

Step	Hyp	Ref	Expression
1		cprjcrv 43086	. 2 class ℙ𝕣𝕠𝕛Crv
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12435	. . 3 class ℕ0
5		cfield 20709	. . 3 class Field
6		vf	. . . 4 setvar 𝑓
7		cc0 11036	. . . . . . . 8 class 0
8	2	cv 1546	. . . . . . . 8 class 𝑛
9		cfz 13459	. . . . . . . 8 class ...
10	7, 8, 9	co 7363	. . . . . . 7 class (0...𝑛)
11	3	cv 1546	. . . . . . 7 class 𝑘
12		cmhp 22128	. . . . . . 7 class mHomP
13	10, 11, 12	co 7363	. . . . . 6 class ((0...𝑛) mHomP 𝑘)
14	13	crn 5626	. . . . 5 class ran ((0...𝑛) mHomP 𝑘)
15	14	cuni 4845	. . . 4 class ∪ ran ((0...𝑛) mHomP 𝑘)
16	6	cv 1546	. . . . . . . 8 class 𝑓
17		cevl 22056	. . . . . . . . 9 class eval
18	10, 11, 17	co 7363	. . . . . . . 8 class ((0...𝑛) eval 𝑘)
19	16, 18	cfv 6492	. . . . . . 7 class (((0...𝑛) eval 𝑘)‘𝑓)
20		vp	. . . . . . . 8 setvar 𝑝
21	20	cv 1546	. . . . . . 7 class 𝑝
22	19, 21	cima 5628	. . . . . 6 class ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝)
23		c0g 17400	. . . . . . . 8 class 0g
24	11, 23	cfv 6492	. . . . . . 7 class (0g‘𝑘)
25	24	csn 4562	. . . . . 6 class {(0g‘𝑘)}
26	22, 25	wceq 1547	. . . . 5 wff ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}
27		cprjspn 43071	. . . . . 6 class ℙ𝕣𝕠𝕛n
28	8, 11, 27	co 7363	. . . . 5 class (𝑛ℙ𝕣𝕠𝕛n𝑘)
29	26, 20, 28	crab 3392	. . . 4 class {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}
30	6, 15, 29	cmpt 5160	. . 3 class (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}})
31	2, 3, 4, 5, 30	cmpo 7365	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))
32	1, 31	wceq 1547	1 wff ℙ𝕣𝕠𝕛Crv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))

This definition is referenced by:  prjcrvfval  43088