Metamath Proof Explorer


Theorem mhpmpl

Description: A homogeneous polynomial is a polynomial. (Contributed by Steven Nguyen, 25-Aug-2023)

Ref Expression
Hypotheses mhpmpl.h H = I mHomP R
mhpmpl.p P = I mPoly R
mhpmpl.b B = Base P
mhpmpl.x φ X H N
Assertion mhpmpl φ X B

Proof

Step Hyp Ref Expression
1 mhpmpl.h H = I mHomP R
2 mhpmpl.p P = I mPoly R
3 mhpmpl.b B = Base P
4 mhpmpl.x φ X H N
5 eqid 0 R = 0 R
6 eqid h 0 I | h -1 Fin = h 0 I | h -1 Fin
7 1 4 mhprcl φ N 0
8 1 2 3 5 6 7 ismhp φ X H N X B X supp 0 R g h 0 I | h -1 Fin | fld 𝑠 0 g = N
9 8 simprbda φ X H N X B
10 4 9 mpdan φ X B