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

Metamath Proof Explorer

Theorem mhpinvcl

Description: Homogeneous polynomials are closed under taking the opposite. (Contributed by SN, 12-Sep-2023) Remove closure hypotheses. (Revised by SN, 4-Sep-2025)

Ref Expression
Hypotheses mhpinvcl.h 
|- H = ( I mHomP R )
mhpinvcl.p 
|- P = ( I mPoly R )
mhpinvcl.m 
|- M = ( invg ` P )
mhpinvcl.r 
|- ( ph -> R e. Grp )
mhpinvcl.x 
|- ( ph -> X e. ( H ` N ) )
Assertion mhpinvcl 
|- ( ph -> ( M ` X ) e. ( H ` N ) )

Proof

Step Hyp Ref Expression
1 mhpinvcl.h 
 |-  H = ( I mHomP R )
2 mhpinvcl.p 
 |-  P = ( I mPoly R )
3 mhpinvcl.m 
 |-  M = ( invg ` P )
4 mhpinvcl.r 
 |-  ( ph -> R e. Grp )
5 mhpinvcl.x 
 |-  ( ph -> X e. ( H ` N ) )
6 eqid 
 |-  ( Base ` P ) = ( Base ` P )
7 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
8 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
9 1 5 mhprcl 
 |-  ( ph -> N e. NN0 )
10 reldmmhp 
 |-  Rel dom mHomP
11 10 1 5 elfvov1 
 |-  ( ph -> I e. _V )
12 2 mplgrp 
 |-  ( ( I e. _V /\ R e. Grp ) -> P e. Grp )
13 11 4 12 syl2anc 
 |-  ( ph -> P e. Grp )
14 1 2 6 5 mhpmpl 
 |-  ( ph -> X e. ( Base ` P ) )
15 6 3 13 14 grpinvcld 
 |-  ( ph -> ( M ` X ) e. ( Base ` P ) )
16 eqid 
 |-  ( invg ` R ) = ( invg ` R )
17 2 6 16 3 11 4 14 mplneg 
 |-  ( ph -> ( M ` X ) = ( ( invg ` R ) o. X ) )
18 17 oveq1d 
 |-  ( ph -> ( ( M ` X ) supp ( 0g ` R ) ) = ( ( ( invg ` R ) o. X ) supp ( 0g ` R ) ) )
19 eqid 
 |-  ( Base ` R ) = ( Base ` R )
20 19 16 grpinvfn 
 |-  ( invg ` R ) Fn ( Base ` R )
21 20 a1i 
 |-  ( ph -> ( invg ` R ) Fn ( Base ` R ) )
22 2 19 6 8 14 mplelf 
 |-  ( ph -> X : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
23 ovex 
 |-  ( NN0 ^m I ) e. _V
24 23 rabex 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V
25 24 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V )
26 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
27 7 16 grpinvid 
 |-  ( R e. Grp -> ( ( invg ` R ) ` ( 0g ` R ) ) = ( 0g ` R ) )
28 4 27 syl 
 |-  ( ph -> ( ( invg ` R ) ` ( 0g ` R ) ) = ( 0g ` R ) )
29 21 22 25 26 28 suppcoss 
 |-  ( ph -> ( ( ( invg ` R ) o. X ) supp ( 0g ` R ) ) C_ ( X supp ( 0g ` R ) ) )
30 18 29 eqsstrd 
 |-  ( ph -> ( ( M ` X ) supp ( 0g ` R ) ) C_ ( X supp ( 0g ` R ) ) )
31 1 7 8 5 mhpdeg 
 |-  ( ph -> ( X supp ( 0g ` R ) ) C_ { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } )
32 30 31 sstrd 
 |-  ( ph -> ( ( M ` X ) supp ( 0g ` R ) ) C_ { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } )
33 1 2 6 7 8 9 15 32 ismhp2 
 |-  ( ph -> ( M ` X ) e. ( H ` N ) )