Definition df-prjcrv 43224

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 43194 and prjspvs 43204). (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 43223	. 2 class ℙ𝕣𝕠𝕛Crv
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12495	. . 3 class ℕ0
5		cfield 20805	. . 3 class Field
6		vf	. . . 4 setvar 𝑓
7		cc0 11088	. . . . . . . 8 class 0
8	2	cv 1562	. . . . . . . 8 class 𝑛
9		cfz 13526	. . . . . . . 8 class ...
10	7, 8, 9	co 7400	. . . . . . 7 class (0...𝑛)
11	3	cv 1562	. . . . . . 7 class 𝑘
12		cmhp 22256	. . . . . . 7 class mHomP
13	10, 11, 12	co 7400	. . . . . 6 class ((0...𝑛) mHomP 𝑘)
14	13	crn 5653	. . . . 5 class ran ((0...𝑛) mHomP 𝑘)
15	14	cuni 4868	. . . 4 class ∪ ran ((0...𝑛) mHomP 𝑘)
16	6	cv 1562	. . . . . . . 8 class 𝑓
17		cevl 22184	. . . . . . . . 9 class eval
18	10, 11, 17	co 7400	. . . . . . . 8 class ((0...𝑛) eval 𝑘)
19	16, 18	cfv 6525	. . . . . . 7 class (((0...𝑛) eval 𝑘)‘𝑓)
20		vp	. . . . . . . 8 setvar 𝑝
21	20	cv 1562	. . . . . . 7 class 𝑝
22	19, 21	cima 5655	. . . . . 6 class ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝)
23		c0g 17482	. . . . . . . 8 class 0g
24	11, 23	cfv 6525	. . . . . . 7 class (0g‘𝑘)
25	24	csn 4585	. . . . . 6 class {(0g‘𝑘)}
26	22, 25	wceq 1563	. . . . 5 wff ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}
27		cprjspn 43208	. . . . . 6 class ℙ𝕣𝕠𝕛n
28	8, 11, 27	co 7400	. . . . 5 class (𝑛ℙ𝕣𝕠𝕛n𝑘)
29	26, 20, 28	crab 3417	. . . 4 class {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}
30	6, 15, 29	cmpt 5186	. . 3 class (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}})
31	2, 3, 4, 5, 30	cmpo 7402	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))
32	1, 31	wceq 1563	1 wff ℙ𝕣𝕠𝕛Crv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))

This definition is referenced by:  prjcrvfval  43225