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=ImHomPR
mhpfval.p P=ImPolyR
mhpfval.b B=BaseP
mhpfval.0 0˙=0R
mhpfval.d D=h0I|h-1Fin
mhpfval.i φIV
mhpfval.r φRW
mhpval.n φN0
Assertion ismhp φXHNXBXsupp0˙gD|fld𝑠0g=N

Proof

Step Hyp Ref Expression
1 mhpfval.h H=ImHomPR
2 mhpfval.p P=ImPolyR
3 mhpfval.b B=BaseP
4 mhpfval.0 0˙=0R
5 mhpfval.d D=h0I|h-1Fin
6 mhpfval.i φIV
7 mhpfval.r φRW
8 mhpval.n φN0
9 1 2 3 4 5 6 7 8 mhpval φHN=fB|fsupp0˙gD|fld𝑠0g=N
10 9 eleq2d φXHNXfB|fsupp0˙gD|fld𝑠0g=N
11 oveq1 f=Xfsupp0˙=Xsupp0˙
12 11 sseq1d f=Xfsupp0˙gD|fld𝑠0g=NXsupp0˙gD|fld𝑠0g=N
13 12 elrab XfB|fsupp0˙gD|fld𝑠0g=NXBXsupp0˙gD|fld𝑠0g=N
14 10 13 bitrdi φXHNXBXsupp0˙gD|fld𝑠0g=N