Metamath Proof Explorer


Theorem mhpdeg

Description: All nonzero terms of a homogeneous polynomial have degree N . (Contributed by Steven Nguyen, 25-Aug-2023)

Ref Expression
Hypotheses mhpdeg.h
|- H = ( I mHomP R )
mhpdeg.0
|- .0. = ( 0g ` R )
mhpdeg.d
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
mhpdeg.x
|- ( ph -> X e. ( H ` N ) )
Assertion mhpdeg
|- ( ph -> ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } )

Proof

Step Hyp Ref Expression
1 mhpdeg.h
 |-  H = ( I mHomP R )
2 mhpdeg.0
 |-  .0. = ( 0g ` R )
3 mhpdeg.d
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
4 mhpdeg.x
 |-  ( ph -> X e. ( H ` N ) )
5 eqid
 |-  ( I mPoly R ) = ( I mPoly R )
6 eqid
 |-  ( Base ` ( I mPoly R ) ) = ( Base ` ( I mPoly R ) )
7 1 4 mhprcl
 |-  ( ph -> N e. NN0 )
8 1 5 6 2 3 7 ismhp
 |-  ( ph -> ( X e. ( H ` N ) <-> ( X e. ( Base ` ( I mPoly R ) ) /\ ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } ) ) )
9 8 simplbda
 |-  ( ( ph /\ X e. ( H ` N ) ) -> ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } )
10 4 9 mpdan
 |-  ( ph -> ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } )