MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cpmadugsumlemF Structured version   Unicode version

Theorem cpmadugsumlemF 19898
Description: Lemma F for cpmadugsum 19900. (Contributed by AV, 7-Nov-2019.)
Hypotheses
Ref Expression
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
Ref Expression
cpmadugsumlemF  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( ( X  .x.  .1.  )  .X.  ( Y  gsumg  ( i  e.  ( 0 ... s ) 
|->  ( ( i  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) ) )  .-  ( ( T `  M )  .X.  ( Y  gsumg  ( i  e.  ( 0 ... s ) 
|->  ( ( i  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) ) ) )  =  ( ( Y 
gsumg  ( 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
) ) ) ) ) )
Distinct variable groups:    B, i    i, M    i, N    R, i    i, X    i, Y    .X. , i    .x. , i    .1. , i    i, b    i, s    T, i   
.^ , i    .- , i
Allowed substitution hints:    A( i, s, b)    B( s, b)    P( i, s, b)    .+ ( i, s, b)    R( s, b)    T( s, b)    .x. ( s, b)    .X. ( s, b)    .1. ( s,
b)    .^ ( s, b)    M( s, b)    .- ( s, b)    N( s, b)    X( s, b)    Y( s, b)

Proof of Theorem cpmadugsumlemF
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 nnnn0 10883 . . . 4  |-  ( s  e.  NN  ->  s  e.  NN0 )
2 cpmadugsum.a . . . . 5  |-  A  =  ( N Mat  R )
3 cpmadugsum.b . . . . 5  |-  B  =  ( Base `  A
)
4 cpmadugsum.p . . . . 5  |-  P  =  (Poly1 `  R )
5 cpmadugsum.y . . . . 5  |-  Y  =  ( N Mat  P )
6 cpmadugsum.t . . . . 5  |-  T  =  ( N matToPolyMat  R )
7 cpmadugsum.x . . . . 5  |-  X  =  (var1 `  R )
8 cpmadugsum.e . . . . 5  |-  .^  =  (.g
`  (mulGrp `  P )
)
9 cpmadugsum.m . . . . 5  |-  .x.  =  ( .s `  Y )
10 cpmadugsum.r . . . . 5  |-  .X.  =  ( .r `  Y )
11 cpmadugsum.1 . . . . 5  |-  .1.  =  ( 1r `  Y )
122, 3, 4, 5, 6, 7, 8, 9, 10, 11cpmadugsumlemB 19896 . . . 4  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN0  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( X 
.x.  .1.  )  .X.  ( Y  gsumg  ( i  e.  ( 0 ... s ) 
|->  ( ( i  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) ) )  =  ( Y  gsumg  ( i  e.  ( 0 ... s ) 
|->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) ) )
131, 12sylanr1 656 . . 3  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( X 
.x.  .1.  )  .X.  ( Y  gsumg  ( i  e.  ( 0 ... s ) 
|->  ( ( i  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) ) )  =  ( Y  gsumg  ( i  e.  ( 0 ... s ) 
|->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) ) )
142, 3, 4, 5, 6, 7, 8, 9, 10, 11cpmadugsumlemC 19897 . . . 4  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN0  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( T `
 M )  .X.  ( Y  gsumg  ( i  e.  ( 0 ... s ) 
|->  ( ( i  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) ) )  =  ( Y  gsumg  ( i  e.  ( 0 ... s ) 
|->  ( ( i  .^  X )  .x.  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) ) )
151, 14sylanr1 656 . . 3  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( T `
 M )  .X.  ( Y  gsumg  ( i  e.  ( 0 ... s ) 
|->  ( ( i  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) ) )  =  ( Y  gsumg  ( i  e.  ( 0 ... s ) 
|->  ( ( i  .^  X )  .x.  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) ) )
1613, 15oveq12d 6323 . 2  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( ( X  .x.  .1.  )  .X.  ( Y  gsumg  ( i  e.  ( 0 ... s ) 
|->  ( ( i  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) ) )  .-  ( ( T `  M )  .X.  ( Y  gsumg  ( i  e.  ( 0 ... s ) 
|->  ( ( i  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) ) ) )  =  ( ( Y 
gsumg  ( i  e.  ( 0 ... s ) 
|->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) )  .-  ( Y  gsumg  ( i  e.  ( 0 ... s ) 
|->  ( ( i  .^  X )  .x.  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) ) ) )
17 nncn 10624 . . . . . . . . 9  |-  ( s  e.  NN  ->  s  e.  CC )
18 npcan1 10051 . . . . . . . . . 10  |-  ( s  e.  CC  ->  (
( s  -  1 )  +  1 )  =  s )
1918eqcomd 2430 . . . . . . . . 9  |-  ( s  e.  CC  ->  s  =  ( ( s  -  1 )  +  1 ) )
2017, 19syl 17 . . . . . . . 8  |-  ( s  e.  NN  ->  s  =  ( ( s  -  1 )  +  1 ) )
2120oveq2d 6321 . . . . . . 7  |-  ( s  e.  NN  ->  (
0 ... s )  =  ( 0 ... (
( s  -  1 )  +  1 ) ) )
2221mpteq1d 4505 . . . . . 6  |-  ( 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 ) ) ) ) )
2322oveq2d 6321 . . . . 5  |-  ( s  e.  NN  ->  ( Y  gsumg  ( i  e.  ( 0 ... s ) 
|->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) )  =  ( Y  gsumg  ( i  e.  ( 0 ... ( ( s  -  1 )  +  1 ) ) 
|->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) ) )
2423ad2antrl 732 . . . 4  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( i  e.  ( 0 ... s )  |->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  (
b `  i )
) ) ) )  =  ( Y  gsumg  ( i  e.  ( 0 ... ( ( s  - 
1 )  +  1 ) )  |->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  (
b `  i )
) ) ) ) )
25 eqid 2422 . . . . 5  |-  ( Base `  Y )  =  (
Base `  Y )
26 cpmadugsum.g . . . . 5  |-  .+  =  ( +g  `  Y )
27 crngring 17790 . . . . . . . . . 10  |-  ( R  e.  CRing  ->  R  e.  Ring )
2827anim2i 571 . . . . . . . . 9  |-  ( ( N  e.  Fin  /\  R  e.  CRing )  -> 
( N  e.  Fin  /\  R  e.  Ring )
)
29283adant3 1025 . . . . . . . 8  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  ( N  e.  Fin  /\  R  e.  Ring ) )
304, 5pmatring 19715 . . . . . . . 8  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  Y  e.  Ring )
3129, 30syl 17 . . . . . . 7  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  Y  e.  Ring )
32 ringcmn 17810 . . . . . . 7  |-  ( Y  e.  Ring  ->  Y  e. CMnd
)
3331, 32syl 17 . . . . . 6  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  Y  e. CMnd )
3433adantr 466 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  Y  e. CMnd )
35 nnm1nn0 10918 . . . . . 6  |-  ( s  e.  NN  ->  (
s  -  1 )  e.  NN0 )
3635ad2antrl 732 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( s  - 
1 )  e.  NN0 )
37 simpll1 1044 . . . . . 6  |-  ( ( ( ( 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 )
38273ad2ant2 1027 . . . . . . . 8  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  R  e.  Ring )
3938adantr 466 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  R  e.  Ring )
4039adantr 466 . . . . . 6  |-  ( ( ( ( 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 )
41 elmapi 7504 . . . . . . . . . 10  |-  ( b  e.  ( B  ^m  ( 0 ... s
) )  ->  b : ( 0 ... s ) --> B )
4221feq2d 5733 . . . . . . . . . 10  |-  ( s  e.  NN  ->  (
b : ( 0 ... s ) --> B  <-> 
b : ( 0 ... ( ( s  -  1 )  +  1 ) ) --> B ) )
4341, 42syl5ibcom 223 . . . . . . . . 9  |-  ( b  e.  ( B  ^m  ( 0 ... s
) )  ->  (
s  e.  NN  ->  b : ( 0 ... ( ( s  - 
1 )  +  1 ) ) --> B ) )
4443impcom 431 . . . . . . . 8  |-  ( ( s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) )  -> 
b : ( 0 ... ( ( s  -  1 )  +  1 ) ) --> B )
4544adantl 467 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  b : ( 0 ... ( ( s  -  1 )  +  1 ) ) --> B )
4645ffvelrnda 6037 . . . . . 6  |-  ( ( ( ( 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 )
47 elfznn0 11894 . . . . . . . 8  |-  ( i  e.  ( 0 ... ( ( s  - 
1 )  +  1 ) )  ->  i  e.  NN0 )
4847adantl 467 . . . . . . 7  |-  ( ( ( ( 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 )
49 1nn0 10892 . . . . . . . 8  |-  1  e.  NN0
5049a1i 11 . . . . . . 7  |-  ( ( ( ( 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 )
5148, 50nn0addcld 10936 . . . . . 6  |-  ( ( ( ( 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 )
522, 3, 6, 4, 5, 25, 9, 8, 7mat2pmatscmxcl 19762 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( ( b `  i )  e.  B  /\  ( i  +  1 )  e.  NN0 )
)  ->  ( (
( i  +  1 )  .^  X )  .x.  ( T `  (
b `  i )
) )  e.  (
Base `  Y )
)
5337, 40, 46, 51, 52syl22anc 1265 . . . . 5  |-  ( ( ( ( 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
) )
5425, 26, 34, 36, 53gsummptfzsplit 17564 . . . 4  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( i  e.  ( 0 ... ( ( s  - 
1 )  +  1 ) )  |->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  (
b `  i )
) ) ) )  =  ( ( Y 
gsumg  ( i  e.  ( 0 ... ( s  -  1 ) ) 
|->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) )  .+  ( Y  gsumg  ( i  e.  {
( ( s  - 
1 )  +  1 ) }  |->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  (
b `  i )
) ) ) ) ) )
55 ringmnd 17788 . . . . . . . 8  |-  ( Y  e.  Ring  ->  Y  e. 
Mnd )
5631, 55syl 17 . . . . . . 7  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  Y  e.  Mnd )
5756adantr 466 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  Y  e.  Mnd )
58 ovex 6333 . . . . . . 7  |-  ( ( s  -  1 )  +  1 )  e. 
_V
5958a1i 11 . . . . . 6  |-  ( ( ( 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 1008 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  N  e.  Fin )
61 nn0fz0 11897 . . . . . . . . . . 11  |-  ( s  e.  NN0  <->  s  e.  ( 0 ... s ) )
621, 61sylib 199 . . . . . . . . . 10  |-  ( s  e.  NN  ->  s  e.  ( 0 ... s
) )
63 ffvelrn 6035 . . . . . . . . . 10  |-  ( ( b : ( 0 ... s ) --> B  /\  s  e.  ( 0 ... s ) )  ->  ( b `  s )  e.  B
)
6441, 62, 63syl2anr 480 . . . . . . . . 9  |-  ( ( s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) )  -> 
( b `  s
)  e.  B )
651adantr 466 . . . . . . . . . 10  |-  ( ( s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) )  -> 
s  e.  NN0 )
6649a1i 11 . . . . . . . . . 10  |-  ( ( s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) )  -> 
1  e.  NN0 )
6765, 66nn0addcld 10936 . . . . . . . . 9  |-  ( ( s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) )  -> 
( s  +  1 )  e.  NN0 )
6864, 67jca 534 . . . . . . . 8  |-  ( ( s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) )  -> 
( ( b `  s )  e.  B  /\  ( s  +  1 )  e.  NN0 )
)
6968adantl 467 . . . . . . 7  |-  ( ( ( 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 ) )
702, 3, 6, 4, 5, 25, 9, 8, 7mat2pmatscmxcl 19762 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( ( b `  s )  e.  B  /\  ( s  +  1 )  e.  NN0 )
)  ->  ( (
( s  +  1 )  .^  X )  .x.  ( T `  (
b `  s )
) )  e.  (
Base `  Y )
)
7160, 39, 69, 70syl21anc 1263 . . . . . 6  |-  ( ( ( 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 6312 . . . . . . . . 9  |-  ( i  =  ( ( s  -  1 )  +  1 )  ->  (
i  +  1 )  =  ( ( ( s  -  1 )  +  1 )  +  1 ) )
7372oveq1d 6320 . . . . . . . 8  |-  ( i  =  ( ( s  -  1 )  +  1 )  ->  (
( i  +  1 )  .^  X )  =  ( ( ( ( s  -  1 )  +  1 )  +  1 )  .^  X ) )
74 fveq2 5881 . . . . . . . . 9  |-  ( i  =  ( ( s  -  1 )  +  1 )  ->  (
b `  i )  =  ( b `  ( ( s  - 
1 )  +  1 ) ) )
7574fveq2d 5885 . . . . . . . 8  |-  ( i  =  ( ( s  -  1 )  +  1 )  ->  ( T `  ( b `  i ) )  =  ( T `  (
b `  ( (
s  -  1 )  +  1 ) ) ) )
7673, 75oveq12d 6323 . . . . . . 7  |-  ( i  =  ( ( s  -  1 )  +  1 )  ->  (
( ( i  +  1 )  .^  X
)  .x.  ( T `  ( b `  i
) ) )  =  ( ( ( ( ( s  -  1 )  +  1 )  +  1 )  .^  X )  .x.  ( T `  ( b `  ( ( s  - 
1 )  +  1 ) ) ) ) )
7717, 18syl 17 . . . . . . . . . . 11  |-  ( s  e.  NN  ->  (
( s  -  1 )  +  1 )  =  s )
7877oveq1d 6320 . . . . . . . . . 10  |-  ( s  e.  NN  ->  (
( ( s  - 
1 )  +  1 )  +  1 )  =  ( s  +  1 ) )
7978oveq1d 6320 . . . . . . . . 9  |-  ( s  e.  NN  ->  (
( ( ( s  -  1 )  +  1 )  +  1 )  .^  X )  =  ( ( s  +  1 )  .^  X ) )
8077fveq2d 5885 . . . . . . . . . 10  |-  ( s  e.  NN  ->  (
b `  ( (
s  -  1 )  +  1 ) )  =  ( b `  s ) )
8180fveq2d 5885 . . . . . . . . 9  |-  ( s  e.  NN  ->  ( T `  ( b `  ( ( s  - 
1 )  +  1 ) ) )  =  ( T `  (
b `  s )
) )
8279, 81oveq12d 6323 . . . . . . . 8  |-  ( s  e.  NN  ->  (
( ( ( ( s  -  1 )  +  1 )  +  1 )  .^  X
)  .x.  ( T `  ( b `  (
( s  -  1 )  +  1 ) ) ) )  =  ( ( ( s  +  1 )  .^  X )  .x.  ( T `  ( b `  s ) ) ) )
8382ad2antrl 732 . . . . . . 7  |-  ( ( ( 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 )
) ) )
8476, 83sylan9eqr 2485 . . . . . 6  |-  ( ( ( ( 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 ) ) ) )
8525, 57, 59, 71, 84gsumsnd 17584 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( i  e.  { ( ( s  -  1 )  +  1 ) } 
|->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) )  =  ( ( ( s  +  1 )  .^  X
)  .x.  ( T `  ( b `  s
) ) ) )
8685oveq2d 6321 . . . 4  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( Y 
gsumg  ( i  e.  ( 0 ... ( s  -  1 ) ) 
|->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) )  .+  ( Y  gsumg  ( i  e.  {
( ( s  - 
1 )  +  1 ) }  |->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  (
b `  i )
) ) ) ) )  =  ( ( Y  gsumg  ( i  e.  ( 0 ... ( s  -  1 ) ) 
|->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) )  .+  (
( ( s  +  1 )  .^  X
)  .x.  ( T `  ( b `  s
) ) ) ) )
8724, 54, 863eqtrd 2467 . . 3  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( i  e.  ( 0 ... s )  |->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  (
b `  i )
) ) ) )  =  ( ( Y 
gsumg  ( i  e.  ( 0 ... ( s  -  1 ) ) 
|->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) )  .+  (
( ( s  +  1 )  .^  X
)  .x.  ( T `  ( b `  s
) ) ) ) )
881ad2antrl 732 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  s  e.  NN0 )
894, 5pmatlmod 19716 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  Y  e.  LMod )
9028, 89syl 17 . . . . . . . . 9  |-  ( ( N  e.  Fin  /\  R  e.  CRing )  ->  Y  e.  LMod )
91903adant3 1025 . . . . . . . 8  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  Y  e.  LMod )
9291adantr 466 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  Y  e.  LMod )
9392adantr 466 . . . . . 6  |-  ( ( ( ( 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 )
944ply1ring 18840 . . . . . . . . . . . . 13  |-  ( R  e.  Ring  ->  P  e. 
Ring )
9527, 94syl 17 . . . . . . . . . . . 12  |-  ( R  e.  CRing  ->  P  e.  Ring )
96953ad2ant2 1027 . . . . . . . . . . 11  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  P  e.  Ring )
97 eqid 2422 . . . . . . . . . . . 12  |-  (mulGrp `  P )  =  (mulGrp `  P )
9897ringmgp 17785 . . . . . . . . . . 11  |-  ( P  e.  Ring  ->  (mulGrp `  P )  e.  Mnd )
9996, 98syl 17 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  (mulGrp `  P )  e.  Mnd )
10099adantr 466 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  (mulGrp `  P )  e.  Mnd )
101100adantr 466 . . . . . . . 8  |-  ( ( ( ( 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 )
102 elfznn0 11894 . . . . . . . . 9  |-  ( i  e.  ( 0 ... s )  ->  i  e.  NN0 )
103102adantl 467 . . . . . . . 8  |-  ( ( ( ( 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 )
104 eqid 2422 . . . . . . . . . . . . 13  |-  ( Base `  P )  =  (
Base `  P )
1057, 4, 104vr1cl 18809 . . . . . . . . . . . 12  |-  ( R  e.  Ring  ->  X  e.  ( Base `  P
) )
10627, 105syl 17 . . . . . . . . . . 11  |-  ( R  e.  CRing  ->  X  e.  ( Base `  P )
)
1071063ad2ant2 1027 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  X  e.  ( Base `  P
) )
108107adantr 466 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  X  e.  (
Base `  P )
)
109108adantr 466 . . . . . . . 8  |-  ( ( ( ( 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
) )
11097, 104mgpbas 17728 . . . . . . . . 9  |-  ( Base `  P )  =  (
Base `  (mulGrp `  P
) )
111110, 8mulgnn0cl 16773 . . . . . . . 8  |-  ( ( (mulGrp `  P )  e.  Mnd  /\  i  e. 
NN0  /\  X  e.  ( Base `  P )
)  ->  ( i  .^  X )  e.  (
Base `  P )
)
112101, 103, 109, 111syl3anc 1264 . . . . . . 7  |-  ( ( ( ( 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
) )
1134ply1crng 18790 . . . . . . . . . . . . . . 15  |-  ( R  e.  CRing  ->  P  e.  CRing
)
114113anim2i 571 . . . . . . . . . . . . . 14  |-  ( ( N  e.  Fin  /\  R  e.  CRing )  -> 
( N  e.  Fin  /\  P  e.  CRing ) )
1151143adant3 1025 . . . . . . . . . . . . 13  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  ( N  e.  Fin  /\  P  e.  CRing ) )
1165matsca2 19443 . . . . . . . . . . . . 13  |-  ( ( N  e.  Fin  /\  P  e.  CRing )  ->  P  =  (Scalar `  Y
) )
117115, 116syl 17 . . . . . . . . . . . 12  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  P  =  (Scalar `  Y )
)
118117eqcomd 2430 . . . . . . . . . . 11  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  (Scalar `  Y )  =  P )
119118fveq2d 5885 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  ( Base `  (Scalar `  Y
) )  =  (
Base `  P )
)
120119eleq2d 2492 . . . . . . . . 9  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  (
( i  .^  X
)  e.  ( Base `  (Scalar `  Y )
)  <->  ( i  .^  X )  e.  (
Base `  P )
) )
121120adantr 466 . . . . . . . 8  |-  ( ( ( 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 )
) )
122121adantr 466 . . . . . . 7  |-  ( ( ( ( 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 )
) )
123112, 122mpbird 235 . . . . . 6  |-  ( ( ( ( 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 ) ) )
12431adantr 466 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  Y  e.  Ring )
125124adantr 466 . . . . . . 7  |-  ( ( ( ( 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 )
126 simpll1 1044 . . . . . . . 8  |-  ( ( ( ( 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 )
12739adantr 466 . . . . . . . 8  |-  ( ( ( ( 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 )
128 simpll3 1046 . . . . . . . 8  |-  ( ( ( ( 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 )
1296, 2, 3, 4, 5mat2pmatbas 19748 . . . . . . . 8  |-  ( ( N  e.  Fin  /\  R  e.  Ring  /\  M  e.  B )  ->  ( T `  M )  e.  ( Base `  Y
) )
130126, 127, 128, 129syl3anc 1264 . . . . . . 7  |-  ( ( ( ( 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
) )
13188adantr 466 . . . . . . . 8  |-  ( ( ( ( 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 )
132 simprr 764 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  b  e.  ( B  ^m  ( 0 ... s ) ) )
133132anim1i 570 . . . . . . . 8  |-  ( ( ( ( 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 ) ) )
1342, 3, 4, 5, 6m2pmfzmap 19769 . . . . . . . 8  |-  ( ( ( 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 )
)
135126, 127, 131, 133, 134syl31anc 1267 . . . . . . 7  |-  ( ( ( ( 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
) )
13625, 10ringcl 17793 . . . . . . 7  |-  ( ( Y  e.  Ring  /\  ( T `  M )  e.  ( Base `  Y
)  /\  ( T `  ( b `  i
) )  e.  (
Base `  Y )
)  ->  ( ( T `  M )  .X.  ( T `  (
b `  i )
) )  e.  (
Base `  Y )
)
137125, 130, 135, 136syl3anc 1264 . . . . . 6  |-  ( ( ( ( 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
) )
138 eqid 2422 . . . . . . 7  |-  (Scalar `  Y )  =  (Scalar `  Y )
139 eqid 2422 . . . . . . 7  |-  ( Base `  (Scalar `  Y )
)  =  ( Base `  (Scalar `  Y )
)
14025, 138, 9, 139lmodvscl 18107 . . . . . 6  |-  ( ( 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
) )
14193, 123, 137, 140syl3anc 1264 . . . . 5  |-  ( ( ( ( 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
) )
14225, 26, 34, 88, 141gsummptfzsplitl 17565 . . . 4  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( i  e.  ( 0 ... s )  |->  ( ( i  .^  X )  .x.  ( ( T `  M )  .X.  ( T `  ( b `  i ) ) ) ) ) )  =  ( ( Y  gsumg  ( i  e.  ( 1 ... s )  |->  ( ( i  .^  X )  .x.  ( ( T `  M )  .X.  ( T `  ( b `  i ) ) ) ) ) )  .+  ( Y  gsumg  ( i  e.  {
0 }  |->  ( ( i  .^  X )  .x.  ( ( T `  M )  .X.  ( T `  ( b `  i ) ) ) ) ) ) ) )
143 0nn0 10891 . . . . . . . 8  |-  0  e.  NN0
144143a1i 11 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  0  e.  NN0 )
145 eqid 2422 . . . . . . . . . . . . 13  |-  ( 0g
`  (mulGrp `  P )
)  =  ( 0g
`  (mulGrp `  P )
)
146110, 145, 8mulg0 16762 . . . . . . . . . . . 12  |-  ( X  e.  ( Base `  P
)  ->  ( 0 
.^  X )  =  ( 0g `  (mulGrp `  P ) ) )
147107, 146syl 17 . . . . . . . . . . 11  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  (
0  .^  X )  =  ( 0g `  (mulGrp `  P ) ) )
148147adantr 466 . . . . . . . . . 10  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( 0  .^  X )  =  ( 0g `  (mulGrp `  P ) ) )
149148oveq1d 6320 . . . . . . . . 9  |-  ( ( ( 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 ) ) ) ) )
150 eqid 2422 . . . . . . . . . . . . 13  |-  ( 1r
`  P )  =  ( 1r `  P
)
15197, 150ringidval 17736 . . . . . . . . . . . 12  |-  ( 1r
`  P )  =  ( 0g `  (mulGrp `  P ) )
152151a1i 11 . . . . . . . . . . 11  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( 1r `  P )  =  ( 0g `  (mulGrp `  P ) ) )
153152eqcomd 2430 . . . . . . . . . 10  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( 0g `  (mulGrp `  P ) )  =  ( 1r `  P ) )
154153oveq1d 6320 . . . . . . . . 9  |-  ( ( ( 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
) ) ) ) )
155117adantr 466 . . . . . . . . . . . 12  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  P  =  (Scalar `  Y ) )
156155fveq2d 5885 . . . . . . . . . . 11  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( 1r `  P )  =  ( 1r `  (Scalar `  Y ) ) )
157156oveq1d 6320 . . . . . . . . . 10  |-  ( ( ( 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 ) ) ) ) )
15827, 129syl3an2 1298 . . . . . . . . . . . . 13  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  ( T `  M )  e.  ( Base `  Y
) )
159158adantr 466 . . . . . . . . . . . 12  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( T `  M )  e.  (
Base `  Y )
)
160 simpl 458 . . . . . . . . . . . . . . . . . 18  |-  ( ( b : ( 0 ... s ) --> B  /\  s  e.  NN )  ->  b : ( 0 ... s ) --> B )
161 elnn0uz 11203 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  e.  NN0  <->  s  e.  (
ZZ>= `  0 ) )
1621, 161sylib 199 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  e.  NN  ->  s  e.  ( ZZ>= `  0 )
)
163 eluzfz1 11813 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... s
) )
164162, 163syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( s  e.  NN  ->  0  e.  ( 0 ... s
) )
165164adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( b : ( 0 ... s ) --> B  /\  s  e.  NN )  ->  0  e.  ( 0 ... s ) )
166160, 165ffvelrnd 6038 . . . . . . . . . . . . . . . . 17  |-  ( ( b : ( 0 ... s ) --> B  /\  s  e.  NN )  ->  ( b ` 
0 )  e.  B
)
167166ex 435 . . . . . . . . . . . . . . . 16  |-  ( b : ( 0 ... s ) --> B  -> 
( s  e.  NN  ->  ( b `  0
)  e.  B ) )
16841, 167syl 17 . . . . . . . . . . . . . . 15  |-  ( b  e.  ( B  ^m  ( 0 ... s
) )  ->  (
s  e.  NN  ->  ( b `  0 )  e.  B ) )
169168impcom 431 . . . . . . . . . . . . . 14  |-  ( ( s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) )  -> 
( b `  0
)  e.  B )
170169adantl 467 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( b ` 
0 )  e.  B
)
1716, 2, 3, 4, 5mat2pmatbas 19748 . . . . . . . . . . . . 13  |-  ( ( N  e.  Fin  /\  R  e.  Ring  /\  (
b `  0 )  e.  B )  ->  ( T `  ( b `  0 ) )  e.  ( Base `  Y
) )
17260, 39, 170, 171syl3anc 1264 . . . . . . . . . . . 12  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( T `  ( b `  0
) )  e.  (
Base `  Y )
)
17325, 10ringcl 17793 . . . . . . . . . . . 12  |-  ( ( Y  e.  Ring  /\  ( T `  M )  e.  ( Base `  Y
)  /\  ( T `  ( b `  0
) )  e.  (
Base `  Y )
)  ->  ( ( T `  M )  .X.  ( T `  (
b `  0 )
) )  e.  (
Base `  Y )
)
174124, 159, 172, 173syl3anc 1264 . . . . . . . . . . 11  |-  ( ( ( 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 ) )
175 eqid 2422 . . . . . . . . . . . 12  |-  ( 1r
`  (Scalar `  Y )
)  =  ( 1r
`  (Scalar `  Y )
)
17625, 138, 9, 175lmodvs1 18118 . . . . . . . . . . 11  |-  ( ( 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
) ) ) )
17792, 174, 176syl2anc 665 . . . . . . . . . 10  |-  ( ( ( 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 ) ) ) )
178157, 177eqtrd 2463 . . . . . . . . 9  |-  ( ( ( 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
) ) ) )
179149, 154, 1783eqtrd 2467 . . . . . . . 8  |-  ( ( ( 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
) ) ) )
180179, 174eqeltrd 2507 . . . . . . 7  |-  ( ( ( 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 )
)
181 oveq1 6312 . . . . . . . . 9  |-  ( i  =  0  ->  (
i  .^  X )  =  ( 0  .^  X ) )
182 fveq2 5881 . . . . . . . . . . 11  |-  ( i  =  0  ->  (
b `  i )  =  ( b ` 
0 ) )
183182fveq2d 5885 . . . . . . . . . 10  |-  ( i  =  0  ->  ( T `  ( b `  i ) )  =  ( T `  (
b `  0 )
) )
184183oveq2d 6321 . . . . . . . . 9  |-  ( i  =  0  ->  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) )  =  ( ( T `  M )  .X.  ( T `  ( b `  0 ) ) ) )
185181, 184oveq12d 6323 . . . . . . . 8  |-  ( i  =  0  ->  (
( i  .^  X
)  .x.  ( ( T `  M )  .X.  ( T `  (
b `  i )
) ) )  =  ( ( 0  .^  X )  .x.  (
( T `  M
)  .X.  ( T `  ( b `  0
) ) ) ) )
186185adantl 467 . . . . . . 7  |-  ( ( ( ( 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 ) ) ) ) )
18725, 57, 144, 180, 186gsumsnd 17584 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( i  e.  { 0 } 
|->  ( ( i  .^  X )  .x.  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) )  =  ( ( 0  .^  X
)  .x.  ( ( T `  M )  .X.  ( T `  (
b `  0 )
) ) ) )
188110, 151, 8mulg0 16762 . . . . . . . . 9  |-  ( X  e.  ( Base `  P
)  ->  ( 0 
.^  X )  =  ( 1r `  P
) )
189107, 188syl 17 . . . . . . . 8  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  (
0  .^  X )  =  ( 1r `  P ) )
190189adantr 466 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( 0  .^  X )  =  ( 1r `  P ) )
191190oveq1d 6320 . . . . . 6  |-  ( ( ( 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 )
) ) ) )
192187, 191, 1783eqtrd 2467 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( i  e.  { 0 } 
|->  ( ( i  .^  X )  .x.  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) )  =  ( ( T `  M
)  .X.  ( T `  ( b `  0
) ) ) )
193192oveq2d 6321 . . . 4  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( Y 
gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  X )  .x.  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) )  .+  ( Y  gsumg  ( i  e.  {
0 }  |->  ( ( i  .^  X )  .x.  ( ( T `  M )  .X.  ( T `  ( b `  i ) ) ) ) ) ) )  =  ( ( Y 
gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  X )  .x.  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) )  .+  (
( T `  M
)  .X.  ( T `  ( b `  0
) ) ) ) )
194142, 193eqtrd 2463 . . 3  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( i  e.  ( 0 ... s )  |->  ( ( i  .^  X )  .x.  ( ( T `  M )  .X.  ( T `  ( b `  i ) ) ) ) ) )  =  ( ( Y  gsumg  ( i  e.  ( 1 ... s )  |->  ( ( i  .^  X )  .x.  ( ( T `  M )  .X.  ( T `  ( b `  i ) ) ) ) ) )  .+  ( ( T `  M )  .X.  ( T `  ( b `  0 ) ) ) ) )
19587, 194oveq12d 6323 . 2  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( Y 
gsumg  ( i  e.  ( 0 ... s ) 
|->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) )  .-  ( Y  gsumg  ( i  e.  ( 0 ... s ) 
|->  ( ( i  .^  X )  .x.  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) ) )  =  ( ( ( Y 
gsumg  ( i  e.  ( 0 ... ( s  -  1 ) ) 
|->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) )  .+  (
( ( s  +  1 )  .^  X
)  .x.  ( T `  ( b `  s
) ) ) ) 
.-  ( ( Y 
gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  X )  .x.  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) )  .+  (
( T `  M
)  .X.  ( T `  ( b `  0
) ) ) ) ) )
196 fzfid 12192 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( 0 ... ( s  -  1 ) )  e.  Fin )
197 simpll1 1044 . . . . . . . 8  |-  ( ( ( ( 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 )
19839adantr 466 . . . . . . . 8  |-  ( ( ( ( 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 )
19941adantl 467 . . . . . . . . . . 11  |-  ( ( s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) )  -> 
b : ( 0 ... s ) --> B )
200199adantr 466 . . . . . . . . . 10  |-  ( ( ( s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s ) ) )  /\  i  e.  ( 0 ... ( s  -  1 ) ) )  ->  b :
( 0 ... s
) --> B )
201 nnz 10966 . . . . . . . . . . . . . . . 16  |-  ( s  e.  NN  ->  s  e.  ZZ )
202 fzoval 11928 . . . . . . . . . . . . . . . 16  |-  ( s  e.  ZZ  ->  (
0..^ s )  =  ( 0 ... (
s  -  1 ) ) )
203201, 202syl 17 . . . . . . . . . . . . . . 15  |-  ( s  e.  NN  ->  (
0..^ s )  =  ( 0 ... (
s  -  1 ) ) )
204203eqcomd 2430 . . . . . . . . . . . . . 14  |-  ( s  e.  NN  ->  (
0 ... ( s  - 
1 ) )  =  ( 0..^ s ) )
205204eleq2d 2492 . . . . . . . . . . . . 13  |-  ( s  e.  NN  ->  (
i  e.  ( 0 ... ( s  - 
1 ) )  <->  i  e.  ( 0..^ s ) ) )
206 elfzofz 11942 . . . . . . . . . . . . 13  |-  ( i  e.  ( 0..^ s )  ->  i  e.  ( 0 ... s
) )
207205, 206syl6bi 231 . . . . . . . . . . . 12  |-  ( s  e.  NN  ->  (
i  e.  ( 0 ... ( s  - 
1 ) )  -> 
i  e.  ( 0 ... s ) ) )
208207adantr 466 . . . . . . . . . . 11  |-  ( ( s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) )  -> 
( i  e.  ( 0 ... ( s  -  1 ) )  ->  i  e.  ( 0 ... s ) ) )
209208imp 430 . . . . . . . . . 10  |-  ( ( ( s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s ) ) )  /\  i  e.  ( 0 ... ( s  -  1 ) ) )  ->  i  e.  ( 0 ... s
) )
210200, 209ffvelrnd 6038 . . . . . . . . 9  |-  ( ( ( s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s ) ) )  /\  i  e.  ( 0 ... ( s  -  1 ) ) )  ->  ( b `  i )  e.  B
)
211210adantll 718 . . . . . . . 8  |-  ( ( ( ( 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 )
212 elfznn0 11894 . . . . . . . . . 10  |-  ( i  e.  ( 0 ... ( s  -  1 ) )  ->  i  e.  NN0 )
213212adantl 467 . . . . . . . . 9  |-  ( ( ( ( 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 )
21449a1i 11 . . . . . . . . 9  |-  ( ( ( ( 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 )
215213, 214nn0addcld 10936 . . . . . . . 8  |-  ( ( ( ( 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 )
216197, 198, 211, 215, 52syl22anc 1265 . . . . . . 7  |-  ( ( ( ( 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
) )
217216ralrimiva 2836 . . . . . 6  |-  ( ( ( 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
) )
21825, 34, 196, 217gsummptcl 17598 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( i  e.  ( 0 ... ( s  -  1 ) )  |->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  (
b `  i )
) ) ) )  e.  ( Base `  Y
) )
21925, 26cmncom 17445 . . . . 5  |-  ( ( Y  e. CMnd  /\  ( Y  gsumg  ( 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  gsumg  ( 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  gsumg  ( i  e.  ( 0 ... ( s  -  1 ) ) 
|->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) ) ) )
22034, 218, 71, 219syl3anc 1264 . . . 4  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( Y 
gsumg  ( 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  gsumg  ( i  e.  ( 0 ... ( s  -  1 ) ) 
|->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) ) ) )
221220oveq1d 6320 . . 3  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( ( Y  gsumg  ( i  e.  ( 0 ... ( s  -  1 ) ) 
|->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) )  .+  (
( ( s  +  1 )  .^  X
)  .x.  ( T `  ( b `  s
) ) ) ) 
.-  ( ( Y 
gsumg  ( 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  gsumg  ( i  e.  ( 0 ... ( s  -  1 ) )  |->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  (
b `  i )
) ) ) ) )  .-  ( ( Y  gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  X )  .x.  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) )  .+  (
( T `  M
)  .X.  ( T `  ( b `  0
) ) ) ) ) )
222 ringgrp 17784 . . . . . . . . 9  |-  ( Y  e.  Ring  ->  Y  e. 
Grp )
22331, 222syl 17 . . . . . . . 8  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  Y  e.  Grp )
224223adantr 466 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  Y  e.  Grp )
225 fzfid 12192 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( 1 ... s )  e.  Fin )
22692adantr 466 . . . . . . . . . 10  |-  ( ( ( ( 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 )
227100adantr 466 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )
228 elfznn 11835 . . . . . . . . . . . . . 14  |-  ( i  e.  ( 1 ... s )  ->  i  e.  NN )
229228nnnn0d 10932 . . . . . . . . . . . . 13  |-  ( i  e.  ( 1 ... s )  ->  i  e.  NN0 )
230229adantl 467 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )
231108adantr 466 . . . . . . . . . . . 12  |-  ( ( ( ( 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
) )
232227, 230, 231, 111syl3anc 1264 . . . . . . . . . . 11  |-  ( ( ( ( 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
) )
233117fveq2d 5885 . . . . . . . . . . . . 13  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  ( Base `  P )  =  ( Base `  (Scalar `  Y ) ) )
234233adantr 466 . . . . . . . . . . . 12  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Base `  P
)  =  ( Base `  (Scalar `  Y )
) )
235234adantr 466 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) ) )
236232, 235eleqtrd 2509 . . . . . . . . . 10  |-  ( ( ( ( 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 ) ) )
237124adantr 466 . . . . . . . . . . 11  |-  ( ( ( ( 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 )
238159adantr 466 . . . . . . . . . . 11  |-  ( ( ( ( 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
) )
239 simpll1 1044 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )
24039adantr 466 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )
241199adantl 467 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  b : ( 0 ... s ) --> B )
242241adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
243 1eluzge0 11209 . . . . . . . . . . . . . . . . 17  |-  1  e.  ( ZZ>= `  0 )
244 fzss1 11844 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  ( ZZ>= `  0
)  ->  ( 1 ... s )  C_  ( 0 ... s
) )
245243, 244mp1i 13 . . . . . . . . . . . . . . . 16  |-  ( s  e.  NN  ->  (
1 ... s )  C_  ( 0 ... s
) )
246245sseld 3463 . . . . . . . . . . . . . . 15  |-  ( s  e.  NN  ->  (
i  e.  ( 1 ... s )  -> 
i  e.  ( 0 ... s ) ) )
247246ad2antrl 732 . . . . . . . . . . . . . 14  |-  ( ( ( 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
) ) )
248247imp 430 . . . . . . . . . . . . 13  |-  ( ( ( ( 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
) )
249242, 248ffvelrnd 6038 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )
2506, 2, 3, 4, 5mat2pmatbas 19748 . . . . . . . . . . . 12  |-  ( ( N  e.  Fin  /\  R  e.  Ring  /\  (
b `  i )  e.  B )  ->  ( T `  ( b `  i ) )  e.  ( Base `  Y
) )
251239, 240, 249, 250syl3anc 1264 . . . . . . . . . . 11  |-  ( ( ( ( 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
) )
252237, 238, 251, 136syl3anc 1264 . . . . . . . . . 10  |-  ( ( ( ( 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
) )
253226, 236, 252, 140syl3anc 1264 . . . . . . . . 9  |-  ( ( ( ( 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
) )
254253ralrimiva 2836 . . . . . . . 8  |-  ( ( ( 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
) )
25525, 34, 225, 254gsummptcl 17598 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( i  e.  ( 1 ... s )  |->  ( ( i  .^  X )  .x.  ( ( T `  M )  .X.  ( T `  ( b `  i ) ) ) ) ) )  e.  ( Base `  Y
) )
256 cpmadugsum.s . . . . . . . 8  |-  .-  =  ( -g `  Y )
25725, 26, 256grpaddsubass 16743 . . . . . . 7  |-  ( ( Y  e.  Grp  /\  ( ( ( ( s  +  1 ) 
.^  X )  .x.  ( T `  ( b `
 s ) ) )  e.  ( Base `  Y )  /\  ( Y  gsumg  ( i  e.  ( 0 ... ( s  -  1 ) ) 
|->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) )  e.  (
Base `  Y )  /\  ( Y  gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  X )  .x.  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) )  e.  (
Base `  Y )
) )  ->  (
( ( ( ( s  +  1 ) 
.^  X )  .x.  ( T `  ( b `
 s ) ) )  .+  ( Y 
gsumg  ( i  e.  ( 0 ... ( s  -  1 ) ) 
|->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) ) )  .-  ( Y  gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  X )  .x.  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) ) )  =  ( ( ( ( s  +  1 ) 
.^  X )  .x.  ( T `  ( b `
 s ) ) )  .+  ( ( Y  gsumg  ( i  e.  ( 0 ... ( s  -  1 ) ) 
|->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) )  .-  ( Y  gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  X )  .x.  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) ) ) ) )
258224, 71, 218, 255, 257syl13anc 1266 . . . . . 6  |-  ( ( ( 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  gsumg  ( i  e.  ( 0 ... ( s  -  1 ) ) 
|->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) ) )  .-  ( Y  gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  X )  .x.  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) ) )  =  ( ( ( ( s  +  1 ) 
.^  X )  .x.  ( T `  ( b `
 s ) ) )  .+  ( ( Y  gsumg  ( i  e.  ( 0 ... ( s  -  1 ) ) 
|->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) )  .-  ( Y  gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  X )  .x.  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) ) ) ) )
259 oveq1 6312 . . . . . . . . . . . . . . . 16  |-  ( x  =  i  ->  (
x  -  1 )  =  ( i  - 
1 ) )
260259oveq1d 6320 . . . . . . . . . . . . . . 15  |-  ( x  =  i  ->  (
( x  -  1 )  +  1 )  =  ( ( i  -  1 )  +  1 ) )
261260oveq1d 6320 . . . . . . . . . . . . . 14  |-  ( x  =  i  ->  (
( ( x  - 
1 )  +  1 )  .^  X )  =  ( ( ( i  -  1 )  +  1 )  .^  X ) )
262259fveq2d 5885 . . . . . . . . . . . . . . 15  |-  ( x  =  i  ->  (
b `  ( x  -  1 ) )  =  ( b `  ( i  -  1 ) ) )
263262fveq2d 5885 . . . . . . . . . . . . . 14  |-  ( x  =  i  ->  ( T `  ( b `  ( x  -  1 ) ) )  =  ( T `  (
b `  ( i  -  1 ) ) ) )
264261, 263oveq12d 6323 . . . . . . . . . . . . 13  |-  ( x  =  i  ->  (
( ( ( x  -  1 )  +  1 )  .^  X
)  .x.  ( T `  ( b `  (
x  -  1 ) ) ) )  =  ( ( ( ( i  -  1 )  +  1 )  .^  X )  .x.  ( T `  ( b `  ( i  -  1 ) ) ) ) )
265264cbvmptv 4516 . . . . . . . . . . . 12  |-  ( 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 ) ) ) ) )
266228nncnd 10632 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 1 ... s )  ->  i  e.  CC )
267266adantl 467 . . . . . . . . . . . . . . . 16  |-  ( ( s  e.  NN  /\  i  e.  ( 1 ... s ) )  ->  i  e.  CC )
268 npcan1 10051 . . . . . . . . . . . . . . . 16  |-  ( i  e.  CC  ->  (
( i  -  1 )  +  1 )  =  i )
269267, 268syl 17 . . . . . . . . . . . . . . 15  |-  ( ( s  e.  NN  /\  i  e.  ( 1 ... s ) )  ->  ( ( i  -  1 )  +  1 )  =  i )
270269oveq1d 6320 . . . . . . . . . . . . . 14  |-  ( ( s  e.  NN  /\  i  e.  ( 1 ... s ) )  ->  ( ( ( i  -  1 )  +  1 )  .^  X )  =  ( i  .^  X )
)
271270oveq1d 6320 . . . . . . . . . . . . 13  |-  ( ( s  e.  NN  /\  i  e.  ( 1 ... s ) )  ->  ( ( ( ( i  -  1 )  +  1 ) 
.^  X )  .x.  ( T `  ( b `
 ( i  - 
1 ) ) ) )  =  ( ( i  .^  X )  .x.  ( T `  (
b `  ( i  -  1 ) ) ) ) )
272271mpteq2dva 4510 . . . . . . . . . . . 12  |-  ( 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 ) ) ) ) ) )
273265, 272syl5eq 2475 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) ) )
274273oveq2d 6321 . . . . . . . . . 10  |-  ( s  e.  NN  ->  ( Y  gsumg  ( x  e.  ( 1 ... s ) 
|->  ( ( ( ( x  -  1 )  +  1 )  .^  X )  .x.  ( T `  ( b `  ( x  -  1 ) ) ) ) ) )  =  ( Y  gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  X )  .x.  ( T `  ( b `  ( i  -  1 ) ) ) ) ) ) )
275274ad2antrl 732 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( x  e.  ( 1 ... s )  |->  ( ( ( ( x  - 
1 )  +  1 )  .^  X )  .x.  ( T `  (
b `  ( x  -  1 ) ) ) ) ) )  =  ( Y  gsumg  ( i  e.  ( 1 ... s )  |->  ( ( i  .^  X )  .x.  ( T `  (
b `  ( i  -  1 ) ) ) ) ) ) )
276275oveq1d 6320 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( Y 
gsumg  ( x  e.  (
1 ... s )  |->  ( ( ( ( x  -  1 )  +  1 )  .^  X
)  .x.  ( T `  ( b `  (
x  -  1 ) ) ) ) ) )  .-  ( Y 
gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  X )  .x.  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) ) )  =  ( ( Y  gsumg  ( i  e.  ( 1 ... s )  |->  ( ( i  .^  X )  .x.  ( T `  (
b `  ( i  -  1 ) ) ) ) ) ) 
.-  ( Y  gsumg  ( i  e.  ( 1 ... s )  |->  ( ( i  .^  X )  .x.  ( ( T `  M )  .X.  ( T `  ( b `  i ) ) ) ) ) ) ) )
277 eqid 2422 . . . . . . . . . . 11  |-  ( 0g
`  Y )  =  ( 0g `  Y
)
278 1zzd 10975 . . . . . . . . . . 11  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  1  e.  ZZ )
279 0zd 10956 . . . . . . . . . . 11  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  0  e.  ZZ )
28036nn0zd 11045 . . . . . . . . . . 11  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( s  - 
1 )  e.  ZZ )
281 oveq1 6312 . . . . . . . . . . . . 13  |-  ( i  =  ( x  - 
1 )  ->  (
i  +  1 )  =  ( ( x  -  1 )  +  1 ) )
282281oveq1d 6320 . . . . . . . . . . . 12  |-  ( i  =  ( x  - 
1 )  ->  (
( i  +  1 )  .^  X )  =  ( ( ( x  -  1 )  +  1 )  .^  X ) )
283 fveq2 5881 . . . . . . . . . . . . 13  |-  ( i  =  ( x  - 
1 )  ->  (
b `  i )  =  ( b `  ( x  -  1
) ) )
284283fveq2d 5885 . . . . . . . . . . . 12  |-  ( i  =  ( x  - 
1 )  ->  ( T `  ( b `  i ) )  =  ( T `  (
b `  ( x  -  1 ) ) ) )
285282, 284oveq12d 6323 . . . . . . . . . . 11  |-  ( i  =  ( x  - 
1 )  ->  (
( ( i  +  1 )  .^  X
)  .x.  ( T `  ( b `  i
) ) )  =  ( ( ( ( x  -  1 )  +  1 )  .^  X )  .x.  ( T `  ( b `  ( x  -  1 ) ) ) ) )
28625, 277, 34, 278, 279, 280, 216, 285gsummptshft 17568 . . . . . . . . . 10  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( i  e.  ( 0 ... ( s  -  1 ) )  |->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  (
b `  i )
) ) ) )  =  ( Y  gsumg  ( x  e.  ( ( 0  +  1 ) ... ( ( s  - 
1 )  +  1 ) )  |->  ( ( ( ( x  - 
1 )  +  1 )  .^  X )  .x.  ( T `  (
b `  ( x  -  1 ) ) ) ) ) ) )
287 0p1e1 10728 . . . . . . . . . . . . . 14  |-  ( 0  +  1 )  =  1
288287a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( 0  +  1 )  =  1 )
28977ad2antrl 732 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( s  -  1 )  +  1 )  =  s )
290288, 289oveq12d 6323 . . . . . . . . . . . 12  |-  ( ( ( 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 ) )
291290mpteq1d 4505 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) ) ) )
292291oveq2d 6321 . . . . . . . . . 10  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( x  e.  ( ( 0  +  1 ) ... ( ( s  - 
1 )  +  1 ) )  |->  ( ( ( ( x  - 
1 )  +  1 )  .^  X )  .x.  ( T `  (
b `  ( x  -  1 ) ) ) ) ) )  =  ( Y  gsumg  ( x  e.  ( 1 ... s )  |->  ( ( ( ( x  - 
1 )  +  1 )  .^  X )  .x.  ( T `  (
b `  ( x  -  1 ) ) ) ) ) ) )
293286, 292eqtrd 2463 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( i  e.  ( 0 ... ( s  -  1 ) )  |->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  (
b `  i )
) ) ) )  =  ( Y  gsumg  ( x  e.  ( 1 ... s )  |->  ( ( ( ( x  - 
1 )  +  1 )  .^  X )  .x.  ( T `  (
b `  ( x  -  1 ) ) ) ) ) ) )
294293oveq1d 6320 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( Y 
gsumg  ( i  e.  ( 0 ... ( s  -  1 ) ) 
|->  ( ( ( i  +  1 )  .^  X )  .x.  ( T `  ( b `  i ) ) ) ) )  .-  ( Y  gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  X )  .x.  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) ) )  =  ( ( Y  gsumg  ( x  e.  ( 1 ... s )  |->  ( ( ( ( x  - 
1 )  +  1 )  .^  X )  .x.  ( T `  (
b `  ( x  -  1 ) ) ) ) ) ) 
.-  ( Y  gsumg  ( i  e.  ( 1 ... s )  |->  ( ( i  .^  X )  .x.  ( ( T `  M )  .X.  ( T `  ( b `  i ) ) ) ) ) ) ) )
295 ringabl 17809 . . . . . . . . . . 11  |-  ( Y  e.  Ring  ->  Y  e. 
Abel )
29631, 295syl 17 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  Y  e.  Abel )
297296adantr 466 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  Y  e.  Abel )
298228adantl 467 . . . . . . . . . . . . . . 15  |-  ( ( s  e.  NN  /\  i  e.  ( 1 ... s ) )  ->  i  e.  NN )
299 nnz 10966 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  NN  ->  i  e.  ZZ )
300 elfzm1b 11879 . . . . . . . . . . . . . . . . . 18  |-  ( ( i  e.  ZZ  /\  s  e.  ZZ )  ->  ( i  e.  ( 1 ... s )  <-> 
( i  -  1 )  e.  ( 0 ... ( s  - 
1 ) ) ) )
301299, 201, 300syl2an 479 . . . . . . . . . . . . . . . . 17  |-  ( ( i  e.  NN  /\  s  e.  NN )  ->  ( i  e.  ( 1 ... s )  <-> 
( i  -  1 )  e.  ( 0 ... ( s  - 
1 ) ) ) )
302203adantl 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  NN  /\  s  e.  NN )  ->  ( 0..^ s )  =  ( 0 ... ( s  -  1 ) ) )
303302eqcomd 2430 . . . . . . . . . . . . . . . . . . 19  |-  ( ( i  e.  NN  /\  s  e.  NN )  ->  ( 0 ... (
s  -  1 ) )  =  ( 0..^ s ) )
304303eleq2d 2492 . . . . . . . . . . . . . . . . . 18  |-  ( ( i  e.  NN  /\  s  e.  NN )  ->  ( ( i  - 
1 )  e.  ( 0 ... ( s  -  1 ) )  <-> 
( i  -  1 )  e.  ( 0..^ s ) ) )
305 elfzofz 11942 . . . . . . . . . . . . . . . . . 18  |-  ( ( i  -  1 )  e.  ( 0..^ s )  ->  ( i  -  1 )  e.  ( 0 ... s
) )
306304, 305syl6bi 231 . . . . . . . . . . . . . . . . 17  |-  ( ( i  e.  NN  /\  s  e.  NN )  ->  ( ( i  - 
1 )  e.  ( 0 ... ( s  -  1 ) )  ->  ( i  - 
1 )  e.  ( 0 ... s ) ) )
307301, 306sylbid 218 . . . . . . . . . . . . . . . 16  |-  ( ( i  e.  NN  /\  s  e.  NN )  ->  ( i  e.  ( 1 ... s )  ->  ( i  - 
1 )  e.  ( 0 ... s ) ) )
308307expimpd 606 . . . . . . . . . . . . . . 15  |-  ( i  e.  NN  ->  (
( s  e.  NN  /\  i  e.  ( 1 ... s ) )  ->  ( i  - 
1 )  e.  ( 0 ... s ) ) )
309298, 308mpcom 37 . . . . . . . . . . . . . 14  |-  ( ( s  e.  NN  /\  i  e.  ( 1 ... s ) )  ->  ( i  - 
1 )  e.  ( 0 ... s ) )
310309ex 435 . . . . . . . . . . . . 13  |-  ( s  e.  NN  ->  (
i  e.  ( 1 ... s )  -> 
( i  -  1 )  e.  ( 0 ... s ) ) )
311310ad2antrl 732 . . . . . . . . . . . 12  |-  ( ( ( 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
) ) )
312311imp 430 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) )
313242, 312ffvelrnd 6038 . . . . . . . . . 10  |-  ( ( ( ( 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 )
3142, 3, 6, 4, 5, 25, 9, 8, 7mat2pmatscmxcl 19762 . . . . . . . . . 10  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring )  /\  ( ( b `  ( i  -  1 ) )  e.  B  /\  i  e.  NN0 ) )  ->  (
( i  .^  X
)  .x.  ( T `  ( b `  (
i  -  1 ) ) ) )  e.  ( Base `  Y
) )
315239, 240, 313, 230, 314syl22anc 1265 . . . . . . . . 9  |-  ( ( ( ( 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
) )
316 eqid 2422 . . . . . . . . 9  |-  ( i  e.  ( 1 ... s )  |->  ( ( i  .^  X )  .x.  ( T `  (
b `  ( i  -  1 ) ) ) ) )  =  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  X )  .x.  ( T `  ( b `  ( i  -  1 ) ) ) ) )
317 eqid 2422 . . . . . . . . 9  |-  ( 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 )
) ) ) )
31825, 256, 297, 225, 315, 253, 316, 317gsummptfidmsub 17582 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( i  e.  ( 1 ... s )  |->  ( (