This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 } )