Metamath Proof Explorer

Theorem cpmadugsumlemB

Description: Lemma B for cpmadugsum . (Contributed by AV, 2-Nov-2019)

Ref Expression
Hypotheses cpmadugsum.a 
|- A = ( N Mat R )
cpmadugsum.b 
|- B = ( Base ` A )
cpmadugsum.p 
|- P = ( Poly1 ` R )
cpmadugsum.y 
|- Y = ( N Mat P )
cpmadugsum.t 
|- T = ( N matToPolyMat R )
cpmadugsum.x 
|- X = ( var1 ` R )
cpmadugsum.e 
|- .^ = ( .g ` ( mulGrp ` P ) )
cpmadugsum.m 
|- .x. = ( .s ` Y )
cpmadugsum.r 
|- .X. = ( .r ` Y )
cpmadugsum.1 
|- .1. = ( 1r ` Y )
Assertion cpmadugsumlemB 
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( X .x. .1. ) .X. ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) = ( Y gsum ( i e. ( 0 ... s ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cpmadugsum.a 
 |-  A = ( N Mat R )
2 cpmadugsum.b 
 |-  B = ( Base ` A )
3 cpmadugsum.p 
 |-  P = ( Poly1 ` R )
4 cpmadugsum.y 
 |-  Y = ( N Mat P )
5 cpmadugsum.t 
 |-  T = ( N matToPolyMat R )
6 cpmadugsum.x 
 |-  X = ( var1 ` R )
7 cpmadugsum.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
8 cpmadugsum.m 
 |-  .x. = ( .s ` Y )
9 cpmadugsum.r 
 |-  .X. = ( .r ` Y )
10 cpmadugsum.1 
 |-  .1. = ( 1r ` Y )
11 crngring 
 |-  ( R e. CRing -> R e. Ring )
12 3 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
13 11 12 syl 
 |-  ( R e. CRing -> P e. Ring )
14 13 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P e. Ring )
15 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
16 15 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
17 14 16 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( mulGrp ` P ) e. Mnd )
18 17 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( mulGrp ` P ) e. Mnd )
19 elfznn0 
 |-  ( i e. ( 0 ... s ) -> i e. NN0 )
20 19 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> i e. NN0 )
21 1nn0 
 |-  1 e. NN0
22 21 a1i 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> 1 e. NN0 )
23 11 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R e. Ring )
24 eqid 
 |-  ( Base ` P ) = ( Base ` P )
25 6 3 24 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` P ) )
26 23 25 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> X e. ( Base ` P ) )
27 26 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> X e. ( Base ` P ) )
28 15 24 mgpbas 
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
29 eqid 
 |-  ( .r ` P ) = ( .r ` P )
30 15 29 mgpplusg 
 |-  ( .r ` P ) = ( +g ` ( mulGrp ` P ) )
31 28 7 30 mulgnn0dir 
 |-  ( ( ( mulGrp ` P ) e. Mnd /\ ( i e. NN0 /\ 1 e. NN0 /\ X e. ( Base ` P ) ) ) -> ( ( i + 1 ) .^ X ) = ( ( i .^ X ) ( .r ` P ) ( 1 .^ X ) ) )
32 18 20 22 27 31 syl13anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( ( i + 1 ) .^ X ) = ( ( i .^ X ) ( .r ` P ) ( 1 .^ X ) ) )
33 3 ply1crng 
 |-  ( R e. CRing -> P e. CRing )
34 33 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ P e. CRing ) )
35 34 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ P e. CRing ) )
36 4 matsca2 
 |-  ( ( N e. Fin /\ P e. CRing ) -> P = ( Scalar ` Y ) )
37 35 36 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P = ( Scalar ` Y ) )
38 37 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> P = ( Scalar ` Y ) )
39 38 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( .r ` P ) = ( .r ` ( Scalar ` Y ) ) )
40 eqidd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( i .^ X ) = ( i .^ X ) )
41 28 7 mulg1 
 |-  ( X e. ( Base ` P ) -> ( 1 .^ X ) = X )
42 26 41 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( 1 .^ X ) = X )
43 42 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( 1 .^ X ) = X )
44 39 40 43 oveq123d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( ( i .^ X ) ( .r ` P ) ( 1 .^ X ) ) = ( ( i .^ X ) ( .r ` ( Scalar ` Y ) ) X ) )
45 32 44 eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( ( i + 1 ) .^ X ) = ( ( i .^ X ) ( .r ` ( Scalar ` Y ) ) X ) )
46 13 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ P e. Ring ) )
47 46 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ P e. Ring ) )
48 4 matring 
 |-  ( ( N e. Fin /\ P e. Ring ) -> Y e. Ring )
