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 ffvelcdmda 
 |-  ( ( ( ( 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 ffvelcdm 
 |-  ( ( 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 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
94 eqid 
 |-  ( Base ` P ) = ( Base ` P )
95 93 94 mgpbas 
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
96 3 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
97 28 96 syl 
 |-  ( R e. CRing -> P e. Ring )
98 97 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P e. Ring )
99 93 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
100 98 99 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( mulGrp ` P ) e. Mnd )
101 100 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( mulGrp ` P ) e. Mnd )
102 101 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 )
103 elfznn0 
 |-  ( i e. ( 0 ... s ) -> i e. NN0 )
104 103 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 )
105 6 3 94 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` P ) )
106 28 105 syl 
 |-  ( R e. CRing -> X e. ( Base ` P ) )
107 106 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> 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 ) ) ) ) -> X e. ( Base ` P ) )
109 108 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 ) )
110 95 7 102 104 109 mulgnn0cld 
 |-  ( ( ( ( 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 ) )
111 3 ply1crng 
 |-  ( R e. CRing -> P e. CRing )
112 111 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ P e. CRing ) )
113 112 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ P e. CRing ) )
114 4 matsca2 
 |-  ( ( N e. Fin /\ P e. CRing ) -> P = ( Scalar ` Y ) )
115 113 114 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P = ( Scalar ` Y ) )
116 115 eqcomd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Scalar ` Y ) = P )
117 116 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Base ` ( Scalar ` Y ) ) = ( Base ` P ) )
118 117 eleq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( i .^ X ) e. ( Base ` ( Scalar ` Y ) ) <-> ( i .^ X ) e. ( Base ` P ) ) )
119 118 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 ) ) )
120 119 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 ) ) )
121 110 120 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 ) ) )
122 32 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Ring )
123 122 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 )
124 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 )
125 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 )
126 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 )
127 5 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
128 124 125 126 127 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 ) )
129 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 )
130 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 ) ) )
131 130 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 ) ) )
132 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 ) )
133 124 125 129 131 132 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 ) )
134 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 ) )
135 123 128 133 134 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 ) )
136 eqid 
 |-  ( Scalar ` Y ) = ( Scalar ` Y )
137 eqid 
 |-  ( Base ` ( Scalar ` Y ) ) = ( Base ` ( Scalar ` Y ) )
138 27 136 8 137 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 ) )
139 92 121 135 138 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 ) )
140 27 11 35 87 139 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 ) ) ) ) ) ) ) )
141 0nn0 
 |-  0 e. NN0
142 141 a1i 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> 0 e. NN0 )
143 eqid 
 |-  ( 0g ` ( mulGrp ` P ) ) = ( 0g ` ( mulGrp ` P ) )
144 95 143 7 mulg0 
 |-  ( X e. ( Base ` P ) -> ( 0 .^ X ) = ( 0g ` ( mulGrp ` P ) ) )
145 107 144 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( 0 .^ X ) = ( 0g ` ( mulGrp ` P ) ) )
146 145 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0 .^ X ) = ( 0g ` ( mulGrp ` P ) ) )
147 146 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 ) ) ) ) )
148 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
149 93 148 ringidval 
 |-  ( 1r ` P ) = ( 0g ` ( mulGrp ` P ) )
150 149 a1i 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 1r ` P ) = ( 0g ` ( mulGrp ` P ) ) )
151 150 eqcomd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0g ` ( mulGrp ` P ) ) = ( 1r ` P ) )
152 151 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 ) ) ) ) )
153 115 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> P = ( Scalar ` Y ) )
154 153 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 1r ` P ) = ( 1r ` ( Scalar ` Y ) ) )
155 154 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 ) ) ) ) )
156 28 127 syl3an2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
157 156 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` M ) e. ( Base ` Y ) )
158 simpl 
 |-  ( ( b : ( 0 ... s ) --> B /\ s e. NN ) -> b : ( 0 ... s ) --> B )
159 elnn0uz 
 |-  ( s e. NN0 <-> s e. ( ZZ>= ` 0 ) )
160 13 159 sylib 
 |-  ( s e. NN -> s e. ( ZZ>= ` 0 ) )
161 eluzfz1 
 |-  ( s e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... s ) )
162 160 161 syl 
 |-  ( s e. NN -> 0 e. ( 0 ... s ) )
163 162 adantl 
 |-  ( ( b : ( 0 ... s ) --> B /\ s e. NN ) -> 0 e. ( 0 ... s ) )
164 158 163 ffvelcdmd 
 |-  ( ( b : ( 0 ... s ) --> B /\ s e. NN ) -> ( b ` 0 ) e. B )
165 164 ex 
 |-  ( b : ( 0 ... s ) --> B -> ( s e. NN -> ( b ` 0 ) e. B ) )
