Metamath Proof Explorer

Theorem cpmadugsumlemF

Description: Lemma F for cpmadugsum . (Contributed by AV, 7-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 )
cpmadugsum.g 
|- .+ = ( +g ` Y )
cpmadugsum.s 
|- .- = ( -g ` Y )
Assertion cpmadugsumlemF 
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( X .x. .1. ) .X. ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( ( T ` M ) .X. ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )

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 cpmadugsum.g 
 |-  .+ = ( +g ` Y )
12 cpmadugsum.s 
 |-  .- = ( -g ` Y )
13 nnnn0 
 |-  ( s e. NN -> s e. NN0 )
14 1 2 3 4 5 6 7 8 9 10 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 ) ) ) ) ) )
15 13 14 sylanr1 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ 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 ) ) ) ) ) )
16 1 2 3 4 5 6 7 8 9 10 cpmadugsumlemC 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN0 /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( T ` M ) .X. ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) = ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) )
17 13 16 sylanr1 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( T ` M ) .X. ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) = ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) )
18 15 17 oveq12d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( X .x. .1. ) .X. ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( ( T ` M ) .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 ) ) ) ) ) .- ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) )
19 nncn 
 |-  ( s e. NN -> s e. CC )
20 npcan1 
 |-  ( s e. CC -> ( ( s - 1 ) + 1 ) = s )
21 20 eqcomd 
 |-  ( s e. CC -> s = ( ( s - 1 ) + 1 ) )
22 19 21 syl 
 |-  ( s e. NN -> s = ( ( s - 1 ) + 1 ) )
23 22 oveq2d 
 |-  ( s e. NN -> ( 0 ... s ) = ( 0 ... ( ( s - 1 ) + 1 ) ) )
24 23 mpteq1d 
 |-  ( s e. NN -> ( i e. ( 0 ... s ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) = ( i e. ( 0 ... ( ( s - 1 ) + 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) )
25 24 oveq2d 
 |-  ( s e. NN -> ( Y gsum ( i e. ( 0 ... s ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) = ( Y gsum ( i e. ( 0 ... ( ( s - 1 ) + 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) )
26 25 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ 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 - 1 ) + 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) )
27 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
28 crngring 
 |-  ( R e. CRing -> R e. Ring )
29 28 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
30 29 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ R e. Ring ) )
31 3 4 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Y e. Ring )
32 30 31 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Ring )
33 ringcmn 
 |-  ( Y e. Ring -> Y e. CMnd )
34 32 33 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. CMnd )
35 34 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. CMnd )
36 nnm1nn0 
 |-  ( s e. NN -> ( s - 1 ) e. NN0 )
37 36 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( s - 1 ) e. NN0 )
38 simpll1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( ( s - 1 ) + 1 ) ) ) -> N e. Fin )
39 28 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R e. Ring )
40 39 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> R e. Ring )
41 40 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( ( s - 1 ) + 1 ) ) ) -> R e. Ring )
42 elmapi 
 |-  ( b e. ( B ^m ( 0 ... s ) ) -> b : ( 0 ... s ) --> B )
43 23 feq2d 
 |-  ( s e. NN -> ( b : ( 0 ... s ) --> B <-> b : ( 0 ... ( ( s - 1 ) + 1 ) ) --> B ) )
44 42 43 syl5ibcom 
 |-  ( b e. ( B ^m ( 0 ... s ) ) -> ( s e. NN -> b : ( 0 ... ( ( s - 1 ) + 1 ) ) --> B ) )
