Theorem mhpmpl

Description: A homogeneous polynomial is a polynomial. (Contributed by Steven Nguyen, 25-Aug-2023)

	Ref	Expression
Hypotheses	mhpmpl.h	|- H = ( I mHomP R )
	mhpmpl.p	|- P = ( I mPoly R )
	mhpmpl.b	|- B = ( Base ` P )
	mhpmpl.i	|- ( ph -> I e. V )
	mhpmpl.r	|- ( ph -> R e. W )
	mhpmpl.n	|- ( ph -> N e. NN0 )
	mhpmpl.x	|- ( ph -> X e. ( H ` N ) )
Assertion	mhpmpl	|- ( ph -> X e. B )

Proof

Step	Hyp	Ref	Expression
1		mhpmpl.h	|- H = ( I mHomP R )
2		mhpmpl.p	|- P = ( I mPoly R )
3		mhpmpl.b	|- B = ( Base ` P )
4		mhpmpl.i	|- ( ph -> I e. V )
5		mhpmpl.r	|- ( ph -> R e. W )
6		mhpmpl.n	|- ( ph -> N e. NN0 )
7		mhpmpl.x	|- ( ph -> X e. ( H ` N ) )
8		eqid	|- ( 0g ` R ) = ( 0g ` R )
9		eqid	|- { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
10	1 2 3 8 9 4 5 6	ismhp	|- ( ph -> ( X e. ( H ` N ) <-> ( X e. B /\ ( X supp ( 0g ` R ) ) C_ { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) ) )
11	10	simprbda	|- ( ( ph /\ X e. ( H ` N ) ) -> X e. B )
12	7 11	mpdan	|- ( ph -> X e. B )