Definition df-prjcrv 43759

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 43721 and prjspvs 43731). (Contributed by SN, 23-Nov-2024.)

Assertion

Ref	Expression
df-prjcrv	⊢ ℙrojCrv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛 ℙrojn 𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))

Distinct variable group:   𝑘,𝑛,𝑓,𝑝

Detailed syntax breakdown of Definition df-prjcrv

Step	Hyp	Ref	Expression
1		cprjcrv 43758	. 2 class ℙrojCrv
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12609	. . 3 class ℕ0
5		cfield 20986	. . 3 class Field
6		vf	. . . 4 setvar 𝑓
7		cc0 11203	. . . . . . . 8 class 0
8	2	cv 1568	. . . . . . . 8 class 𝑛
9		cfz 13642	. . . . . . . 8 class ...
10	7, 8, 9	co 7420	. . . . . . 7 class (0...𝑛)
11	3	cv 1568	. . . . . . 7 class 𝑘
12		cmhp 22459	. . . . . . 7 class mHomP
13	10, 11, 12	co 7420	. . . . . 6 class ((0...𝑛) mHomP 𝑘)
14	13	crn 5651	. . . . 5 class ran ((0...𝑛) mHomP 𝑘)
15	14	cuni 4866	. . . 4 class ∪ ran ((0...𝑛) mHomP 𝑘)
16	6	cv 1568	. . . . . . . 8 class 𝑓
17		cevl 22387	. . . . . . . . 9 class eval
18	10, 11, 17	co 7420	. . . . . . . 8 class ((0...𝑛) eval 𝑘)
19	16, 18	cfv 6538	. . . . . . 7 class (((0...𝑛) eval 𝑘)‘𝑓)
20		vp	. . . . . . . 8 setvar 𝑝
21	20	cv 1568	. . . . . . 7 class 𝑝
22	19, 21	cima 5653	. . . . . 6 class ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝)
23		c0g 17615	. . . . . . . 8 class 0g
24	11, 23	cfv 6538	. . . . . . 7 class (0g‘𝑘)
25	24	csn 4584	. . . . . 6 class {(0g‘𝑘)}
26	22, 25	wceq 1569	. . . . 5 wff ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}
27		cprjspn 43735	. . . . . 6 class ℙrojn
28	8, 11, 27	co 7420	. . . . 5 class (𝑛 ℙrojn 𝑘)
29	26, 20, 28	crab 3412	. . . 4 class {𝑝 ∈ (𝑛 ℙrojn 𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}
30	6, 15, 29	cmpt 5185	. . 3 class (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛 ℙrojn 𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}})
31	2, 3, 4, 5, 30	cmpo 7422	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛 ℙrojn 𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))
32	1, 31	wceq 1569	1 wff ℙrojCrv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛 ℙrojn 𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))

This definition is used by:  prjcrvfval  43760