45 44 impcom 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> b : ( 0 ... ( ( s - 1 ) + 1 ) ) --> B )
46 45 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> b : ( 0 ... ( ( s - 1 ) + 1 ) ) --> B )
47 46 ffvelrnda 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( ( s - 1 ) + 1 ) ) ) -> ( b ` i ) e. B )
48 elfznn0 
 |-  ( i e. ( 0 ... ( ( s - 1 ) + 1 ) ) -> i e. NN0 )
49 48 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( ( s - 1 ) + 1 ) ) ) -> i e. NN0 )
50 1nn0 
 |-  1 e. NN0
51 50 a1i 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( ( s - 1 ) + 1 ) ) ) -> 1 e. NN0 )
52 49 51 nn0addcld 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( ( s - 1 ) + 1 ) ) ) -> ( i + 1 ) e. NN0 )
53 1 2 5 3 4 27 8 7 6 mat2pmatscmxcl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( ( b ` i ) e. B /\ ( i + 1 ) e. NN0 ) ) -> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
54 38 41 47 52 53 syl22anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( ( s - 1 ) + 1 ) ) ) -> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
55 27 11 35 37 54 gsummptfzsplit 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 0 ... ( ( s - 1 ) + 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) = ( ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .+ ( Y gsum ( i e. { ( ( s - 1 ) + 1 ) } |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) )
56 ringmnd 
 |-  ( Y e. Ring -> Y e. Mnd )
57 32 56 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Mnd )
58 57 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Mnd )
59 ovexd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( s - 1 ) + 1 ) e. _V )
60 simpl1 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> N e. Fin )
61 nn0fz0 
 |-  ( s e. NN0 <-> s e. ( 0 ... s ) )
62 13 61 sylib 
 |-  ( s e. NN -> s e. ( 0 ... s ) )
63 ffvelrn 
 |-  ( ( b : ( 0 ... s ) --> B /\ s e. ( 0 ... s ) ) -> ( b ` s ) e. B )
64 42 62 63 syl2anr 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( b ` s ) e. B )
65 13 adantr 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> s e. NN0 )
66 50 a1i 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> 1 e. NN0 )
67 65 66 nn0addcld 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( s + 1 ) e. NN0 )
68 64 67 jca 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( ( b ` s ) e. B /\ ( s + 1 ) e. NN0 ) )
69 68 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( b ` s ) e. B /\ ( s + 1 ) e. NN0 ) )
70 1 2 5 3 4 27 8 7 6 mat2pmatscmxcl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( ( b ` s ) e. B /\ ( s + 1 ) e. NN0 ) ) -> ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) e. ( Base ` Y ) )
71 60 40 69 70 syl21anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) e. ( Base ` Y ) )
72 oveq1 
 |-  ( i = ( ( s - 1 ) + 1 ) -> ( i + 1 ) = ( ( ( s - 1 ) + 1 ) + 1 ) )
73 72 oveq1d 
 |-  ( i = ( ( s - 1 ) + 1 ) -> ( ( i + 1 ) .^ X ) = ( ( ( ( s - 1 ) + 1 ) + 1 ) .^ X ) )
74 2fveq3 
 |-  ( i = ( ( s - 1 ) + 1 ) -> ( T ` ( b ` i ) ) = ( T ` ( b ` ( ( s - 1 ) + 1 ) ) ) )
75 73 74 oveq12d 
 |-  ( i = ( ( s - 1 ) + 1 ) -> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) = ( ( ( ( ( s - 1 ) + 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( ( s - 1 ) + 1 ) ) ) ) )
76 19 20 syl 
 |-  ( s e. NN -> ( ( s - 1 ) + 1 ) = s )
77 76 oveq1d 
 |-  ( s e. NN -> ( ( ( s - 1 ) + 1 ) + 1 ) = ( s + 1 ) )
78 77 oveq1d 
 |-  ( s e. NN -> ( ( ( ( s - 1 ) + 1 ) + 1 ) .^ X ) = ( ( s + 1 ) .^ X ) )
79 76 fveq2d 
 |-  ( s e. NN -> ( b ` ( ( s - 1 ) + 1 ) ) = ( b ` s ) )
80 79 fveq2d 
 |-  ( s e. NN -> ( T ` ( b ` ( ( s - 1 ) + 1 ) ) ) = ( T ` ( b ` s ) ) )
81 78 80 oveq12d 
 |-  ( s e. NN -> ( ( ( ( ( s - 1 ) + 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( ( s - 1 ) + 1 ) ) ) ) = ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) )
82 81 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( ( s - 1 ) + 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( ( s - 1 ) + 1 ) ) ) ) = ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) )
83 75 82 sylan9eqr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i = ( ( s - 1 ) + 1 ) ) -> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) = ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) )
84 27 58 59 71 83 gsumsnd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. { ( ( s - 1 ) + 1 ) } |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) = ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) )
85 84 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .+ ( Y gsum ( i e. { ( ( s - 1 ) + 1 ) } |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) = ( ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) )
86 26 55 85 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ 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 - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) )
87 13 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> s e. NN0 )
88 3 4 pmatlmod 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Y e. LMod )
89 29 88 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. LMod )
90 89 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. LMod )
91 90 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. LMod )
92 91 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> Y e. LMod )
93 3 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
94 28 93 syl 
 |-  ( R e. CRing -> P e. Ring )
95 94 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P e. Ring )
96 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
97 96 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
98 95 97 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( mulGrp ` P ) e. Mnd )
99 98 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( mulGrp ` P ) e. Mnd )
100 99 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( mulGrp ` P ) e. Mnd )
101 elfznn0 
 |-  ( i e. ( 0 ... s ) -> i e. NN0 )
102 101 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> i e. NN0 )
103 eqid 
 |-  ( Base ` P ) = ( Base ` P )
104 6 3 103 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` P ) )
105 28 104 syl 
 |-  ( R e. CRing -> X e. ( Base ` P ) )
106 105 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> X e. ( Base ` P ) )
107 106 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> X e. ( Base ` P ) )
108 107 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> X e. ( Base ` P ) )
109 96 103 mgpbas 
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
110 109 7 mulgnn0cl 
 |-  ( ( ( mulGrp ` P ) e. Mnd /\ i e. NN0 /\ X e. ( Base ` P ) ) -> ( i .^ X ) e. ( Base ` P ) )
111 100 102 108 110 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( i .^ X ) e. ( Base ` P ) )
112 3 ply1crng 
 |-  ( R e. CRing -> P e. CRing )
113 112 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ P e. CRing ) )
114 113 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ P e. CRing ) )
115 4 matsca2 
 |-  ( ( N e. Fin /\ P e. CRing ) -> P = ( Scalar ` Y ) )
116 114 115 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P = ( Scalar ` Y ) )
117 116 eqcomd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Scalar ` Y ) = P )
118 117 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Base ` ( Scalar ` Y ) ) = ( Base ` P ) )
119 118 eleq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( i .^ X ) e. ( Base ` ( Scalar ` Y ) ) <-> ( i .^ X ) e. ( Base ` P ) ) )
120 119 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( i .^ X ) e. ( Base ` ( Scalar ` Y ) ) <-> ( i .^ X ) e. ( Base ` P ) ) )
121 120 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( ( i .^ X ) e. ( Base ` ( Scalar ` Y ) ) <-> ( i .^ X ) e. ( Base ` P ) ) )
122 111 121 mpbird 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( i .^ X ) e. ( Base ` ( Scalar ` Y ) ) )
123 32 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Ring )
124 123 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> Y e. Ring )
125 simpll1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> N e. Fin )
126 40 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> R e. Ring )
127 simpll3 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> M e. B )
128 5 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
129 125 126 127 128 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( T ` M ) e. ( Base ` Y ) )
130 87 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> s e. NN0 )
131 simprr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> b e. ( B ^m ( 0 ... s ) ) )
132 131 anim1i 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( b e. ( B ^m ( 0 ... s ) ) /\ i e. ( 0 ... s ) ) )
133 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 ) )
134 125 126 130 132 133 syl31anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( T ` ( b ` i ) ) e. ( Base ` Y ) )
135 27 9 ringcl 
 |-  ( ( Y e. Ring /\ ( T ` M ) e. ( Base ` Y ) /\ ( T ` ( b ` i ) ) e. ( Base ` Y ) ) -> ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
136 124 129 134 135 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
137 eqid 
 |-  ( Scalar ` Y ) = ( Scalar ` Y )
138 eqid 
 |-  ( Base ` ( Scalar ` Y ) ) = ( Base ` ( Scalar ` Y ) )
