Theorem ismhp2

Description: Deduce a homogeneous polynomial from its properties. (Contributed by SN, 25-May-2024)

	Ref	Expression
Hypotheses	ismhp.h	|- H = ( I mHomP R )
	ismhp.p	|- P = ( I mPoly R )
	ismhp.b	|- B = ( Base ` P )
	ismhp.0	|- .0. = ( 0g ` R )
	ismhp.d	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
	ismhp.n	|- ( ph -> N e. NN0 )
	ismhp2.1	|- ( ph -> X e. B )
	ismhp2.2	|- ( ph -> ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } )
Assertion	ismhp2	|- ( ph -> X e. ( H ` N ) )

Proof

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