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.i	|- ( ph -> I e. V )
	mhpdeg.r	|- ( ph -> R e. W )
	mhpdeg.n	|- ( ph -> N e. NN0 )
	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.i	|- ( ph -> I e. V )
5		mhpdeg.r	|- ( ph -> R e. W )
6		mhpdeg.n	|- ( ph -> N e. NN0 )
7		mhpdeg.x	|- ( ph -> X e. ( H ` N ) )
8		eqid	|- ( I mPoly R ) = ( I mPoly R )
9		eqid	|- ( Base ` ( I mPoly R ) ) = ( Base ` ( I mPoly R ) )
10	1 8 9 2 3 4 5 6	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 } ) ) )
11	10	simplbda	|- ( ( ph /\ X e. ( H ` N ) ) -> ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } )
12	7 11	mpdan	|- ( ph -> ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } )