Theorem mhprcl

Description: Reverse closure for homogeneous polynomials, use elfvov1 and elfvov2 with reldmmhp for the reverse closure of I and R . (Contributed by SN, 4-Aug-2025)

	Ref	Expression
Hypotheses	mhprcl.h	|- H = ( I mHomP R )
	mhprcl.x	|- ( ph -> X e. ( H ` N ) )
Assertion	mhprcl	|- ( ph -> N e. NN0 )

Proof

Step	Hyp	Ref	Expression
1		mhprcl.h	|- H = ( I mHomP R )
2		mhprcl.x	|- ( ph -> X e. ( H ` N ) )
3		eqid	|- ( I mPoly R ) = ( I mPoly R )
4		eqid	|- ( Base ` ( I mPoly R ) ) = ( Base ` ( I mPoly R ) )
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		reldmmhp	|- Rel dom mHomP
8	7 1 2	elfvov1	|- ( ph -> I e. _V )
9	7 1 2	elfvov2	|- ( ph -> R e. _V )
10	1 3 4 5 6 8 9	mhpfval	|- ( ph -> H = ( n e. NN0 |-> { f e. ( Base ` ( I mPoly R ) ) | ( f supp ( 0g ` R ) ) C_ { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = n } } ) )
11	10	fveq1d	|- ( ph -> ( H ` N ) = ( ( n e. NN0 |-> { f e. ( Base ` ( I mPoly R ) ) | ( f supp ( 0g ` R ) ) C_ { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = n } } ) ` N ) )
12	2 11	eleqtrd	|- ( ph -> X e. ( ( n e. NN0 |-> { f e. ( Base ` ( I mPoly R ) ) | ( f supp ( 0g ` R ) ) C_ { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = n } } ) ` N ) )
13		eqid	|- ( n e. NN0 |-> { f e. ( Base ` ( I mPoly R ) ) | ( f supp ( 0g ` R ) ) C_ { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = n } } ) = ( n e. NN0 |-> { f e. ( Base ` ( I mPoly R ) ) | ( f supp ( 0g ` R ) ) C_ { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = n } } )
14	13	mptrcl	|- ( X e. ( ( n e. NN0 |-> { f e. ( Base ` ( I mPoly R ) ) | ( f supp ( 0g ` R ) ) C_ { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = n } } ) ` N ) -> N e. NN0 )
15	12 14	syl	|- ( ph -> N e. NN0 )