139 27 137 8 138 lmodvscl 
 |-  ( ( Y e. LMod /\ ( i .^ X ) e. ( Base ` ( Scalar ` Y ) ) /\ ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) ) -> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) e. ( Base ` Y ) )
140 92 122 136 139 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) e. ( Base ` Y ) )
141 27 11 35 87 140 gsummptfzsplitl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( Y gsum ( i e. { 0 } |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) )
142 0nn0 
 |-  0 e. NN0
143 142 a1i 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> 0 e. NN0 )
144 eqid 
 |-  ( 0g ` ( mulGrp ` P ) ) = ( 0g ` ( mulGrp ` P ) )
145 109 144 7 mulg0 
 |-  ( X e. ( Base ` P ) -> ( 0 .^ X ) = ( 0g ` ( mulGrp ` P ) ) )
146 106 145 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( 0 .^ X ) = ( 0g ` ( mulGrp ` P ) ) )
147 146 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0 .^ X ) = ( 0g ` ( mulGrp ` P ) ) )
148 147 oveq1d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 0 .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( 0g ` ( mulGrp ` P ) ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
149 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
150 96 149 ringidval 
 |-  ( 1r ` P ) = ( 0g ` ( mulGrp ` P ) )
151 150 a1i 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 1r ` P ) = ( 0g ` ( mulGrp ` P ) ) )
152 151 eqcomd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0g ` ( mulGrp ` P ) ) = ( 1r ` P ) )
153 152 oveq1d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 0g ` ( mulGrp ` P ) ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( 1r ` P ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
154 116 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> P = ( Scalar ` Y ) )
155 154 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 1r ` P ) = ( 1r ` ( Scalar ` Y ) ) )
156 155 oveq1d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 1r ` P ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( 1r ` ( Scalar ` Y ) ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
157 28 128 syl3an2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
158 157 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` M ) e. ( Base ` Y ) )
159 simpl 
 |-  ( ( b : ( 0 ... s ) --> B /\ s e. NN ) -> b : ( 0 ... s ) --> B )
160 elnn0uz 
 |-  ( s e. NN0 <-> s e. ( ZZ>= ` 0 ) )
161 13 160 sylib 
 |-  ( s e. NN -> s e. ( ZZ>= ` 0 ) )
162 eluzfz1 
 |-  ( s e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... s ) )
163 161 162 syl 
 |-  ( s e. NN -> 0 e. ( 0 ... s ) )
164 163 adantl 
 |-  ( ( b : ( 0 ... s ) --> B /\ s e. NN ) -> 0 e. ( 0 ... s ) )
165 159 164 ffvelrnd 
 |-  ( ( b : ( 0 ... s ) --> B /\ s e. NN ) -> ( b ` 0 ) e. B )
166 165 ex 
 |-  ( b : ( 0 ... s ) --> B -> ( s e. NN -> ( b ` 0 ) e. B ) )
167 42 166 syl 
 |-  ( b e. ( B ^m ( 0 ... s ) ) -> ( s e. NN -> ( b ` 0 ) e. B ) )
168 167 impcom 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( b ` 0 ) e. B )
169 168 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( b ` 0 ) e. B )
170 5 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` 0 ) e. B ) -> ( T ` ( b ` 0 ) ) e. ( Base ` Y ) )
171 60 40 169 170 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` ( b ` 0 ) ) e. ( Base ` Y ) )
172 27 9 ringcl 
 |-  ( ( Y e. Ring /\ ( T ` M ) e. ( Base ` Y ) /\ ( T ` ( b ` 0 ) ) e. ( Base ` Y ) ) -> ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) e. ( Base ` Y ) )
173 123 158 171 172 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) e. ( Base ` Y ) )
174 eqid 
 |-  ( 1r ` ( Scalar ` Y ) ) = ( 1r ` ( Scalar ` Y ) )
175 27 137 8 174 lmodvs1 
 |-  ( ( Y e. LMod /\ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) e. ( Base ` Y ) ) -> ( ( 1r ` ( Scalar ` Y ) ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) )
176 91 173 175 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 1r ` ( Scalar ` Y ) ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) )
177 156 176 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 1r ` P ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) )
178 148 153 177 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 0 .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) )
179 178 173 eqeltrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 0 .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) e. ( Base ` Y ) )
180 oveq1 
 |-  ( i = 0 -> ( i .^ X ) = ( 0 .^ X ) )
