Definition df-prjcrv 40662

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 40483 and prjspvs 40644). (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 40661	. 2 class ℙ𝕣𝕠𝕛Crv
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12283	. . 3 class ℕ0
5		cfield 20041	. . 3 class Field
6		vf	. . . 4 setvar 𝑓
7		cc0 10921	. . . . . . . 8 class 0
8	2	cv 1538	. . . . . . . 8 class 𝑛
9		cfz 13289	. . . . . . . 8 class ...
10	7, 8, 9	co 7307	. . . . . . 7 class (0...𝑛)
11	3	cv 1538	. . . . . . 7 class 𝑘
12		cmhp 21368	. . . . . . 7 class mHomP
13	10, 11, 12	co 7307	. . . . . 6 class ((0...𝑛) mHomP 𝑘)
14	13	crn 5601	. . . . 5 class ran ((0...𝑛) mHomP 𝑘)
15	14	cuni 4844	. . . 4 class ∪ ran ((0...𝑛) mHomP 𝑘)
16	6	cv 1538	. . . . . . . 8 class 𝑓
17		cevl 21330	. . . . . . . . 9 class eval
18	10, 11, 17	co 7307	. . . . . . . 8 class ((0...𝑛) eval 𝑘)
19	16, 18	cfv 6458	. . . . . . 7 class (((0...𝑛) eval 𝑘)‘𝑓)
20		vp	. . . . . . . 8 setvar 𝑝
21	20	cv 1538	. . . . . . 7 class 𝑝
22	19, 21	cima 5603	. . . . . 6 class ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝)
23		c0g 17199	. . . . . . . 8 class 0g
24	11, 23	cfv 6458	. . . . . . 7 class (0g‘𝑘)
25	24	csn 4565	. . . . . 6 class {(0g‘𝑘)}
26	22, 25	wceq 1539	. . . . 5 wff ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}
27		cprjspn 40648	. . . . . 6 class ℙ𝕣𝕠𝕛n
28	8, 11, 27	co 7307	. . . . 5 class (𝑛ℙ𝕣𝕠𝕛n𝑘)
29	26, 20, 28	crab 3303	. . . 4 class {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}
30	6, 15, 29	cmpt 5164	. . 3 class (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}})
31	2, 3, 4, 5, 30	cmpo 7309	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))
32	1, 31	wceq 1539	1 wff ℙ𝕣𝕠𝕛Crv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))

This definition is referenced by:  prjcrvfval  40663