166 42 165 syl 
 |-  ( b e. ( B ^m ( 0 ... s ) ) -> ( s e. NN -> ( b ` 0 ) e. B ) )
167 166 impcom 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( b ` 0 ) e. B )
168 167 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( b ` 0 ) e. B )
169 5 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` 0 ) e. B ) -> ( T ` ( b ` 0 ) ) e. ( Base ` Y ) )
170 60 40 168 169 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 ) )
171 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 ) )
172 122 157 170 171 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 ) )
173 eqid 
 |-  ( 1r ` ( Scalar ` Y ) ) = ( 1r ` ( Scalar ` Y ) )
174 27 136 8 173 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 ) ) ) )
175 91 172 174 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 ) ) ) )
176 155 175 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 ) ) ) )
177 147 152 176 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 ) ) ) )
178 177 172 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 ) )
179 oveq1 
 |-  ( i = 0 -> ( i .^ X ) = ( 0 .^ X ) )
180 2fveq3 
 |-  ( i = 0 -> ( T ` ( b ` i ) ) = ( T ` ( b ` 0 ) ) )
181 180 oveq2d 
 |-  ( i = 0 -> ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) = ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) )
182 179 181 oveq12d 
 |-  ( i = 0 -> ( ( i .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) = ( ( 0 .^ X ) .x. ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
183 182 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 ) ) ) ) )
184 27 58 142 178 183 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 ) ) ) ) )
185 95 149 7 mulg0 
 |-  ( X e. ( Base ` P ) -> ( 0 .^ X ) = ( 1r ` P ) )
186 107 185 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( 0 .^ X ) = ( 1r ` P ) )
187 186 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0 .^ X ) = ( 1r ` P ) )
188 187 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 ) ) ) ) )
189 184 188 176 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 ) ) ) )
190 189 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 ) ) ) ) )
191 140 190 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 ) ) ) ) )
192 86 191 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 ) ) ) ) ) )
193 fzfid 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0 ... ( s - 1 ) ) e. Fin )
194 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 )
195 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 )
196 42 adantl 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> b : ( 0 ... s ) --> B )
197 196 adantr 
 |-  ( ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> b : ( 0 ... s ) --> B )
198 nnz 
 |-  ( s e. NN -> s e. ZZ )
199 fzoval 
 |-  ( s e. ZZ -> ( 0 ..^ s ) = ( 0 ... ( s - 1 ) ) )
200 198 199 syl 
 |-  ( s e. NN -> ( 0 ..^ s ) = ( 0 ... ( s - 1 ) ) )
201 200 eqcomd 
 |-  ( s e. NN -> ( 0 ... ( s - 1 ) ) = ( 0 ..^ s ) )
202 201 eleq2d 
 |-  ( s e. NN -> ( i e. ( 0 ... ( s - 1 ) ) <-> i e. ( 0 ..^ s ) ) )
203 elfzofz 
 |-  ( i e. ( 0 ..^ s ) -> i e. ( 0 ... s ) )
204 202 203 biimtrdi 
 |-  ( s e. NN -> ( i e. ( 0 ... ( s - 1 ) ) -> i e. ( 0 ... s ) ) )
205 204 adantr 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( i e. ( 0 ... ( s - 1 ) ) -> i e. ( 0 ... s ) ) )
206 205 imp 
 |-  ( ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> i e. ( 0 ... s ) )
207 197 206 ffvelcdmd 
 |-  ( ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ i e. ( 0 ... ( s - 1 ) ) ) -> ( b ` i ) e. B )
208 207 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 )
209 elfznn0 
 |-  ( i e. ( 0 ... ( s - 1 ) ) -> i e. NN0 )
210 209 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 )
211 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 )
212 210 211 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 )
213 194 195 208 212 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 ) )
214 213 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 ) )
215 27 35 193 214 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 ) )
216 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 ) ) ) ) ) ) )
217 35 215 71 216 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 ) ) ) ) ) ) )
218 217 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 ) ) ) ) ) )
219 ringgrp 
 |-  ( Y e. Ring -> Y e. Grp )
220 32 219 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Grp )
221 220 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Grp )
222 fzfid 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 1 ... s ) e. Fin )
223 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 )
224 101 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 )
225 elfznn 
 |-  ( i e. ( 1 ... s ) -> i e. NN )
226 225 nnnn0d 
 |-  ( i e. ( 1 ... s ) -> i e. NN0 )
