Metamath Proof Explorer

Theorem mhpinvcl

Description: Homogeneous polynomials are closed under taking the opposite. (Contributed by SN, 12-Sep-2023)

Ref Expression
Hypotheses mhpinvcl.h 
|- H = ( I mHomP R )
mhpinvcl.p 
|- P = ( I mPoly R )
mhpinvcl.m 
|- M = ( invg ` P )
mhpinvcl.i 
|- ( ph -> I e. V )
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.i 
 |-  ( ph -> I e. V )
5 mhpinvcl.r 
 |-  ( ph -> R e. Grp )
6 mhpinvcl.n 
 |-  ( ph -> N e. NN0 )
7 mhpinvcl.x 
 |-  ( ph -> X e. ( H ` N ) )
8 eqid 
 |-  ( Base ` P ) = ( Base ` P )
9 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
10 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
11 2 mplgrp 
 |-  ( ( I e. V /\ R e. Grp ) -> P e. Grp )
12 4 5 11 syl2anc 
 |-  ( ph -> P e. Grp )
13 1 2 8 4 5 6 7 mhpmpl 
 |-  ( ph -> X e. ( Base ` P ) )
14 8 3 grpinvcl 
 |-  ( ( P e. Grp /\ X e. ( Base ` P ) ) -> ( M ` X ) e. ( Base ` P ) )
15 12 13 14 syl2anc 
 |-  ( ph -> ( M ` X ) e. ( Base ` P ) )
16 eqid 
 |-  ( invg ` R ) = ( invg ` R )
17 2 8 16 3 4 5 13 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 8 10 13 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 9 16 grpinvid 
 |-  ( R e. Grp -> ( ( invg ` R ) ` ( 0g ` R ) ) = ( 0g ` R ) )
28 5 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 9 10 4 5 6 7 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 8 9 10 4 5 6 15 32 ismhp2 
 |-  ( ph -> ( M ` X ) e. ( H ` N ) )