Metamath Proof Explorer


Theorem mhpval

Description: Value of the "homogeneous polynomial" function. (Contributed by Steven Nguyen, 25-Aug-2023)

Ref Expression
Hypotheses mhpfval.h H = I mHomP R
mhpfval.p P = I mPoly R
mhpfval.b B = Base P
mhpfval.0 0 ˙ = 0 R
mhpfval.d D = h 0 I | h -1 Fin
mhpfval.i φ I V
mhpfval.r φ R W
mhpval.n φ N 0
Assertion mhpval φ H N = f B | f supp 0 ˙ g D | fld 𝑠 0 g = N

Proof

Step Hyp Ref Expression
1 mhpfval.h H = I mHomP R
2 mhpfval.p P = I mPoly R
3 mhpfval.b B = Base P
4 mhpfval.0 0 ˙ = 0 R
5 mhpfval.d D = h 0 I | h -1 Fin
6 mhpfval.i φ I V
7 mhpfval.r φ R W
8 mhpval.n φ N 0
9 1 2 3 4 5 6 7 mhpfval φ H = n 0 f B | f supp 0 ˙ g D | fld 𝑠 0 g = n
10 eqeq2 n = N fld 𝑠 0 g = n fld 𝑠 0 g = N
11 10 rabbidv n = N g D | fld 𝑠 0 g = n = g D | fld 𝑠 0 g = N
12 11 sseq2d n = N f supp 0 ˙ g D | fld 𝑠 0 g = n f supp 0 ˙ g D | fld 𝑠 0 g = N
13 12 rabbidv n = N f B | f supp 0 ˙ g D | fld 𝑠 0 g = n = f B | f supp 0 ˙ g D | fld 𝑠 0 g = N
14 13 adantl φ n = N f B | f supp 0 ˙ g D | fld 𝑠 0 g = n = f B | f supp 0 ˙ g D | fld 𝑠 0 g = N
15 3 fvexi B V
16 15 rabex f B | f supp 0 ˙ g D | fld 𝑠 0 g = N V
17 16 a1i φ f B | f supp 0 ˙ g D | fld 𝑠 0 g = N V
18 9 14 8 17 fvmptd φ H N = f B | f supp 0 ˙ g D | fld 𝑠 0 g = N