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 | |- ( ph -> X e. ( H ` N ) ) |
||
| Assertion | mhpmpl | |- ( ph -> X e. B ) |
| 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 | |- ( ph -> X e. ( H ` N ) ) |
|
| 5 | eqid | |- ( 0g ` R ) = ( 0g ` R ) |
|
| 6 | eqid | |- { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |
|
| 7 | 1 4 | mhprcl | |- ( ph -> N e. NN0 ) |
| 8 | 1 2 3 5 6 7 | ismhp | |- ( ph -> ( X e. ( H ` N ) <-> ( X e. B /\ ( X supp ( 0g ` R ) ) C_ { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) ) ) |
| 9 | 8 | simprbda | |- ( ( ph /\ X e. ( H ` N ) ) -> X e. B ) |
| 10 | 4 9 | mpdan | |- ( ph -> X e. B ) |