Metamath Proof Explorer

Theorem mhpaddcl

Description: Homogeneous polynomials are closed under addition. (Contributed by SN, 26-Aug-2023) Remove sethood hypothesis. (Revised by SN, 18-May-2025)

Ref Expression
Hypotheses mhpaddcl.h 
|- H = ( I mHomP R )
mhpaddcl.p 
|- P = ( I mPoly R )
mhpaddcl.a 
|- .+ = ( +g ` P )
mhpaddcl.r 
|- ( ph -> R e. Grp )
mhpaddcl.n 
|- ( ph -> N e. NN0 )
mhpaddcl.x 
|- ( ph -> X e. ( H ` N ) )
mhpaddcl.y 
|- ( ph -> Y e. ( H ` N ) )
Assertion mhpaddcl 
|- ( ph -> ( X .+ Y ) e. ( H ` N ) )

Proof

Step Hyp Ref Expression
1 mhpaddcl.h 
 |-  H = ( I mHomP R )
2 mhpaddcl.p 
 |-  P = ( I mPoly R )
3 mhpaddcl.a 
 |-  .+ = ( +g ` P )
4 mhpaddcl.r 
 |-  ( ph -> R e. Grp )
5 mhpaddcl.n 
 |-  ( ph -> N e. NN0 )
6 mhpaddcl.x 
 |-  ( ph -> X e. ( H ` N ) )
7 mhpaddcl.y 
 |-  ( ph -> Y 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 reldmmhp 
 |-  Rel dom mHomP
12 11 1 6 elfvov1 
 |-  ( ph -> I e. _V )
13 2 mplgrp 
 |-  ( ( I e. _V /\ R e. Grp ) -> P e. Grp )
14 12 4 13 syl2anc 
 |-  ( ph -> P e. Grp )
15 1 2 8 12 4 5 6 mhpmpl 
 |-  ( ph -> X e. ( Base ` P ) )
16 1 2 8 12 4 5 7 mhpmpl 
 |-  ( ph -> Y e. ( Base ` P ) )
17 8 3 grpcl 
 |-  ( ( P e. Grp /\ X e. ( Base ` P ) /\ Y e. ( Base ` P ) ) -> ( X .+ Y ) e. ( Base ` P ) )
18 14 15 16 17 syl3anc 
 |-  ( ph -> ( X .+ Y ) e. ( Base ` P ) )
19 eqid 
 |-  ( +g ` R ) = ( +g ` R )
20 2 8 19 3 15 16 mpladd 
 |-  ( ph -> ( X .+ Y ) = ( X oF ( +g ` R ) Y ) )
21 20 oveq1d 
 |-  ( ph -> ( ( X .+ Y ) supp ( 0g ` R ) ) = ( ( X oF ( +g ` R ) Y ) supp ( 0g ` R ) ) )
22 ovexd 
 |-  ( ph -> ( NN0 ^m I ) e. _V )
23 10 22 rabexd 
 |-  ( ph -> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V )
24 eqid 
 |-  ( Base ` R ) = ( Base ` R )
25 24 9 grpidcl 
 |-  ( R e. Grp -> ( 0g ` R ) e. ( Base ` R ) )
26 4 25 syl 
 |-  ( ph -> ( 0g ` R ) e. ( Base ` R ) )
27 2 24 8 10 15 mplelf 
 |-  ( ph -> X : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
28 2 24 8 10 16 mplelf 
 |-  ( ph -> Y : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
29 24 19 9 grplid 
 |-  ( ( R e. Grp /\ ( 0g ` R ) e. ( Base ` R ) ) -> ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
30 4 26 29 syl2anc 
 |-  ( ph -> ( ( 0g ` R ) ( +g ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
31 23 26 27 28 30 suppofssd 
 |-  ( ph -> ( ( X oF ( +g ` R ) Y ) supp ( 0g ` R ) ) C_ ( ( X supp ( 0g ` R ) ) u. ( Y supp ( 0g ` R ) ) ) )
32 21 31 eqsstrd 
 |-  ( ph -> ( ( X .+ Y ) supp ( 0g ` R ) ) C_ ( ( X supp ( 0g ` R ) ) u. ( Y supp ( 0g ` R ) ) ) )
33 1 9 10 12 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 } )
34 1 9 10 12 4 5 7 mhpdeg 
 |-  ( ph -> ( Y supp ( 0g ` R ) ) C_ { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } )
35 33 34 unssd 
 |-  ( ph -> ( ( X supp ( 0g ` R ) ) u. ( Y supp ( 0g ` R ) ) ) C_ { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } )
36 32 35 sstrd 
 |-  ( ph -> ( ( X .+ Y ) supp ( 0g ` R ) ) C_ { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } )
37 1 2 8 9 10 12 4 5 18 36 ismhp2 
 |-  ( ph -> ( X .+ Y ) e. ( H ` N ) )