Definition df-prjcrv 42585

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 42555 and prjspvs 42565). (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 42584	. 2 class ℙ𝕣𝕠𝕛Crv
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12553	. . 3 class ℕ0
5		cfield 20752	. . 3 class Field
6		vf	. . . 4 setvar 𝑓
7		cc0 11184	. . . . . . . 8 class 0
8	2	cv 1536	. . . . . . . 8 class 𝑛
9		cfz 13567	. . . . . . . 8 class ...
10	7, 8, 9	co 7448	. . . . . . 7 class (0...𝑛)
11	3	cv 1536	. . . . . . 7 class 𝑘
12		cmhp 22156	. . . . . . 7 class mHomP
13	10, 11, 12	co 7448	. . . . . 6 class ((0...𝑛) mHomP 𝑘)
14	13	crn 5701	. . . . 5 class ran ((0...𝑛) mHomP 𝑘)
15	14	cuni 4931	. . . 4 class ∪ ran ((0...𝑛) mHomP 𝑘)
16	6	cv 1536	. . . . . . . 8 class 𝑓
17		cevl 22120	. . . . . . . . 9 class eval
18	10, 11, 17	co 7448	. . . . . . . 8 class ((0...𝑛) eval 𝑘)
19	16, 18	cfv 6573	. . . . . . 7 class (((0...𝑛) eval 𝑘)‘𝑓)
20		vp	. . . . . . . 8 setvar 𝑝
21	20	cv 1536	. . . . . . 7 class 𝑝
22	19, 21	cima 5703	. . . . . 6 class ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝)
23		c0g 17499	. . . . . . . 8 class 0g
24	11, 23	cfv 6573	. . . . . . 7 class (0g‘𝑘)
25	24	csn 4648	. . . . . 6 class {(0g‘𝑘)}
26	22, 25	wceq 1537	. . . . 5 wff ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}
27		cprjspn 42569	. . . . . 6 class ℙ𝕣𝕠𝕛n
28	8, 11, 27	co 7448	. . . . 5 class (𝑛ℙ𝕣𝕠𝕛n𝑘)
29	26, 20, 28	crab 3443	. . . 4 class {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}
30	6, 15, 29	cmpt 5249	. . 3 class (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}})
31	2, 3, 4, 5, 30	cmpo 7450	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))
32	1, 31	wceq 1537	1 wff ℙ𝕣𝕠𝕛Crv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))

This definition is referenced by:  prjcrvfval  42586