Metamath Proof Explorer

Definition df-prjcrv

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

Ref Expression
Assertion df-prjcrv ⊢ PrjCrv = n ∈ ℕ 0 , k ∈ Field ⟼ f ∈ ⋃ ran ⁡ 0 … n mHomP k ⟼ p ∈ n ℙ𝕣𝕠𝕛 n k | 0 … n eval k ⁡ f p = 0 k

Detailed syntax breakdown

Step Hyp Ref Expression
0 cprjcrv class PrjCrv
1 vn setvar n
2 cn0 class ℕ 0
3 vk setvar k
4 cfield class Field
5 vf setvar f
6 cc0 class 0
7 cfz class …
8 1 cv setvar n
9 6 8 7 co class 0 … n
10 cmhp class mHomP
11 3 cv setvar k
12 9 11 10 co class 0 … n mHomP k
13 12 crn class ran ⁡ 0 … n mHomP k
14 13 cuni class ⋃ ran ⁡ 0 … n mHomP k
15 vp setvar p
16 cprjspn class ℙ𝕣𝕠𝕛 n
17 8 11 16 co class n ℙ𝕣𝕠𝕛 n k
18 cevl class eval
19 9 11 18 co class 0 … n eval k
20 5 cv setvar f
21 20 19 cfv class 0 … n eval k ⁡ f
22 15 cv setvar p
23 21 22 cima class 0 … n eval k ⁡ f p
24 c0g class 0 𝑔
25 11 24 cfv class 0 k
26 25 csn class 0 k
27 23 26 wceq wff 0 … n eval k ⁡ f p = 0 k
28 27 15 17 crab class p ∈ n ℙ𝕣𝕠𝕛 n k | 0 … n eval k ⁡ f p = 0 k
29 5 14 28 cmpt class f ∈ ⋃ ran ⁡ 0 … n mHomP k ⟼ p ∈ n ℙ𝕣𝕠𝕛 n k | 0 … n eval k ⁡ f p = 0 k
30 1 3 2 4 29 cmpo class n ∈ ℕ 0 , k ∈ Field ⟼ f ∈ ⋃ ran ⁡ 0 … n mHomP k ⟼ p ∈ n ℙ𝕣𝕠𝕛 n k | 0 … n eval k ⁡ f p = 0 k
31 0 30 wceq wff PrjCrv = n ∈ ℕ 0 , k ∈ Field ⟼ f ∈ ⋃ ran ⁡ 0 … n mHomP k ⟼ p ∈ n ℙ𝕣𝕠𝕛 n k | 0 … n eval k ⁡ f p = 0 k