Metamath Proof Explorer

Theorem mhpinvcl

Description: Homogeneous polynomials are closed under taking the opposite. (Contributed by SN, 12-Sep-2023) Remove sethood hypothesis. (Revised by SN, 18-May-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.n 
|- ( ph -> N e. NN0 )
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.n 
 |-  ( ph -> N e. NN0 )
6 mhpinvcl.x 
 |-  ( ph -> X e. ( H ` N ) )
7 eqid 
 |-  ( Base ` P ) = ( Base ` P )
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 reldmmhp 
 |-  Rel dom mHomP
11 10 1 6 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 7 11 4 5 6 mhpmpl 
 |-  ( ph -> X e. ( Base ` P ) )
15 7 3 grpinvcl 
 |-  ( ( P e. Grp /\ X e. ( Base ` P ) ) -> ( M ` X ) e. ( Base ` P ) )
16 13 14 15 syl2anc 
 |-  ( ph -> ( M ` X ) e. ( Base ` P ) )
17 eqid 
 |-  ( invg ` R ) = ( invg ` R )
18 2 7 17 3 11 4 14 mplneg 
 |-  ( ph -> ( M ` X ) = ( ( invg ` R ) o. X ) )
19 18 oveq1d 
 |-  ( ph -> ( ( M ` X ) supp ( 0g ` R ) ) = ( ( ( invg ` R ) o. X ) supp ( 0g ` R ) ) )
20 eqid 
 |-  ( Base ` R ) = ( Base ` R )
21 20 17 grpinvfn 
 |-  ( invg ` R ) Fn ( Base ` R )
22 21 a1i 
 |-  ( ph -> ( invg ` R ) Fn ( Base ` R ) )
23 2 20 7 9 14 mplelf 
 |-  ( ph -> X : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
24 ovex 
 |-  ( NN0 ^m I ) e. _V
25 24 rabex 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V
26 25 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V )
27 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
28 8 17 grpinvid 
 |-  ( R e. Grp -> ( ( invg ` R ) ` ( 0g ` R ) ) = ( 0g ` R ) )
29 4 28 syl 
 |-  ( ph -> ( ( invg ` R ) ` ( 0g ` R ) ) = ( 0g ` R ) )
30 22 23 26 27 29 suppcoss 
 |-  ( ph -> ( ( ( invg ` R ) o. X ) supp ( 0g ` R ) ) C_ ( X supp ( 0g ` R ) ) )
31 19 30 eqsstrd 
 |-  ( ph -> ( ( M ` X ) supp ( 0g ` R ) ) C_ ( X supp ( 0g ` R ) ) )
32 1 8 9 11 4 5 6 mhpdeg 
 |-  ( ph -> ( X supp ( 0g ` R ) ) C_ { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } )
33 31 32 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 } )
34 1 2 7 8 9 11 4 5 16 33 ismhp2 
 |-  ( ph -> ( M ` X ) e. ( H ` N ) )