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 18 20 27 mulgnn0cld 
 |-  ( ( ( ( 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 ) )
72 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 ) )
73 71 72 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 ) ) )
74 46 48 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. Ring )
75 74 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Ring )
76 58 10 ringidcl 
 |-  ( Y e. Ring -> .1. e. ( Base ` Y ) )
77 75 76 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> .1. e. ( Base ` Y ) )
78 77 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 ) )
79 eqid 
 |-  ( Scalar ` Y ) = ( Scalar ` Y )
80 eqid 
 |-  ( Base ` ( Scalar ` Y ) ) = ( Base ` ( Scalar ` Y ) )
81 eqid 
 |-  ( .r ` ( Scalar ` Y ) ) = ( .r ` ( Scalar ` Y ) )
82 58 79 80 81 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 ) ) ) ) )
83 66 70 73 78 57 82 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 ) ) ) ) )
84 83 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 ) ) ) ) )
85 62 84 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 ) ) ) ) )
86 85 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 ) ) ) ) ) )
87 86 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 ) ) ) ) ) ) )
88 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
89 75 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Ring )
90 ovexd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0 ... s ) e. _V )
91 4 matlmod 
 |-  ( ( N e. Fin /\ P e. Ring ) -> Y e. LMod )
92 46 91 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. LMod )
93 92 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. LMod )
94 11 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R e. Ring )
95 94 25 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> X e. ( Base ` P ) )
96 34 36 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> P = ( Scalar ` Y ) )
97 96 eqcomd 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( Scalar ` Y ) = P )
98 97 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( Base ` ( Scalar ` Y ) ) = ( Base ` P ) )
99 95 98 eleqtrrd 
 |-  ( ( N e. Fin /\ R e. CRing ) -> X e. ( Base ` ( Scalar ` Y ) ) )
100 99 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> X e. ( Base ` ( Scalar ` Y ) ) )
101 49 76 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> .1. e. ( Base ` Y ) )
102 58 79 8 80 lmodvscl 
 |-  ( ( Y e. LMod /\ X e. ( Base ` ( Scalar ` Y ) ) /\ .1. e. ( Base ` Y ) ) -> ( X .x. .1. ) e. ( Base ` Y ) )
103 93 100 101 102 syl3anc 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( X .x. .1. ) e. ( Base ` Y ) )
104 103 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 ) )
105 93 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 )
106 36 eqcomd 
 |-  ( ( N e. Fin /\ P e. CRing ) -> ( Scalar ` Y ) = P )
107 106 fveq2d 
 |-  ( ( N e. Fin /\ P e. CRing ) -> ( Base ` ( Scalar ` Y ) ) = ( Base ` P ) )
108 35 107 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Base ` ( Scalar ` Y ) ) = ( Base ` P ) )
109 108 eleq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( i .^ X ) e. ( Base ` ( Scalar ` Y ) ) <-> ( i .^ X ) e. ( Base ` P ) ) )
110 109 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 ) ) )
111 71 110 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 ) ) )
112 58 79 8 80 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 ) )
113 105 111 57 112 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 ) )
114 simpl1 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> N e. Fin )
115 23 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> R e. Ring )
116 simprl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> s e. NN0 )
117 eqid 
 |-  ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) = ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) )
118 fzfid 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ s e. NN0 ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( 0 ... s ) e. Fin )
119 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 )
120 fvexd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ s e. NN0 ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( 0g ` Y ) e. _V )
121 117 118 119 120 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 ) )
122 114 115 116 54 121 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 ) )
123 58 88 9 89 90 104 113 122 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 ) ) ) ) ) ) )
124 87 123 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 ) ) ) ) ) )