Definition df-prjcrv 41372

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 41172 and prjspvs 41352). (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 41371	. 2 class ℙ𝕣𝕠𝕛Crv
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12472	. . 3 class ℕ0
5		cfield 20358	. . 3 class Field
6		vf	. . . 4 setvar 𝑓
7		cc0 11110	. . . . . . . 8 class 0
8	2	cv 1541	. . . . . . . 8 class 𝑛
9		cfz 13484	. . . . . . . 8 class ...
10	7, 8, 9	co 7409	. . . . . . 7 class (0...𝑛)
11	3	cv 1541	. . . . . . 7 class 𝑘
12		cmhp 21672	. . . . . . 7 class mHomP
13	10, 11, 12	co 7409	. . . . . 6 class ((0...𝑛) mHomP 𝑘)
14	13	crn 5678	. . . . 5 class ran ((0...𝑛) mHomP 𝑘)
15	14	cuni 4909	. . . 4 class ∪ ran ((0...𝑛) mHomP 𝑘)
16	6	cv 1541	. . . . . . . 8 class 𝑓
17		cevl 21634	. . . . . . . . 9 class eval
18	10, 11, 17	co 7409	. . . . . . . 8 class ((0...𝑛) eval 𝑘)
19	16, 18	cfv 6544	. . . . . . 7 class (((0...𝑛) eval 𝑘)‘𝑓)
20		vp	. . . . . . . 8 setvar 𝑝
21	20	cv 1541	. . . . . . 7 class 𝑝
22	19, 21	cima 5680	. . . . . 6 class ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝)
23		c0g 17385	. . . . . . . 8 class 0g
24	11, 23	cfv 6544	. . . . . . 7 class (0g‘𝑘)
25	24	csn 4629	. . . . . 6 class {(0g‘𝑘)}
26	22, 25	wceq 1542	. . . . 5 wff ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}
27		cprjspn 41356	. . . . . 6 class ℙ𝕣𝕠𝕛n
28	8, 11, 27	co 7409	. . . . 5 class (𝑛ℙ𝕣𝕠𝕛n𝑘)
29	26, 20, 28	crab 3433	. . . 4 class {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}
30	6, 15, 29	cmpt 5232	. . 3 class (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}})
31	2, 3, 4, 5, 30	cmpo 7411	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))
32	1, 31	wceq 1542	1 wff ℙ𝕣𝕠𝕛Crv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))

This definition is referenced by:  prjcrvfval  41373