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 ) )