Theorem ismhp

Description: Property of being a homogeneous polynomial. (Contributed by Steven Nguyen, 25-Aug-2023)

	Ref	Expression
Hypotheses	mhpfval.h	|- H = ( I mHomP R )
	mhpfval.p	|- P = ( I mPoly R )
	mhpfval.b	|- B = ( Base ` P )
	mhpfval.0	|- .0. = ( 0g ` R )
	mhpfval.d	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
	mhpfval.i	|- ( ph -> I e. V )
	mhpfval.r	|- ( ph -> R e. W )
	mhpval.n	|- ( ph -> N e. NN0 )
Assertion	ismhp	|- ( ph -> ( X e. ( H ` N ) <-> ( X e. B /\ ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } ) ) )

Proof

Step	Hyp	Ref	Expression
1		mhpfval.h	|- H = ( I mHomP R )
2		mhpfval.p	|- P = ( I mPoly R )
3		mhpfval.b	|- B = ( Base ` P )
4		mhpfval.0	|- .0. = ( 0g ` R )
5		mhpfval.d	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
6		mhpfval.i	|- ( ph -> I e. V )
7		mhpfval.r	|- ( ph -> R e. W )
8		mhpval.n	|- ( ph -> N e. NN0 )
9	1 2 3 4 5 6 7 8	mhpval	|- ( ph -> ( H ` N ) = { f e. B | ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } } )
10	9	eleq2d	|- ( ph -> ( X e. ( H ` N ) <-> X e. { f e. B | ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } } ) )
11		oveq1	|- ( f = X -> ( f supp .0. ) = ( X supp .0. ) )
12	11	sseq1d	|- ( f = X -> ( ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } <-> ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } ) )
13	12	elrab	|- ( X e. { f e. B | ( f supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } } <-> ( X e. B /\ ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } ) )
14	10 13	bitrdi	|- ( ph -> ( X e. ( H ` N ) <-> ( X e. B /\ ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } ) ) )