Definition df-prjcrv 42620

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 42590 and prjspvs 42600). (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 42619	. 2 class ℙ𝕣𝕠𝕛Crv
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12372	. . 3 class ℕ0
5		cfield 20599	. . 3 class Field
6		vf	. . . 4 setvar 𝑓
7		cc0 10997	. . . . . . . 8 class 0
8	2	cv 1539	. . . . . . . 8 class 𝑛
9		cfz 13398	. . . . . . . 8 class ...
10	7, 8, 9	co 7340	. . . . . . 7 class (0...𝑛)
11	3	cv 1539	. . . . . . 7 class 𝑘
12		cmhp 21998	. . . . . . 7 class mHomP
13	10, 11, 12	co 7340	. . . . . 6 class ((0...𝑛) mHomP 𝑘)
14	13	crn 5614	. . . . 5 class ran ((0...𝑛) mHomP 𝑘)
15	14	cuni 4856	. . . 4 class ∪ ran ((0...𝑛) mHomP 𝑘)
16	6	cv 1539	. . . . . . . 8 class 𝑓
17		cevl 21962	. . . . . . . . 9 class eval
18	10, 11, 17	co 7340	. . . . . . . 8 class ((0...𝑛) eval 𝑘)
19	16, 18	cfv 6476	. . . . . . 7 class (((0...𝑛) eval 𝑘)‘𝑓)
20		vp	. . . . . . . 8 setvar 𝑝
21	20	cv 1539	. . . . . . 7 class 𝑝
22	19, 21	cima 5616	. . . . . 6 class ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝)
23		c0g 17330	. . . . . . . 8 class 0g
24	11, 23	cfv 6476	. . . . . . 7 class (0g‘𝑘)
25	24	csn 4573	. . . . . 6 class {(0g‘𝑘)}
26	22, 25	wceq 1540	. . . . 5 wff ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}
27		cprjspn 42604	. . . . . 6 class ℙ𝕣𝕠𝕛n
28	8, 11, 27	co 7340	. . . . 5 class (𝑛ℙ𝕣𝕠𝕛n𝑘)
29	26, 20, 28	crab 3392	. . . 4 class {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}
30	6, 15, 29	cmpt 5169	. . 3 class (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}})
31	2, 3, 4, 5, 30	cmpo 7342	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))
32	1, 31	wceq 1540	1 wff ℙ𝕣𝕠𝕛Crv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))

This definition is referenced by:  prjcrvfval  42621