227 226 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 )
228 108 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 ) )
229 95 7 224 227 228 mulgnn0cld 
 |-  ( ( ( ( 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 ) )
230 115 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Base ` P ) = ( Base ` ( Scalar ` Y ) ) )
231 230 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 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 ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( Base ` P ) = ( Base ` ( Scalar ` Y ) ) )
233 229 232 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 ) ) )
234 122 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 )
235 157 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 ) )
236 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 )
237 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 )
238 196 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> b : ( 0 ... s ) --> B )
239 238 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 )
240 1eluzge0 
 |-  1 e. ( ZZ>= ` 0 )
241 fzss1 
 |-  ( 1 e. ( ZZ>= ` 0 ) -> ( 1 ... s ) C_ ( 0 ... s ) )
242 240 241 mp1i 
 |-  ( s e. NN -> ( 1 ... s ) C_ ( 0 ... s ) )
243 242 sseld 
 |-  ( s e. NN -> ( i e. ( 1 ... s ) -> i e. ( 0 ... s ) ) )
244 243 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 ) ) )
245 244 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 ) )
246 239 245 ffvelcdmd 
 |-  ( ( ( ( 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 )
247 5 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` i ) e. B ) -> ( T ` ( b ` i ) ) e. ( Base ` Y ) )
248 236 237 246 247 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 ) )
249 234 235 248 134 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 ) )
250 223 233 249 138 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 ) )
251 250 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 ) )
252 27 35 222 251 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 ) )
253 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 ) ) ) ) ) ) ) ) )
254 221 71 215 252 253 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 ) ) ) ) ) ) ) ) )
255 oveq1 
 |-  ( x = i -> ( x - 1 ) = ( i - 1 ) )
256 255 oveq1d 
 |-  ( x = i -> ( ( x - 1 ) + 1 ) = ( ( i - 1 ) + 1 ) )
257 256 oveq1d 
 |-  ( x = i -> ( ( ( x - 1 ) + 1 ) .^ X ) = ( ( ( i - 1 ) + 1 ) .^ X ) )
258 255 fveq2d 
 |-  ( x = i -> ( b ` ( x - 1 ) ) = ( b ` ( i - 1 ) ) )
259 258 fveq2d 
 |-  ( x = i -> ( T ` ( b ` ( x - 1 ) ) ) = ( T ` ( b ` ( i - 1 ) ) ) )
260 257 259 oveq12d 
 |-  ( x = i -> ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) = ( ( ( ( i - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) )
261 260 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 ) ) ) ) )
262 225 nncnd 
 |-  ( i e. ( 1 ... s ) -> i e. CC )
263 262 adantl 
 |-  ( ( s e. NN /\ i e. ( 1 ... s ) ) -> i e. CC )
264 npcan1 
 |-  ( i e. CC -> ( ( i - 1 ) + 1 ) = i )
265 263 264 syl 
 |-  ( ( s e. NN /\ i e. ( 1 ... s ) ) -> ( ( i - 1 ) + 1 ) = i )
266 265 oveq1d 
 |-  ( ( s e. NN /\ i e. ( 1 ... s ) ) -> ( ( ( i - 1 ) + 1 ) .^ X ) = ( i .^ X ) )
267 266 oveq1d 
 |-  ( ( s e. NN /\ i e. ( 1 ... s ) ) -> ( ( ( ( i - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) = ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) )
268 267 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 ) ) ) ) ) )
269 261 268 eqtrid 
 |-  ( 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 ) ) ) ) ) )
270 269 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 ) ) ) ) ) ) )
271 270 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 ) ) ) ) ) ) )
272 271 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 ) ) ) ) ) ) ) )
273 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
274 1zzd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> 1 e. ZZ )
275 0zd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> 0 e. ZZ )
276 37 nn0zd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( s - 1 ) e. ZZ )
277 oveq1 
 |-  ( i = ( x - 1 ) -> ( i + 1 ) = ( ( x - 1 ) + 1 ) )
278 277 oveq1d 
 |-  ( i = ( x - 1 ) -> ( ( i + 1 ) .^ X ) = ( ( ( x - 1 ) + 1 ) .^ X ) )
279 2fveq3 
 |-  ( i = ( x - 1 ) -> ( T ` ( b ` i ) ) = ( T ` ( b ` ( x - 1 ) ) ) )
280 278 279 oveq12d 
 |-  ( i = ( x - 1 ) -> ( ( ( i + 1 ) .^ X ) .x. ( T ` ( b ` i ) ) ) = ( ( ( ( x - 1 ) + 1 ) .^ X ) .x. ( T ` ( b ` ( x - 1 ) ) ) ) )
281 27 273 35 274 275 276 213 280 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 ) ) ) ) ) ) )
282 0p1e1 
 |-  ( 0 + 1 ) = 1
