Metamath Proof Explorer

Theorem mhpind

Description: The homogeneous polynomials of degree N are generated by the terms of degree N and addition. (Contributed by SN, 28-Jul-2024)

Ref Expression
Hypotheses mhpind.h 
|- H = ( I mHomP R )
mhpind.b 
|- B = ( Base ` R )
mhpind.z 
|- .0. = ( 0g ` R )
mhpind.p 
|- P = ( I mPoly R )
mhpind.a 
|- .+ = ( +g ` P )
mhpind.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
mhpind.s 
|- S = { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N }
mhpind.r 
|- ( ph -> R e. Grp )
mhpind.x 
|- ( ph -> X e. ( H ` N ) )
mhpind.0 
|- ( ph -> ( D X. { .0. } ) e. G )
mhpind.1 
|- ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( s e. D |-> if ( s = a , b , .0. ) ) e. G )
mhpind.2 
|- ( ( ph /\ ( x e. ( ( H ` N ) i^i G ) /\ y e. ( ( H ` N ) i^i G ) ) ) -> ( x .+ y ) e. G )
Assertion mhpind 
|- ( ph -> X e. G )

Proof

Step Hyp Ref Expression
1 mhpind.h 
 |-  H = ( I mHomP R )
2 mhpind.b 
 |-  B = ( Base ` R )
3 mhpind.z 
 |-  .0. = ( 0g ` R )
4 mhpind.p 
 |-  P = ( I mPoly R )
5 mhpind.a 
 |-  .+ = ( +g ` P )
6 mhpind.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
7 mhpind.s 
 |-  S = { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N }
8 mhpind.r 
 |-  ( ph -> R e. Grp )
9 mhpind.x 
 |-  ( ph -> X e. ( H ` N ) )
10 mhpind.0 
 |-  ( ph -> ( D X. { .0. } ) e. G )
11 mhpind.1 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( s e. D |-> if ( s = a , b , .0. ) ) e. G )
12 mhpind.2 
 |-  ( ( ph /\ ( x e. ( ( H ` N ) i^i G ) /\ y e. ( ( H ` N ) i^i G ) ) ) -> ( x .+ y ) e. G )
13 eqid 
 |-  ( +g ` R ) = ( +g ` R )
14 ovexd 
 |-  ( ph -> ( NN0 ^m I ) e. _V )
15 6 14 rabexd 
 |-  ( ph -> D e. _V )
16 ssrab2 
 |-  { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } C_ D
17 16 a1i 
 |-  ( ph -> { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } C_ D )
18 reldmmhp 
 |-  Rel dom mHomP
19 18 1 9 elfvov1 
 |-  ( ph -> I e. _V )
20 1 9 mhprcl 
 |-  ( ph -> N e. NN0 )
21 1 3 6 19 8 20 mhp0cl 
 |-  ( ph -> ( D X. { .0. } ) e. ( H ` N ) )
22 21 10 elind 
 |-  ( ph -> ( D X. { .0. } ) e. ( ( H ` N ) i^i G ) )
23 7 eleq2i 
 |-  ( a e. S <-> a e. { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } )
24 23 biimpri 
 |-  ( a e. { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } -> a e. S )
25 eqid 
 |-  ( Base ` P ) = ( Base ` P )
26 20 adantr 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> N e. NN0 )
27 simplrr 
 |-  ( ( ( ph /\ ( a e. S /\ b e. B ) ) /\ s e. D ) -> b e. B )
28 2 3 grpidcl 
 |-  ( R e. Grp -> .0. e. B )
29 8 28 syl 
 |-  ( ph -> .0. e. B )
30 29 ad2antrr 
 |-  ( ( ( ph /\ ( a e. S /\ b e. B ) ) /\ s e. D ) -> .0. e. B )
31 27 30 ifcld 
 |-  ( ( ( ph /\ ( a e. S /\ b e. B ) ) /\ s e. D ) -> if ( s = a , b , .0. ) e. B )
32 31 fmpttd 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( s e. D |-> if ( s = a , b , .0. ) ) : D --> B )
33 2 fvexi 
 |-  B e. _V
34 33 a1i 
 |-  ( ph -> B e. _V )
35 34 15 elmapd 
 |-  ( ph -> ( ( s e. D |-> if ( s = a , b , .0. ) ) e. ( B ^m D ) <-> ( s e. D |-> if ( s = a , b , .0. ) ) : D --> B ) )
36 35 adantr 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( ( s e. D |-> if ( s = a , b , .0. ) ) e. ( B ^m D ) <-> ( s e. D |-> if ( s = a , b , .0. ) ) : D --> B ) )
37 32 36 mpbird 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( s e. D |-> if ( s = a , b , .0. ) ) e. ( B ^m D ) )
38 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
39 eqid 
 |-  ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
