This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )