Definition df-prjcrv 40456

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 40277 and prjspvs 40438). (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 40455	. 2 class ℙ𝕣𝕠𝕛Crv
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12225	. . 3 class ℕ0
5		cfield 19982	. . 3 class Field
6		vf	. . . 4 setvar 𝑓
7		cc0 10864	. . . . . . . 8 class 0
8	2	cv 1541	. . . . . . . 8 class 𝑛
9		cfz 13230	. . . . . . . 8 class ...
10	7, 8, 9	co 7269	. . . . . . 7 class (0...𝑛)
11	3	cv 1541	. . . . . . 7 class 𝑘
12		cmhp 21309	. . . . . . 7 class mHomP
13	10, 11, 12	co 7269	. . . . . 6 class ((0...𝑛) mHomP 𝑘)
14	13	crn 5590	. . . . 5 class ran ((0...𝑛) mHomP 𝑘)
15	14	cuni 4845	. . . 4 class ∪ ran ((0...𝑛) mHomP 𝑘)
16	6	cv 1541	. . . . . . . 8 class 𝑓
17		cevl 21271	. . . . . . . . 9 class eval
18	10, 11, 17	co 7269	. . . . . . . 8 class ((0...𝑛) eval 𝑘)
19	16, 18	cfv 6431	. . . . . . 7 class (((0...𝑛) eval 𝑘)‘𝑓)
20		vp	. . . . . . . 8 setvar 𝑝
21	20	cv 1541	. . . . . . 7 class 𝑝
22	19, 21	cima 5592	. . . . . 6 class ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝)
23		c0g 17140	. . . . . . . 8 class 0g
24	11, 23	cfv 6431	. . . . . . 7 class (0g‘𝑘)
25	24	csn 4567	. . . . . 6 class {(0g‘𝑘)}
26	22, 25	wceq 1542	. . . . 5 wff ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}
27		cprjspn 40442	. . . . . 6 class ℙ𝕣𝕠𝕛n
28	8, 11, 27	co 7269	. . . . 5 class (𝑛ℙ𝕣𝕠𝕛n𝑘)
29	26, 20, 28	crab 3070	. . . 4 class {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}
30	6, 15, 29	cmpt 5162	. . 3 class (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}})
31	2, 3, 4, 5, 30	cmpo 7271	. 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  40457