40 38 2 6 39 19 psrbas 
 |-  ( ph -> ( Base ` ( I mPwSer R ) ) = ( B ^m D ) )
41 40 adantr 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( Base ` ( I mPwSer R ) ) = ( B ^m D ) )
42 37 41 eleqtrrd 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( s e. D |-> if ( s = a , b , .0. ) ) e. ( Base ` ( I mPwSer R ) ) )
43 3 fvexi 
 |-  .0. e. _V
44 43 a1i 
 |-  ( ph -> .0. e. _V )
45 eqid 
 |-  ( s e. D |-> if ( s = a , b , .0. ) ) = ( s e. D |-> if ( s = a , b , .0. ) )
46 15 44 45 sniffsupp 
 |-  ( ph -> ( s e. D |-> if ( s = a , b , .0. ) ) finSupp .0. )
47 46 adantr 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( s e. D |-> if ( s = a , b , .0. ) ) finSupp .0. )
48 4 38 39 3 25 mplelbas 
 |-  ( ( s e. D |-> if ( s = a , b , .0. ) ) e. ( Base ` P ) <-> ( ( s e. D |-> if ( s = a , b , .0. ) ) e. ( Base ` ( I mPwSer R ) ) /\ ( s e. D |-> if ( s = a , b , .0. ) ) finSupp .0. ) )
49 42 47 48 sylanbrc 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( s e. D |-> if ( s = a , b , .0. ) ) e. ( Base ` P ) )
50 elneeldif 
 |-  ( ( a e. S /\ s e. ( D \ S ) ) -> a =/= s )
51 50 necomd 
 |-  ( ( a e. S /\ s e. ( D \ S ) ) -> s =/= a )
52 51 adantll 
 |-  ( ( ( ph /\ a e. S ) /\ s e. ( D \ S ) ) -> s =/= a )
53 52 adantlrr 
 |-  ( ( ( ph /\ ( a e. S /\ b e. B ) ) /\ s e. ( D \ S ) ) -> s =/= a )
54 53 neneqd 
 |-  ( ( ( ph /\ ( a e. S /\ b e. B ) ) /\ s e. ( D \ S ) ) -> -. s = a )
55 54 iffalsed 
 |-  ( ( ( ph /\ ( a e. S /\ b e. B ) ) /\ s e. ( D \ S ) ) -> if ( s = a , b , .0. ) = .0. )
56 15 adantr 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> D e. _V )
57 55 56 suppss2 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( ( s e. D |-> if ( s = a , b , .0. ) ) supp .0. ) C_ S )
58 57 7 sseqtrdi 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( ( s e. D |-> if ( s = a , b , .0. ) ) supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } )
59 1 4 25 3 6 26 49 58 ismhp2 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( s e. D |-> if ( s = a , b , .0. ) ) e. ( H ` N ) )
60 59 11 elind 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( s e. D |-> if ( s = a , b , .0. ) ) e. ( ( H ` N ) i^i G ) )
61 24 60 sylanr1 
 |-  ( ( ph /\ ( a e. { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. B ) ) -> ( s e. D |-> if ( s = a , b , .0. ) ) e. ( ( H ` N ) i^i G ) )
62 elinel1 
 |-  ( x e. ( ( H ` N ) i^i G ) -> x e. ( H ` N ) )
63 62 ad2antrl 
 |-  ( ( ph /\ ( x e. ( ( H ` N ) i^i G ) /\ y e. ( ( H ` N ) i^i G ) ) ) -> x e. ( H ` N ) )
64 1 4 25 63 mhpmpl 
 |-  ( ( ph /\ ( x e. ( ( H ` N ) i^i G ) /\ y e. ( ( H ` N ) i^i G ) ) ) -> x e. ( Base ` P ) )
65 elinel1 
 |-  ( y e. ( ( H ` N ) i^i G ) -> y e. ( H ` N ) )
66 65 ad2antll 
 |-  ( ( ph /\ ( x e. ( ( H ` N ) i^i G ) /\ y e. ( ( H ` N ) i^i G ) ) ) -> y e. ( H ` N ) )
67 1 4 25 66 mhpmpl 
 |-  ( ( ph /\ ( x e. ( ( H ` N ) i^i G ) /\ y e. ( ( H ` N ) i^i G ) ) ) -> y e. ( Base ` P ) )
68 4 25 13 5 64 67 mpladd 
 |-  ( ( ph /\ ( x e. ( ( H ` N ) i^i G ) /\ y e. ( ( H ` N ) i^i G ) ) ) -> ( x .+ y ) = ( x oF ( +g ` R ) y ) )
69 8 adantr 
 |-  ( ( ph /\ ( x e. ( ( H ` N ) i^i G ) /\ y e. ( ( H ` N ) i^i G ) ) ) -> R e. Grp )
70 1 4 5 69 63 66 mhpaddcl 
 |-  ( ( ph /\ ( x e. ( ( H ` N ) i^i G ) /\ y e. ( ( H ` N ) i^i G ) ) ) -> ( x .+ y ) e. ( H ` N ) )
71 70 12 elind 
 |-  ( ( ph /\ ( x e. ( ( H ` N ) i^i G ) /\ y e. ( ( H ` N ) i^i G ) ) ) -> ( x .+ y ) e. ( ( H ` N ) i^i G ) )
72 68 71 eqeltrrd 
 |-  ( ( ph /\ ( x e. ( ( H ` N ) i^i G ) /\ y e. ( ( H ` N ) i^i G ) ) ) -> ( x oF ( +g ` R ) y ) e. ( ( H ` N ) i^i G ) )
73 1 4 25 9 mhpmpl 
 |-  ( ph -> X e. ( Base ` P ) )
74 4 2 25 6 73 mplelf 
 |-  ( ph -> X : D --> B )
75 4 25 3 73 mplelsfi 
 |-  ( ph -> X finSupp .0. )
76 1 3 6 9 mhpdeg 
 |-  ( ph -> ( X supp .0. ) C_ { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } )
77 2 3 13 8 15 17 22 61 72 74 75 76 fsuppssind 
 |-  ( ph -> X e. ( ( H ` N ) i^i G ) )
78 77 elin2d 
 |-  ( ph -> X e. G )