49 47 48 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Ring )
50 49 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> Y e. Ring )
51 simpll1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> N e. Fin )
52 23 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> R e. Ring )
53 simplrl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> s e. NN0 )
54 simprr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> b e. ( B ^m ( 0 ... s ) ) )
55 54 anim1i 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( b e. ( B ^m ( 0 ... s ) ) /\ i e. ( 0 ... s ) ) )
56 1 2 3 4 5 m2pmfzmap 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ s e. NN0 ) /\ ( b e. ( B ^m ( 0 ... s ) ) /\ i e. ( 0 ... s ) ) ) -> ( T ` ( b ` i ) ) e. ( Base ` Y ) )
57 51 52 53 55 56 syl31anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( T ` ( b ` i ) ) e. ( Base ` Y ) )
58 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
59 58 9 10 ringlidm 
 |-  ( ( Y e. Ring /\ ( T ` ( b ` i ) ) e. ( Base ` Y ) ) -> ( .1. .X. ( T ` ( b ` i ) ) ) = ( T ` ( b ` i ) ) )
60 50 57 59 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( .1. .X. ( T ` ( b ` i ) ) ) = ( T ` ( b ` i ) ) )
61 60 eqcomd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( T ` ( b ` i ) ) = ( .1. .X. ( T ` ( b ` i ) ) ) )
62 45 61 oveq12d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) = ( ( ( i .^ X ) ( .r ` ( Scalar ` Y ) ) X ) .x. ( .1. .X. ( T ` ( b ` i ) ) ) ) )
63 4 matassa 
 |-  ( ( N e. Fin /\ P e. CRing ) -> Y e. AssAlg )
64 34 63 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. AssAlg )
65 64 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. AssAlg )
66 65 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> Y e. AssAlg )
67 37 eqcomd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Scalar ` Y ) = P )
68 67 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Base ` ( Scalar ` Y ) ) = ( Base ` P ) )
69 26 68 eleqtrrd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> X e. ( Base ` ( Scalar ` Y ) ) )
70 69 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> X e. ( Base ` ( Scalar ` Y ) ) )
71 28 7 mulgnn0cl 
 |-  ( ( ( mulGrp ` P ) e. Mnd /\ i e. NN0 /\ X e. ( Base ` P ) ) -> ( i .^ X ) e. ( Base ` P ) )
72 18 20 27 71 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( i .^ X ) e. ( Base ` P ) )
73 68 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( Base ` ( Scalar ` Y ) ) = ( Base ` P ) )
74 72 73 eleqtrrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( i .^ X ) e. ( Base ` ( Scalar ` Y ) ) )
75 46 48 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. Ring )
76 75 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Ring )
77 58 10 ringidcl 
 |-  ( Y e. Ring -> .1. e. ( Base ` Y ) )
78 76 77 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> .1. e. ( Base ` Y ) )
79 78 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> .1. e. ( Base ` Y ) )
80 eqid 
 |-  ( Scalar ` Y ) = ( Scalar ` Y )
81 eqid 
 |-  ( Base ` ( Scalar ` Y ) ) = ( Base ` ( Scalar ` Y ) )
82 eqid 
 |-  ( .r ` ( Scalar ` Y ) ) = ( .r ` ( Scalar ` Y ) )
83 58 80 81 82 8 9 assa2ass 
 |-  ( ( Y e. AssAlg /\ ( X e. ( Base ` ( Scalar ` Y ) ) /\ ( i .^ X ) e. ( Base ` ( Scalar ` Y ) ) ) /\ ( .1. e. ( Base ` Y ) /\ ( T ` ( b ` i ) ) e. ( Base ` Y ) ) ) -> ( ( X .x. .1. ) .X. ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) = ( ( ( i .^ X ) ( .r ` ( Scalar ` Y ) ) X ) .x. ( .1. .X. ( T ` ( b ` i ) ) ) ) )
84 66 70 74 79 57 83 syl122anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( ( X .x. .1. ) .X. ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) = ( ( ( i .^ X ) ( .r ` ( Scalar ` Y ) ) X ) .x. ( .1. .X. ( T ` ( b ` i ) ) ) ) )
85 84 eqcomd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( ( ( i .^ X ) ( .r ` ( Scalar ` Y ) ) X ) .x. ( .1. .X. ( T ` ( b ` i ) ) ) ) = ( ( X .x. .1. ) .X. ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) )
86 62 85 eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) = ( ( X .x. .1. ) .X. ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) )
87 86 mpteq2dva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( i e. ( 0 ... s ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) = ( i e. ( 0 ... s ) |-> ( ( X .x. .1. ) .X. ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) )
88 87 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 0 ... s ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) = ( Y gsum ( i e. ( 0 ... s ) |-> ( ( X .x. .1. ) .X. ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) )
89 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
90 eqid 
 |-  ( +g ` Y ) = ( +g ` Y )
91 76 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Ring )
92 ovexd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0 ... s ) e. _V )
93 4 matlmod 
 |-  ( ( N e. Fin /\ P e. Ring ) -> Y e. LMod )
94 46 93 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. LMod )
95 94 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. LMod )
96 11 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R e. Ring )
97 96 25 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> X e. ( Base ` P ) )
98 34 36 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> P = ( Scalar ` Y ) )
99 98 eqcomd 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( Scalar ` Y ) = P )
100 99 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( Base ` ( Scalar ` Y ) ) = ( Base ` P ) )
101 97 100 eleqtrrd 
 |-  ( ( N e. Fin /\ R e. CRing ) -> X e. ( Base ` ( Scalar ` Y ) ) )
102 101 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> X e. ( Base ` ( Scalar ` Y ) ) )
103 49 77 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> .1. e. ( Base ` Y ) )
104 58 80 8 81 lmodvscl 
 |-  ( ( Y e. LMod /\ X e. ( Base ` ( Scalar ` Y ) ) /\ .1. e. ( Base ` Y ) ) -> ( X .x. .1. ) e. ( Base ` Y ) )
105 95 102 103 104 syl3anc 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( X .x. .1. ) e. ( Base ` Y ) )
106 105 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( X .x. .1. ) e. ( Base ` Y ) )
107 95 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> Y e. LMod )
108 36 eqcomd 
 |-  ( ( N e. Fin /\ P e. CRing ) -> ( Scalar ` Y ) = P )
109 108 fveq2d 
 |-  ( ( N e. Fin /\ P e. CRing ) -> ( Base ` ( Scalar ` Y ) ) = ( Base ` P ) )
110 35 109 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Base ` ( Scalar ` Y ) ) = ( Base ` P ) )
111 110 eleq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( i .^ X ) e. ( Base ` ( Scalar ` Y ) ) <-> ( i .^ X ) e. ( Base ` P ) ) )
112 111 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( ( i .^ X ) e. ( Base ` ( Scalar ` Y ) ) <-> ( i .^ X ) e. ( Base ` P ) ) )
113 72 112 mpbird 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( i .^ X ) e. ( Base ` ( Scalar ` Y ) ) )
114 58 80 8 81 lmodvscl 
 |-  ( ( Y e. LMod /\ ( i .^ X ) e. ( Base ` ( Scalar ` Y ) ) /\ ( T ` ( b ` i ) ) e. ( Base ` Y ) ) -> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
115 107 113 57 114 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
116 simpl1 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> N e. Fin )
117 23 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> R e. Ring )
118 simprl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> s e. NN0 )
119 eqid 
 |-  ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) = ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) )
120 fzfid 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ s e. NN0 ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( 0 ... s ) e. Fin )
121 ovexd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ s e. NN0 ) /\ b e. ( B ^m ( 0 ... s ) ) ) /\ i e. ( 0 ... s ) ) -> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) e. _V )
122 fvexd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ s e. NN0 ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( 0g ` Y ) e. _V )
123 119 120 121 122 fsuppmptdm 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ s e. NN0 ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) finSupp ( 0g ` Y ) )
124 116 117 118 54 123 syl31anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) finSupp ( 0g ` Y ) )
125 58 89 90 9 91 92 106 115 124 gsummulc2 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 0 ... s ) |-> ( ( X .x. .1. ) .X. ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) = ( ( X .x. .1. ) .X. ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) )
126 88 125 eqtr2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( X .x. .1. ) .X. ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) = ( Y gsum ( i e. ( 0 ... s ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) )