Definition df-prjcrv 43403

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 43373 and prjspvs 43383). (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 43402	. 2 class ℙ𝕣𝕠𝕛Crv
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12522	. . 3 class ℕ0
5		cfield 20865	. . 3 class Field
6		vf	. . . 4 setvar 𝑓
7		cc0 11118	. . . . . . . 8 class 0
8	2	cv 1569	. . . . . . . 8 class 𝑛
9		cfz 13553	. . . . . . . 8 class ...
10	7, 8, 9	co 7423	. . . . . . 7 class (0...𝑛)
11	3	cv 1569	. . . . . . 7 class 𝑘
12		cmhp 22333	. . . . . . 7 class mHomP
13	10, 11, 12	co 7423	. . . . . 6 class ((0...𝑛) mHomP 𝑘)
14	13	crn 5667	. . . . 5 class ran ((0...𝑛) mHomP 𝑘)
15	14	cuni 4877	. . . 4 class ∪ ran ((0...𝑛) mHomP 𝑘)
16	6	cv 1569	. . . . . . . 8 class 𝑓
17		cevl 22261	. . . . . . . . 9 class eval
18	10, 11, 17	co 7423	. . . . . . . 8 class ((0...𝑛) eval 𝑘)
19	16, 18	cfv 6543	. . . . . . 7 class (((0...𝑛) eval 𝑘)‘𝑓)
20		vp	. . . . . . . 8 setvar 𝑝
21	20	cv 1569	. . . . . . 7 class 𝑝
22	19, 21	cima 5669	. . . . . 6 class ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝)
23		c0g 17517	. . . . . . . 8 class 0g
24	11, 23	cfv 6543	. . . . . . 7 class (0g‘𝑘)
25	24	csn 4594	. . . . . 6 class {(0g‘𝑘)}
26	22, 25	wceq 1570	. . . . 5 wff ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}
27		cprjspn 43387	. . . . . 6 class ℙ𝕣𝕠𝕛n
28	8, 11, 27	co 7423	. . . . 5 class (𝑛ℙ𝕣𝕠𝕛n𝑘)
29	26, 20, 28	crab 3419	. . . 4 class {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}
30	6, 15, 29	cmpt 5197	. . 3 class (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}})
31	2, 3, 4, 5, 30	cmpo 7425	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))
32	1, 31	wceq 1570	1 wff ℙ𝕣𝕠𝕛Crv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))

This definition is used by:  prjcrvfval  43404