Definition df-prjcrv 43870

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 43832 and prjspvs 43842). (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 43869	. 2 class ℙrojCrv
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12636	. . 3 class ℕ0
5		cfield 21014	. . 3 class Field
6		vf	. . . 4 setvar 𝑓
7		cc0 11230	. . . . . . . 8 class 0
8	2	cv 1569	. . . . . . . 8 class 𝑛
9		cfz 13669	. . . . . . . 8 class ...
10	7, 8, 9	co 7446	. . . . . . 7 class (0...𝑛)
11	3	cv 1569	. . . . . . 7 class 𝑘
12		cmhp 22487	. . . . . . 7 class mHomP
13	10, 11, 12	co 7446	. . . . . 6 class ((0...𝑛) mHomP 𝑘)
14	13	crn 5657	. . . . 5 class ran ((0...𝑛) mHomP 𝑘)
15	14	cuni 4870	. . . 4 class ∪ ran ((0...𝑛) mHomP 𝑘)
16	6	cv 1569	. . . . . . . 8 class 𝑓
17		cevl 22415	. . . . . . . . 9 class eval
18	10, 11, 17	co 7446	. . . . . . . 8 class ((0...𝑛) eval 𝑘)
19	16, 18	cfv 6561	. . . . . . 7 class (((0...𝑛) eval 𝑘)‘𝑓)
20		vp	. . . . . . . 8 setvar 𝑝
21	20	cv 1569	. . . . . . 7 class 𝑝
22	19, 21	cima 5659	. . . . . 6 class ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝)
23		c0g 17642	. . . . . . . 8 class 0g
24	11, 23	cfv 6561	. . . . . . 7 class (0g‘𝑘)
25	24	csn 4588	. . . . . 6 class {(0g‘𝑘)}
26	22, 25	wceq 1570	. . . . 5 wff ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}
27		cprjspn 43846	. . . . . 6 class ℙrojn
28	8, 11, 27	co 7446	. . . . 5 class (𝑛 ℙrojn 𝑘)
29	26, 20, 28	crab 3416	. . . 4 class {𝑝 ∈ (𝑛 ℙrojn 𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}
30	6, 15, 29	cmpt 5190	. . 3 class (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛 ℙrojn 𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}})
31	2, 3, 4, 5, 30	cmpo 7448	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛 ℙrojn 𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))
32	1, 31	wceq 1570	1 wff ℙrojCrv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ∈ ∪ ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛 ℙrojn 𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g‘𝑘)}}))

This definition is used by:  prjcrvfval  43871