181 2fveq3 
 |-  ( i = 0 -> ( T ` ( b ` i ) ) = ( T ` ( b ` 0 ) ) )
182 181 oveq2d 
 |-  ( i = 0 -> ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) = ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) )
183 180 182 oveq12d 
 |-  ( i = 0 -> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) = ( ( 0 .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
184 183 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i = 0 ) -> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) = ( ( 0 .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
185 27 58 143 179 184 gsumsnd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. { 0 } |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) = ( ( 0 .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
186 109 150 7 mulg0 
 |-  ( X e. ( Base ` P ) -> ( 0 .^ X ) = ( 1r ` P ) )
187 106 186 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( 0 .^ X ) = ( 1r ` P ) )
188 187 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0 .^ X ) = ( 1r ` P ) )
189 188 oveq1d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 0 .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( 1r ` P ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
190 185 189 177 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. { 0 } |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) = ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) )
191 190 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( Y gsum ( i e. { 0 } |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
192 141 191 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
193 86 192 oveq12d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ 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 ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) .- ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
194 fzfid 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0 ... ( s - 1 ) ) e. Fin )
195 simpll1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> N e. Fin )
196 40 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> R e. Ring )
197 42 adantl 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> b : ( 0 ... s ) --> B )
198 197 adantr 
 |-  ( ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> b : ( 0 ... s ) --> B )
199 nnz 
 |-  ( s e. NN -> s e. ZZ )
200 fzoval 
 |-  ( s e. ZZ -> ( 0 ..^ s ) = ( 0 ... ( s - 1 ) ) )
201 199 200 syl 
 |-  ( s e. NN -> ( 0 ..^ s ) = ( 0 ... ( s - 1 ) ) )
202 201 eqcomd 
 |-  ( s e. NN -> ( 0 ... ( s - 1 ) ) = ( 0 ..^ s ) )
203 202 eleq2d 
 |-  ( s e. NN -> ( i e. ( 0 ... ( s - 1 ) ) <-> i e. ( 0 ..^ s ) ) )
204 elfzofz 
 |-  ( i e. ( 0 ..^ s ) -> i e. ( 0 ... s ) )
205 203 204 syl6bi 
 |-  ( s e. NN -> ( i e. ( 0 ... ( s - 1 ) ) -> i e. ( 0 ... s ) ) )
206 205 adantr 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( i e. ( 0 ... ( s - 1 ) ) -> i e. ( 0 ... s ) ) )
207 206 imp 
 |-  ( ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> i e. ( 0 ... s ) )
208 198 207 ffvelrnd 
 |-  ( ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> ( b ` i ) e. B )
209 208 adantll 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> ( b ` i ) e. B )
210 elfznn0 
 |-  ( i e. ( 0 ... ( s - 1 ) ) -> i e. NN0 )
211 210 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> i e. NN0 )
212 50 a1i 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> 1 e. NN0 )
213 211 212 nn0addcld 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> ( i + 1 ) e. NN0 )
214 195 196 209 213 53 syl22anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
215 214 ralrimiva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> A. i e. ( 0 ... ( s - 1 ) ) ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
216 27 35 194 215 gsummptcl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) e. ( Base ` Y ) )
217 27 11 cmncom 
 |-  ( ( Y e. CMnd /\ ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) e. ( Base ` Y ) /\ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) e. ( Base ` Y ) ) -> ( ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) = ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) )
