Definition df-prjcrv 43093

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 43063 and prjspvs 43073). (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 43092	. 2 class ℙ𝕣𝕠𝕛Crv
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12432	. . 3 class ℕ0
5		cfield 20705	. . 3 class Field
6		vf	. . . 4 setvar 𝑓
7		cc0 11034	. . . . . . . 8 class 0
8	2	cv 1547	. . . . . . . 8 class 𝑛
9		cfz 13456	. . . . . . . 8 class ...
10	7, 8, 9	co 7359	. . . . . . 7 class (0...𝑛)
11	3	cv 1547	. . . . . . 7 class 𝑘
12		cmhp 22124	. . . . . . 7 class mHomP
13	10, 11, 12	co 7359	. . . . . 6 class ((0...𝑛) mHomP 𝑘)
14	13	crn 5621	. . . . 5 class ran ((0...𝑛) mHomP 𝑘)
15	14	cuni 4840	. . . 4 class ∪ ran ((0...𝑛) mHomP 𝑘)
16	6	cv 1547	. . . . . . . 8 class 𝑓
17		cevl 22052	. . . . . . . . 9 class eval
18	10, 11, 17	co 7359	. . . . . . . 8 class ((0...𝑛) eval 𝑘)
19	16, 18	cfv 6488	. . . . . . 7 class (((0...𝑛) eval 𝑘)‘𝑓)
20		vp	. . . . . . . 8 setvar 𝑝
21	20	cv 1547	. . . . . . 7 class 𝑝
22	19, 21	cima 5623	. . . . . 6 class ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝)
23		c0g 17397	. . . . . . . 8 class 0g
24	11, 23	cfv 6488	. . . . . . 7 class (0g‘𝑘)
25	24	csn 4557	. . . . . 6 class {(0g‘𝑘)}
26	22, 25	wceq 1548	. . . . 5 wff ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}
27		cprjspn 43077	. . . . . 6 class ℙ𝕣𝕠𝕛n
28	8, 11, 27	co 7359	. . . . 5 class (𝑛ℙ𝕣𝕠𝕛n𝑘)
29	26, 20, 28	crab 3393	. . . 4 class {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}
30	6, 15, 29	cmpt 5155	. . 3 class (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}})
31	2, 3, 4, 5, 30	cmpo 7361	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))
32	1, 31	wceq 1548	1 wff ℙ𝕣𝕠𝕛Crv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))

This definition is referenced by:  prjcrvfval  43094