Metamath Proof Explorer


Theorem ismhp

Description: Property of being a homogeneous polynomial. (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 ismhp φ X H N X B X 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 8 mhpval φ H N = f B | f supp 0 ˙ g D | fld 𝑠 0 g = N
10 9 eleq2d φ X H N X f B | f supp 0 ˙ g D | fld 𝑠 0 g = N
11 oveq1 f = X f supp 0 ˙ = X supp 0 ˙
12 11 sseq1d f = X f supp 0 ˙ g D | fld 𝑠 0 g = N X supp 0 ˙ g D | fld 𝑠 0 g = N
13 12 elrab X f B | f supp 0 ˙ g D | fld 𝑠 0 g = N X B X supp 0 ˙ g D | fld 𝑠 0 g = N
14 10 13 bitrdi φ X H N X B X supp 0 ˙ g D | fld 𝑠 0 g = N