Definition df-prjcrv 43176

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 43146 and prjspvs 43156). (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 43175	. 2 class ℙ𝕣𝕠𝕛Crv
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12478	. . 3 class ℕ0
5		cfield 20759	. . 3 class Field
6		vf	. . . 4 setvar 𝑓
7		cc0 11070	. . . . . . . 8 class 0
8	2	cv 1558	. . . . . . . 8 class 𝑛
9		cfz 13509	. . . . . . . 8 class ...
10	7, 8, 9	co 7392	. . . . . . 7 class (0...𝑛)
11	3	cv 1558	. . . . . . 7 class 𝑘
12		cmhp 22178	. . . . . . 7 class mHomP
13	10, 11, 12	co 7392	. . . . . 6 class ((0...𝑛) mHomP 𝑘)
14	13	crn 5646	. . . . 5 class ran ((0...𝑛) mHomP 𝑘)
15	14	cuni 4864	. . . 4 class ∪ ran ((0...𝑛) mHomP 𝑘)
16	6	cv 1558	. . . . . . . 8 class 𝑓
17		cevl 22106	. . . . . . . . 9 class eval
18	10, 11, 17	co 7392	. . . . . . . 8 class ((0...𝑛) eval 𝑘)
19	16, 18	cfv 6517	. . . . . . 7 class (((0...𝑛) eval 𝑘)‘𝑓)
20		vp	. . . . . . . 8 setvar 𝑝
21	20	cv 1558	. . . . . . 7 class 𝑝
22	19, 21	cima 5648	. . . . . 6 class ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝)
23		c0g 17451	. . . . . . . 8 class 0g
24	11, 23	cfv 6517	. . . . . . 7 class (0g‘𝑘)
25	24	csn 4581	. . . . . 6 class {(0g‘𝑘)}
26	22, 25	wceq 1559	. . . . 5 wff ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}
27		cprjspn 43160	. . . . . 6 class ℙ𝕣𝕠𝕛n
28	8, 11, 27	co 7392	. . . . 5 class (𝑛ℙ𝕣𝕠𝕛n𝑘)
29	26, 20, 28	crab 3413	. . . 4 class {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}
30	6, 15, 29	cmpt 5180	. . 3 class (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}})
31	2, 3, 4, 5, 30	cmpo 7394	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))
32	1, 31	wceq 1559	1 wff ℙ𝕣𝕠𝕛Crv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))

This definition is referenced by:  prjcrvfval  43177