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.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.x	|- ( ph -> X e. ( H ` N ) )
5		eqid	|- ( 0g ` R ) = ( 0g ` R )
6		eqid	|- { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
7	1 4	mhprcl	|- ( ph -> N e. NN0 )
8	1 2 3 5 6 7	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 } ) ) )
9	8	simprbda	|- ( ( ph /\ X e. ( H ` N ) ) -> X e. B )
10	4 9	mpdan	|- ( ph -> X e. B )