218 35 216 71 217 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) = ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) )
219 218 oveq1d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) .- ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) = ( ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
220 ringgrp 
 |-  ( Y e. Ring -> Y e. Grp )
221 32 220 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Grp )
222 221 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Grp )
223 fzfid 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 1 ... s ) e. Fin )
224 91 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> Y e. LMod )
225 99 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( mulGrp ` P ) e. Mnd )
226 elfznn 
 |-  ( i e. ( 1 ... s ) -> i e. NN )
227 226 nnnn0d 
 |-  ( i e. ( 1 ... s ) -> i e. NN0 )
228 227 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> i e. NN0 )
229 107 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> X e. ( Base ` P ) )
230 225 228 229 110 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( i .^ X ) e. ( Base ` P ) )
231 116 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Base ` P ) = ( Base ` ( Scalar ` Y ) ) )
232 231 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Base ` P ) = ( Base ` ( Scalar ` Y ) ) )
233 232 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( Base ` P ) = ( Base ` ( Scalar ` Y ) ) )
234 230 233 eleqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( i .^ X ) e. ( Base ` ( Scalar ` Y ) ) )
235 123 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> Y e. Ring )
236 158 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( T ` M ) e. ( Base ` Y ) )
237 simpll1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> N e. Fin )
238 40 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> R e. Ring )
239 197 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> b : ( 0 ... s ) --> B )
240 239 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> b : ( 0 ... s ) --> B )
241 1eluzge0 
 |-  1 e. ( ZZ>= ` 0 )
242 fzss1 
 |-  ( 1 e. ( ZZ>= ` 0 ) -> ( 1 ... s ) C_ ( 0 ... s ) )
243 241 242 mp1i 
 |-  ( s e. NN -> ( 1 ... s ) C_ ( 0 ... s ) )
244 243 sseld 
 |-  ( s e. NN -> ( i e. ( 1 ... s ) -> i e. ( 0 ... s ) ) )
245 244 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( i e. ( 1 ... s ) -> i e. ( 0 ... s ) ) )
246 245 imp 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> i e. ( 0 ... s ) )
247 240 246 ffvelrnd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( b ` i ) e. B )
248 5 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` i ) e. B ) -> ( T ` ( b ` i ) ) e. ( Base ` Y ) )
249 237 238 247 248 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( T ` ( b ` i ) ) e. ( Base ` Y ) )
250 235 236 249 135 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
251 224 234 250 139 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) e. ( Base ` Y ) )
252 251 ralrimiva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> A. i e. ( 1 ... s ) ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) e. ( Base ` Y ) )
253 27 35 223 252 gsummptcl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) e. ( Base ` Y ) )
254 27 11 12 grpaddsubass 
 |-  ( ( Y e. Grp /\ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) e. ( Base ` Y ) /\ ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) e. ( Base ` Y ) /\ ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) e. ( Base ` Y ) ) ) -> ( ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .- ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) ) )
255 222 71 216 253 254 syl13anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .- ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) ) )
256 oveq1 
 |-  ( x = i -> ( x - 1 ) = ( i - 1 ) )
257 256 oveq1d 
 |-  ( x = i -> ( ( x - 1 ) + 1 ) = ( ( i - 1 ) + 1 ) )
258 257 oveq1d 
 |-  ( x = i -> ( ( ( x - 1 ) + 1 ) .^ X ) = ( ( ( i - 1 ) + 1 ) .^ X ) )
259 256 fveq2d 
 |-  ( x = i -> ( b ` ( x - 1 ) ) = ( b ` ( i - 1 ) ) )
260 259 fveq2d 
 |-  ( x = i -> ( T ` ( b ` ( x - 1 ) ) ) = ( T ` ( b ` ( i - 1 ) ) ) )
261 258 260 oveq12d 
 |-  ( x = i -> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) = ( ( ( ( i - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) )
262 261 cbvmptv 
 |-  ( x e. ( 1 ... s ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) = ( i e. ( 1 ... s ) |-> ( ( ( ( i - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) )
263 226 nncnd 
 |-  ( i e. ( 1 ... s ) -> i e. CC )
264 263 adantl 
 |-  ( ( s e. NN /\ i e. ( 1 ... s ) ) -> i e. CC )
265 npcan1 
 |-  ( i e. CC -> ( ( i - 1 ) + 1 ) = i )
266 264 265 syl 
 |-  ( ( s e. NN /\ i e. ( 1 ... s ) ) -> ( ( i - 1 ) + 1 ) = i )
267 266 oveq1d 
 |-  ( ( s e. NN /\ i e. ( 1 ... s ) ) -> ( ( ( i - 1 ) + 1 ) .^ X ) = ( i .^ X ) )
268 267 oveq1d 
 |-  ( ( s e. NN /\ i e. ( 1 ... s ) ) -> ( ( ( ( i - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) = ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) )
269 268 mpteq2dva 
 |-  ( s e. NN -> ( i e. ( 1 ... s ) |-> ( ( ( ( i - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) ) = ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) ) )
270 262 269 syl5eq 
 |-  ( s e. NN -> ( x e. ( 1 ... s ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) = ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) ) )
271 270 oveq2d 
 |-  ( s e. NN -> ( Y gsum ( x e. ( 1 ... s ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) ) = ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) ) ) )
272 271 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( x e. ( 1 ... s ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) ) = ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) ) ) )
273 272 oveq1d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsum ( x e. ( 1 ... s ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) ) .- ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) ) ) .- ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) )
274 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
275 1zzd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> 1 e. ZZ )
276 0zd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> 0 e. ZZ )
277 37 nn0zd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( s - 1 ) e. ZZ )
278 oveq1 
 |-  ( i = ( x - 1 ) -> ( i + 1 ) = ( ( x - 1 ) + 1 ) )
