Definition df-prjcrv 41373

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 41174 and prjspvs 41353). (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 41372	. 2 class ℙ𝕣𝕠𝕛Crv
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12471	. . 3 class ℕ0
5		cfield 20357	. . 3 class Field
6		vf	. . . 4 setvar 𝑓
7		cc0 11109	. . . . . . . 8 class 0
8	2	cv 1540	. . . . . . . 8 class 𝑛
9		cfz 13483	. . . . . . . 8 class ...
10	7, 8, 9	co 7408	. . . . . . 7 class (0...𝑛)
11	3	cv 1540	. . . . . . 7 class 𝑘
12		cmhp 21671	. . . . . . 7 class mHomP
13	10, 11, 12	co 7408	. . . . . 6 class ((0...𝑛) mHomP 𝑘)
14	13	crn 5677	. . . . 5 class ran ((0...𝑛) mHomP 𝑘)
15	14	cuni 4908	. . . 4 class ∪ ran ((0...𝑛) mHomP 𝑘)
16	6	cv 1540	. . . . . . . 8 class 𝑓
17		cevl 21633	. . . . . . . . 9 class eval
18	10, 11, 17	co 7408	. . . . . . . 8 class ((0...𝑛) eval 𝑘)
19	16, 18	cfv 6543	. . . . . . 7 class (((0...𝑛) eval 𝑘)‘𝑓)
20		vp	. . . . . . . 8 setvar 𝑝
21	20	cv 1540	. . . . . . 7 class 𝑝
22	19, 21	cima 5679	. . . . . 6 class ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝)
23		c0g 17384	. . . . . . . 8 class 0g
24	11, 23	cfv 6543	. . . . . . 7 class (0g‘𝑘)
25	24	csn 4628	. . . . . 6 class {(0g‘𝑘)}
26	22, 25	wceq 1541	. . . . 5 wff ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}
27		cprjspn 41357	. . . . . 6 class ℙ𝕣𝕠𝕛n
28	8, 11, 27	co 7408	. . . . 5 class (𝑛ℙ𝕣𝕠𝕛n𝑘)
29	26, 20, 28	crab 3432	. . . 4 class {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}
30	6, 15, 29	cmpt 5231	. . 3 class (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}})
31	2, 3, 4, 5, 30	cmpo 7410	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))
32	1, 31	wceq 1541	1 wff ℙ𝕣𝕠𝕛Crv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))

This definition is referenced by:  prjcrvfval  41374