283 282 a1i 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0 + 1 ) = 1 )
284 76 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( s - 1 ) + 1 ) = s )
285 283 284 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 ) )
286 285 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 ) ) ) ) ) )
287 286 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 ) ) ) ) ) ) )
288 281 287 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 ) ) ) ) ) ) )
289 288 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 ) ) ) ) ) ) ) )
290 ringabl 
 |-  ( Y e. Ring -> Y e. Abel )
291 32 290 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Abel )
292 291 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Abel )
293 225 adantl 
 |-  ( ( s e. NN /\ i e. ( 1 ... s ) ) -> i e. NN )
294 nnz 
 |-  ( i e. NN -> i e. ZZ )
295 elfzm1b 
 |-  ( ( i e. ZZ /\ s e. ZZ ) -> ( i e. ( 1 ... s ) <-> ( i - 1 ) e. ( 0 ... ( s - 1 ) ) ) )
296 294 198 295 syl2an 
 |-  ( ( i e. NN /\ s e. NN ) -> ( i e. ( 1 ... s ) <-> ( i - 1 ) e. ( 0 ... ( s - 1 ) ) ) )
297 200 adantl 
 |-  ( ( i e. NN /\ s e. NN ) -> ( 0 ..^ s ) = ( 0 ... ( s - 1 ) ) )
298 297 eqcomd 
 |-  ( ( i e. NN /\ s e. NN ) -> ( 0 ... ( s - 1 ) ) = ( 0 ..^ s ) )
299 298 eleq2d 
 |-  ( ( i e. NN /\ s e. NN ) -> ( ( i - 1 ) e. ( 0 ... ( s - 1 ) ) <-> ( i - 1 ) e. ( 0 ..^ s ) ) )
300 elfzofz 
 |-  ( ( i - 1 ) e. ( 0 ..^ s ) -> ( i - 1 ) e. ( 0 ... s ) )
301 299 300 biimtrdi 
 |-  ( ( i e. NN /\ s e. NN ) -> ( ( i - 1 ) e. ( 0 ... ( s - 1 ) ) -> ( i - 1 ) e. ( 0 ... s ) ) )
302 296 301 sylbid 
 |-  ( ( i e. NN /\ s e. NN ) -> ( i e. ( 1 ... s ) -> ( i - 1 ) e. ( 0 ... s ) ) )
303 302 expimpd 
 |-  ( i e. NN -> ( ( s e. NN /\ i e. ( 1 ... s ) ) -> ( i - 1 ) e. ( 0 ... s ) ) )
304 293 303 mpcom 
 |-  ( ( s e. NN /\ i e. ( 1 ... s ) ) -> ( i - 1 ) e. ( 0 ... s ) )
305 304 ex 
 |-  ( s e. NN -> ( i e. ( 1 ... s ) -> ( i - 1 ) e. ( 0 ... s ) ) )
306 305 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 ) ) )
307 306 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 ) )
308 239 307 ffvelcdmd 
 |-  ( ( ( ( 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 )
309 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 ) )
310 236 237 308 227 309 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 ) )
311 eqid 
 |-  ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) ) = ( i e. ( 1 ... s ) |-> ( ( i .^ X ) .x. ( T ` ( b ` ( i - 1 ) ) ) ) )
312 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 ) ) ) ) )
313 27 12 292 222 310 250 311 312 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 ) ) ) ) ) ) ) )
314 272 289 313 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 ) ) ) ) ) ) ) )
315 314 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 ) ) ) ) ) ) ) ) )
316 221 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 )
317 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 ) )
318 316 310 250 317 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 ) )
319 318 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 ) )
320 27 35 222 319 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 ) )
321 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 ) ) ) ) )
322 35 71 320 321 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 ) ) ) ) )
323 254 315 322 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 ) ) ) ) )
324 323 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 ) ) ) ) )
325 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 ) )
326 58 71 215 325 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 ) )
327 27 11 12 292 326 252 172 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 ) ) ) ) ) )
328 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 ) ) ) ) ) )
329 221 320 71 172 328 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 ) ) ) ) ) )
330 324 327 329 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 ) ) ) ) ) )
331 5 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` ( i - 1 ) ) e. B ) -> ( T ` ( b ` ( i - 1 ) ) ) e. ( Base ` Y ) )
332 236 237 308 331 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 ) )
333 27 8 136 137 12 223 233 332 249 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 ) ) ) ) ) )
334 333 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 ) ) ) ) ) )
335 334 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 ) ) ) ) ) ) )
336 335 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 ) ) ) ) ) ) ) )
337 336 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 ) ) ) ) ) )
338 218 330 337 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 ) ) ) ) ) )
339 18 192 338 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 ) ) ) ) ) )