279 278 oveq1d 
 |-  ( i = ( x - 1 ) -> ( ( i + 1 ) .^ X ) = ( ( ( x - 1 ) + 1 ) .^ X ) )
280 2fveq3 
 |-  ( i = ( x - 1 ) -> ( T ` ( b ` i ) ) = ( T ` ( b ` ( x - 1 ) ) ) )
281 279 280 oveq12d 
 |-  ( i = ( x - 1 ) -> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) = ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) )
282 27 274 35 275 276 277 214 281 gsummptshft 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) = ( Y gsum ( x e. ( ( 0 + 1 ) ... ( ( s - 1 ) + 1 ) ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) ) )
283 0p1e1 
 |-  ( 0 + 1 ) = 1
284 283 a1i 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0 + 1 ) = 1 )
285 76 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( s - 1 ) + 1 ) = s )
286 284 285 oveq12d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 0 + 1 ) ... ( ( s - 1 ) + 1 ) ) = ( 1 ... s ) )
287 286 mpteq1d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( x e. ( ( 0 + 1 ) ... ( ( s - 1 ) + 1 ) ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) = ( x e. ( 1 ... s ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) )
288 287 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( x e. ( ( 0 + 1 ) ... ( ( s - 1 ) + 1 ) ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) ) = ( Y gsum ( x e. ( 1 ... s ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) ) )
289 282 288 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) = ( Y gsum ( x e. ( 1 ... s ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) ) )
290 289 oveq1d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .- ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( Y gsum ( x e. ( 1 ... s ) |-> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) ) ) .- ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) )
291 ringabl 
 |-  ( Y e. Ring -> Y e. Abel )
292 32 291 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Abel )
293 292 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Abel )
294 226 adantl 
 |-  ( ( s e. NN /\ i e. ( 1 ... s ) ) -> i e. NN )
295 nnz 
 |-  ( i e. NN -> i e. ZZ )
296 elfzm1b 
 |-  ( ( i e. ZZ /\ s e. ZZ ) -> ( i e. ( 1 ... s ) <-> ( i - 1 ) e. ( 0 ... ( s - 1 ) ) ) )
297 295 199 296 syl2an 
 |-  ( ( i e. NN /\ s e. NN ) -> ( i e. ( 1 ... s ) <-> ( i - 1 ) e. ( 0 ... ( s - 1 ) ) ) )
298 201 adantl 
 |-  ( ( i e. NN /\ s e. NN ) -> ( 0 ..^ s ) = ( 0 ... ( s - 1 ) ) )
299 298 eqcomd 
 |-  ( ( i e. NN /\ s e. NN ) -> ( 0 ... ( s - 1 ) ) = ( 0 ..^ s ) )
300 299 eleq2d 
 |-  ( ( i e. NN /\ s e. NN ) -> ( ( i - 1 ) e. ( 0 ... ( s - 1 ) ) <-> ( i - 1 ) e. ( 0 ..^ s ) ) )
301 elfzofz 
 |-  ( ( i - 1 ) e. ( 0 ..^ s ) -> ( i - 1 ) e. ( 0 ... s ) )
