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