302 300 301 syl6bi 
 |-  ( ( i e. NN /\ s e. NN ) -> ( ( i - 1 ) e. ( 0 ... ( s - 1 ) ) -> ( i - 1 ) e. ( 0 ... s ) ) )
303 297 302 sylbid 
 |-  ( ( i e. NN /\ s e. NN ) -> ( i e. ( 1 ... s ) -> ( i - 1 ) e. ( 0 ... s ) ) )
304 303 expimpd 
 |-  ( i e. NN -> ( ( s e. NN /\ i e. ( 1 ... s ) ) -> ( i - 1 ) e. ( 0 ... s ) ) )
305 294 304 mpcom 
 |-  ( ( s e. NN /\ i e. ( 1 ... s ) ) -> ( i - 1 ) e. ( 0 ... s ) )
306 305 ex 
 |-  ( s e. NN -> ( i e. ( 1 ... s ) -> ( i - 1 ) e. ( 0 ... s ) ) )
307 306 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( i e. ( 1 ... s ) -> ( i - 1 ) e. ( 0 ... s ) ) )
308 307 imp 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( i - 1 ) e. ( 0 ... s ) )
309 240 308 ffvelrnd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( b ` ( i - 1 ) ) e. B )
310 1 2 5 3 4 27 8 7 6 mat2pmatscmxcl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( ( b ` ( i - 1 ) ) e. B /\ i e. NN0 ) ) -> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) e. ( Base ` Y ) )
311 237 238 309 228 310 syl22anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) e. ( Base ` Y ) )
312 eqid 
 |-  ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) ) = ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) )
313 eqid 
 |-  ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) = ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) )
314 27 12 293 223 311 251 312 313 gsummptfidmsub 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) ) ) .- ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) )
315 273 290 314 3eqtr4d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .- ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) = ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) )
316 315 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .- ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) ) = ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) ) )
317 222 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> Y e. Grp )
318 27 12 grpsubcl 
 |-  ( ( Y e. Grp /\ ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) e. ( Base ` Y ) /\ ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) e. ( Base ` Y ) ) -> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) e. ( Base ` Y ) )
319 317 311 251 318 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) e. ( Base ` Y ) )
320 319 ralrimiva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> A. i e. ( 1 ... s ) ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) e. ( Base ` Y ) )
321 27 35 223 320 gsummptcl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) e. ( Base ` Y ) )
322 27 11 cmncom 
 |-  ( ( Y e. CMnd /\ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) e. ( Base ` Y ) /\ ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) e. ( Base ` Y ) ) -> ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) )
323 35 71 321 322 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) )
324 255 316 323 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) )
325 324 oveq1d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
326 27 11 mndcl 
 |-  ( ( Y e. Mnd /\ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) e. ( Base ` Y ) /\ ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) e. ( Base ` Y ) ) -> ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) e. ( Base ` Y ) )
327 58 71 216 326 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) e. ( Base ` Y ) )
328 27 11 12 293 327 253 173 ablsubsub4 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
329 27 11 12 grpaddsubass 
 |-  ( ( Y e. Grp /\ ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) e. ( Base ` Y ) /\ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) e. ( Base ` Y ) /\ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) e. ( Base ` Y ) ) ) -> ( ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
330 222 321 71 173 329 syl13anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
331 325 328 330 3eqtr3d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .+ ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
332 5 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` ( i - 1 ) ) e. B ) -> ( T ` ( b ` ( i - 1 ) ) ) e. ( Base ` Y ) )
333 237 238 309 332 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( T ` ( b ` ( i - 1 ) ) ) e. ( Base ` Y ) )
334 27 8 137 138 12 224 234 333 250 lmodsubdi 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) = ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) )
335 334 eqcomd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) = ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) )
336 335 mpteq2dva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) = ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) )
337 336 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) = ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) )
338 337 oveq1d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
339 219 331 338 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( Y gsum ( i e. ( 0 ... ( s - 1 ) ) |-> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) .+ ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) ) .- ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
340 18 193 339 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( X .x. .1. ) .X. ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) .- ( ( T ` M ) .X. ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` i ) ) ) ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ X ) .x. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )