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

Theorem chfacfpmmulgsum 19659
Description: Breaking up a sum of values of the "characteristic factor function" multiplied with a constant polynomial matrix. (Contributed by AV, 23-Nov-2019.)
Hypotheses
Ref Expression
cayhamlem1.a  |-  A  =  ( N Mat  R )
cayhamlem1.b  |-  B  =  ( Base `  A
)
cayhamlem1.p  |-  P  =  (Poly1 `  R )
cayhamlem1.y  |-  Y  =  ( N Mat  P )
cayhamlem1.r  |-  .X.  =  ( .r `  Y )
cayhamlem1.s  |-  .-  =  ( -g `  Y )
cayhamlem1.0  |-  .0.  =  ( 0g `  Y )
cayhamlem1.t  |-  T  =  ( N matToPolyMat  R )
cayhamlem1.g  |-  G  =  ( n  e.  NN0  |->  if ( n  =  0 ,  (  .0.  .-  ( ( T `  M )  .X.  ( T `  ( b `  0 ) ) ) ) ,  if ( n  =  (
s  +  1 ) ,  ( T `  ( b `  s
) ) ,  if ( ( s  +  1 )  <  n ,  .0.  ,  ( ( T `  ( b `
 ( n  - 
1 ) ) ) 
.-  ( ( T `
 M )  .X.  ( T `  ( b `
 n ) ) ) ) ) ) ) )
cayhamlem1.e  |-  .^  =  (.g
`  (mulGrp `  Y )
)
chfacfpmmulgsum.p  |-  .+  =  ( +g  `  Y )
Assertion
Ref Expression
chfacfpmmulgsum  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( i  e.  NN0  |->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  =  ( ( Y  gsumg  ( i  e.  ( 1 ... s )  |->  ( ( i  .^  ( T `  M ) )  .X.  ( ( T `  ( b `  (
i  -  1 ) ) )  .-  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) ) )  .+  ( ( ( ( s  +  1 ) 
.^  ( T `  M ) )  .X.  ( T `  ( b `
 s ) ) )  .-  ( ( T `  M ) 
.X.  ( T `  ( b `  0
) ) ) ) ) )
Distinct variable groups:    B, n    n, M    n, N    R, n    n, Y    n, b    n, s    .0. , n    B, i   
i, G    i, M    i, N    R, i    T, i    .X. , i    .^ , i    i, s    i, b    T, n, i    i, Y    .X. , n    .- , n
Allowed substitution hints:    A( i, n, s, b)    B( s, b)    P( i, n, s, b)    .+ ( i, n, s, b)    R( s, b)    T( s, b)    .X. ( s, b)    .^ ( n, s, b)    G( n, s, b)    M( s, b)    .- ( i, s, b)    N( s, b)    Y( s, b)    .0. ( i, s, b)

Proof of Theorem chfacfpmmulgsum
StepHypRef Expression
1 eqid 2404 . . 3  |-  ( Base `  Y )  =  (
Base `  Y )
2 cayhamlem1.0 . . 3  |-  .0.  =  ( 0g `  Y )
3 chfacfpmmulgsum.p . . 3  |-  .+  =  ( +g  `  Y )
4 crngring 17531 . . . . . . . 8  |-  ( R  e.  CRing  ->  R  e.  Ring )
54anim2i 569 . . . . . . 7  |-  ( ( N  e.  Fin  /\  R  e.  CRing )  -> 
( N  e.  Fin  /\  R  e.  Ring )
)
653adant3 1019 . . . . . 6  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  ( N  e.  Fin  /\  R  e.  Ring ) )
7 cayhamlem1.p . . . . . . 7  |-  P  =  (Poly1 `  R )
8 cayhamlem1.y . . . . . . 7  |-  Y  =  ( N Mat  P )
97, 8pmatring 19488 . . . . . 6  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  Y  e.  Ring )
106, 9syl 17 . . . . 5  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  Y  e.  Ring )
11 ringcmn 17551 . . . . 5  |-  ( Y  e.  Ring  ->  Y  e. CMnd
)
1210, 11syl 17 . . . 4  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  Y  e. CMnd )
1312adantr 465 . . 3  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  Y  e. CMnd )
14 nn0ex 10844 . . . 4  |-  NN0  e.  _V
1514a1i 11 . . 3  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  NN0  e.  _V )
16 simpll 754 . . . . 5  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  NN0 )  ->  ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B ) )
17 simplr 756 . . . . 5  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  NN0 )  ->  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )
18 simpr 461 . . . . 5  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  NN0 )  ->  i  e.  NN0 )
1916, 17, 183jca 1179 . . . 4  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  NN0 )  ->  (
( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) )  /\  i  e.  NN0 ) )
20 cayhamlem1.a . . . . 5  |-  A  =  ( N Mat  R )
21 cayhamlem1.b . . . . 5  |-  B  =  ( Base `  A
)
22 cayhamlem1.r . . . . 5  |-  .X.  =  ( .r `  Y )
23 cayhamlem1.s . . . . 5  |-  .-  =  ( -g `  Y )
24 cayhamlem1.t . . . . 5  |-  T  =  ( N matToPolyMat  R )
25 cayhamlem1.g . . . . 5  |-  G  =  ( n  e.  NN0  |->  if ( n  =  0 ,  (  .0.  .-  ( ( T `  M )  .X.  ( T `  ( b `  0 ) ) ) ) ,  if ( n  =  (
s  +  1 ) ,  ( T `  ( b `  s
) ) ,  if ( ( s  +  1 )  <  n ,  .0.  ,  ( ( T `  ( b `
 ( n  - 
1 ) ) ) 
.-  ( ( T `
 M )  .X.  ( T `  ( b `
 n ) ) ) ) ) ) ) )
26 cayhamlem1.e . . . . 5  |-  .^  =  (.g
`  (mulGrp `  Y )
)
2720, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmulcl 19656 . . . 4  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) )  /\  i  e.  NN0 )  -> 
( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) )  e.  ( Base `  Y
) )
2819, 27syl 17 . . 3  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  NN0 )  ->  (
( i  .^  ( T `  M )
)  .X.  ( G `  i ) )  e.  ( Base `  Y
) )
2920, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmulfsupp 19658 . . 3  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( i  e. 
NN0  |->  ( ( i 
.^  ( T `  M ) )  .X.  ( G `  i ) ) ) finSupp  .0.  )
30 nn0disj 11848 . . . 4  |-  ( ( 0 ... ( s  +  1 ) )  i^i  ( ZZ>= `  (
( s  +  1 )  +  1 ) ) )  =  (/)
3130a1i 11 . . 3  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( 0 ... ( s  +  1 ) )  i^i  ( ZZ>= `  ( (
s  +  1 )  +  1 ) ) )  =  (/) )
32 nnnn0 10845 . . . . . 6  |-  ( s  e.  NN  ->  s  e.  NN0 )
33 peano2nn0 10879 . . . . . 6  |-  ( s  e.  NN0  ->  ( s  +  1 )  e. 
NN0 )
3432, 33syl 17 . . . . 5  |-  ( s  e.  NN  ->  (
s  +  1 )  e.  NN0 )
35 nn0split 11847 . . . . 5  |-  ( ( s  +  1 )  e.  NN0  ->  NN0  =  ( ( 0 ... ( s  +  1 ) )  u.  ( ZZ>=
`  ( ( s  +  1 )  +  1 ) ) ) )
3634, 35syl 17 . . . 4  |-  ( s  e.  NN  ->  NN0  =  ( ( 0 ... ( s  +  1 ) )  u.  ( ZZ>=
`  ( ( s  +  1 )  +  1 ) ) ) )
3736ad2antrl 728 . . 3  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  NN0  =  (
( 0 ... (
s  +  1 ) )  u.  ( ZZ>= `  ( ( s  +  1 )  +  1 ) ) ) )
381, 2, 3, 13, 15, 28, 29, 31, 37gsumsplit2 17274 . 2  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( i  e.  NN0  |->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  =  ( ( Y  gsumg  ( i  e.  ( 0 ... ( s  +  1 ) )  |->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  .+  ( Y  gsumg  ( i  e.  (
ZZ>= `  ( ( s  +  1 )  +  1 ) )  |->  ( ( i  .^  ( T `  M )
)  .X.  ( G `  i ) ) ) ) ) )
39 simpll 754 . . . . . . . 8  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  ( ZZ>= `  ( (
s  +  1 )  +  1 ) ) )  ->  ( N  e.  Fin  /\  R  e. 
CRing  /\  M  e.  B
) )
40 simplr 756 . . . . . . . 8  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  ( ZZ>= `  ( (
s  +  1 )  +  1 ) ) )  ->  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )
41 nncn 10586 . . . . . . . . . . . . 13  |-  ( s  e.  NN  ->  s  e.  CC )
42 add1p1 10831 . . . . . . . . . . . . 13  |-  ( s  e.  CC  ->  (
( s  +  1 )  +  1 )  =  ( s  +  2 ) )
4341, 42syl 17 . . . . . . . . . . . 12  |-  ( s  e.  NN  ->  (
( s  +  1 )  +  1 )  =  ( s  +  2 ) )
4443ad2antrl 728 . . . . . . . . . . 11  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( s  +  1 )  +  1 )  =  ( s  +  2 ) )
4544fveq2d 5855 . . . . . . . . . 10  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ZZ>= `  (
( s  +  1 )  +  1 ) )  =  ( ZZ>= `  ( s  +  2 ) ) )
4645eleq2d 2474 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( i  e.  ( ZZ>= `  ( (
s  +  1 )  +  1 ) )  <-> 
i  e.  ( ZZ>= `  ( s  +  2 ) ) ) )
4746biimpa 484 . . . . . . . 8  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  ( ZZ>= `  ( (
s  +  1 )  +  1 ) ) )  ->  i  e.  ( ZZ>= `  ( s  +  2 ) ) )
4820, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmul0 19657 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) )  /\  i  e.  ( ZZ>= `  ( s  +  2 ) ) )  -> 
( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) )  =  .0.  )
4939, 40, 47, 48syl3anc 1232 . . . . . . 7  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  ( ZZ>= `  ( (
s  +  1 )  +  1 ) ) )  ->  ( (
i  .^  ( T `  M ) )  .X.  ( G `  i ) )  =  .0.  )
5049mpteq2dva 4483 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( i  e.  ( ZZ>= `  ( (
s  +  1 )  +  1 ) ) 
|->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) )  =  ( i  e.  ( ZZ>= `  ( (
s  +  1 )  +  1 ) ) 
|->  .0.  ) )
5150oveq2d 6296 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( i  e.  ( ZZ>= `  (
( s  +  1 )  +  1 ) )  |->  ( ( i 
.^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  =  ( Y  gsumg  ( i  e.  (
ZZ>= `  ( ( s  +  1 )  +  1 ) )  |->  .0.  ) ) )
524, 9sylan2 474 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  R  e.  CRing )  ->  Y  e.  Ring )
53 ringmnd 17529 . . . . . . . . . 10  |-  ( Y  e.  Ring  ->  Y  e. 
Mnd )
5452, 53syl 17 . . . . . . . . 9  |-  ( ( N  e.  Fin  /\  R  e.  CRing )  ->  Y  e.  Mnd )
55543adant3 1019 . . . . . . . 8  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  Y  e.  Mnd )
56 fvex 5861 . . . . . . . 8  |-  ( ZZ>= `  ( ( s  +  1 )  +  1 ) )  e.  _V
5755, 56jctir 538 . . . . . . 7  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  ( Y  e.  Mnd  /\  ( ZZ>=
`  ( ( s  +  1 )  +  1 ) )  e. 
_V ) )
5857adantr 465 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  e. 
Mnd  /\  ( ZZ>= `  ( ( s  +  1 )  +  1 ) )  e.  _V ) )
592gsumz 16331 . . . . . 6  |-  ( ( Y  e.  Mnd  /\  ( ZZ>= `  ( (
s  +  1 )  +  1 ) )  e.  _V )  -> 
( Y  gsumg  ( i  e.  (
ZZ>= `  ( ( s  +  1 )  +  1 ) )  |->  .0.  ) )  =  .0.  )
6058, 59syl 17 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( i  e.  ( ZZ>= `  (
( s  +  1 )  +  1 ) )  |->  .0.  ) )  =  .0.  )
6151, 60eqtrd 2445 . . . 4  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( i  e.  ( ZZ>= `  (
( s  +  1 )  +  1 ) )  |->  ( ( i 
.^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  =  .0.  )
6261oveq2d 6296 . . 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  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  .+  ( Y 
gsumg  ( i  e.  (
ZZ>= `  ( ( s  +  1 )  +  1 ) )  |->  ( ( i  .^  ( T `  M )
)  .X.  ( G `  i ) ) ) ) )  =  ( ( Y  gsumg  ( i  e.  ( 0 ... ( s  +  1 ) ) 
|->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  .+  .0.  )
)
6355adantr 465 . . . 4  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  Y  e.  Mnd )
64 fzfid 12126 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( 0 ... ( s  +  1 ) )  e.  Fin )
65 elfznn0 11828 . . . . . . . 8  |-  ( i  e.  ( 0 ... ( s  +  1 ) )  ->  i  e.  NN0 )
6665, 19sylan2 474 . . . . . . 7  |-  ( ( ( ( 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  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) )  /\  i  e.  NN0 ) )
6766, 27syl 17 . . . . . 6  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  ( 0 ... (
s  +  1 ) ) )  ->  (
( i  .^  ( T `  M )
)  .X.  ( G `  i ) )  e.  ( Base `  Y
) )
6867ralrimiva 2820 . . . . 5  |-  ( ( ( 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  .^  ( T `  M ) )  .X.  ( G `  i ) )  e.  ( Base `  Y
) )
691, 13, 64, 68gsummptcl 17317 . . . 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  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  e.  ( Base `  Y
) )
701, 3, 2mndrid 16268 . . . 4  |-  ( ( Y  e.  Mnd  /\  ( Y  gsumg  ( i  e.  ( 0 ... ( s  +  1 ) ) 
|->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  e.  ( Base `  Y ) )  -> 
( ( Y  gsumg  ( i  e.  ( 0 ... ( s  +  1 ) )  |->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  .+  .0.  )  =  ( Y  gsumg  ( i  e.  ( 0 ... ( s  +  1 ) ) 
|->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) ) )
7163, 69, 70syl2anc 661 . . 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  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  .+  .0.  )  =  ( Y  gsumg  ( i  e.  ( 0 ... ( s  +  1 ) )  |->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) ) )
7262, 71eqtrd 2445 . 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  +  1 ) ) 
|->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  .+  ( Y 
gsumg  ( i  e.  (
ZZ>= `  ( ( s  +  1 )  +  1 ) )  |->  ( ( i  .^  ( T `  M )
)  .X.  ( G `  i ) ) ) ) )  =  ( Y  gsumg  ( i  e.  ( 0 ... ( s  +  1 ) ) 
|->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) ) )
7332ad2antrl 728 . . . 4  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  s  e.  NN0 )
741, 3, 13, 73, 67gsummptfzsplit 17277 . . 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  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  =  ( ( Y  gsumg  ( i  e.  ( 0 ... s )  |->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  .+  ( Y  gsumg  ( i  e.  {
( s  +  1 ) }  |->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) ) ) )
75 elfznn0 11828 . . . . . . 7  |-  ( i  e.  ( 0 ... s )  ->  i  e.  NN0 )
7675, 28sylan2 474 . . . . . 6  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  ( 0 ... s
) )  ->  (
( i  .^  ( T `  M )
)  .X.  ( G `  i ) )  e.  ( Base `  Y
) )
771, 3, 13, 73, 76gsummptfzsplitl 17278 . . . . 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 )  |->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  =  ( ( Y  gsumg  ( i  e.  ( 1 ... s )  |->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  .+  ( Y  gsumg  ( i  e.  {
0 }  |->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) ) ) )
78 0nn0 10853 . . . . . . . 8  |-  0  e.  NN0
7978a1i 11 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  0  e.  NN0 )
8020, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmulcl 19656 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) )  /\  0  e.  NN0 )  -> 
( ( 0  .^  ( T `  M ) )  .X.  ( G `  0 ) )  e.  ( Base `  Y
) )
8179, 80mpd3an3 1329 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( 0 
.^  ( T `  M ) )  .X.  ( G `  0 ) )  e.  ( Base `  Y ) )
82 oveq1 6287 . . . . . . . . 9  |-  ( i  =  0  ->  (
i  .^  ( T `  M ) )  =  ( 0  .^  ( T `  M )
) )
83 fveq2 5851 . . . . . . . . 9  |-  ( i  =  0  ->  ( G `  i )  =  ( G ` 
0 ) )
8482, 83oveq12d 6298 . . . . . . . 8  |-  ( i  =  0  ->  (
( i  .^  ( T `  M )
)  .X.  ( G `  i ) )  =  ( ( 0  .^  ( T `  M ) )  .X.  ( G `  0 ) ) )
851, 84gsumsn 17304 . . . . . . 7  |-  ( ( Y  e.  Mnd  /\  0  e.  NN0  /\  (
( 0  .^  ( T `  M )
)  .X.  ( G `  0 ) )  e.  ( Base `  Y
) )  ->  ( Y  gsumg  ( i  e.  {
0 }  |->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  =  ( ( 0  .^  ( T `  M ) )  .X.  ( G `  0 ) ) )
8663, 79, 81, 85syl3anc 1232 . . . . . 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  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  =  ( ( 0  .^  ( T `  M ) )  .X.  ( G `  0 ) ) )
8786oveq2d 6296 . . . . 5  |-  ( ( ( 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  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  .+  ( Y 
gsumg  ( i  e.  {
0 }  |->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) ) )  =  ( ( Y 
gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  .+  ( ( 0  .^  ( T `  M ) )  .X.  ( G `  0 ) ) ) )
8877, 87eqtrd 2445 . . . 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  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  =  ( ( Y  gsumg  ( i  e.  ( 1 ... s )  |->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  .+  ( ( 0  .^  ( T `  M ) )  .X.  ( G `  0 ) ) ) )
89 ovex 6308 . . . . . 6  |-  ( s  +  1 )  e. 
_V
9089a1i 11 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( s  +  1 )  e.  _V )
91 1nn0 10854 . . . . . . . 8  |-  1  e.  NN0
9291a1i 11 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  1  e.  NN0 )
9373, 92nn0addcld 10899 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( s  +  1 )  e.  NN0 )
9420, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmulcl 19656 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) )  /\  ( s  +  1 )  e.  NN0 )  ->  ( ( ( s  +  1 )  .^  ( T `  M ) )  .X.  ( G `  ( s  +  1 ) ) )  e.  ( Base `  Y
) )
9593, 94mpd3an3 1329 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( ( s  +  1 ) 
.^  ( T `  M ) )  .X.  ( G `  ( s  +  1 ) ) )  e.  ( Base `  Y ) )
96 oveq1 6287 . . . . . . 7  |-  ( i  =  ( s  +  1 )  ->  (
i  .^  ( T `  M ) )  =  ( ( s  +  1 )  .^  ( T `  M )
) )
97 fveq2 5851 . . . . . . 7  |-  ( i  =  ( s  +  1 )  ->  ( G `  i )  =  ( G `  ( s  +  1 ) ) )
9896, 97oveq12d 6298 . . . . . 6  |-  ( i  =  ( s  +  1 )  ->  (
( i  .^  ( T `  M )
)  .X.  ( G `  i ) )  =  ( ( ( s  +  1 )  .^  ( T `  M ) )  .X.  ( G `  ( s  +  1 ) ) ) )
991, 98gsumsn 17304 . . . . 5  |-  ( ( Y  e.  Mnd  /\  ( s  +  1 )  e.  _V  /\  ( ( ( s  +  1 )  .^  ( T `  M ) )  .X.  ( G `  ( s  +  1 ) ) )  e.  ( Base `  Y
) )  ->  ( Y  gsumg  ( i  e.  {
( s  +  1 ) }  |->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  =  ( ( ( s  +  1 )  .^  ( T `  M ) )  .X.  ( G `  ( s  +  1 ) ) ) )
10063, 90, 95, 99syl3anc 1232 . . . 4  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( i  e.  { ( s  +  1 ) } 
|->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  =  ( ( ( s  +  1 )  .^  ( T `  M ) )  .X.  ( G `  ( s  +  1 ) ) ) )
10188, 100oveq12d 6298 . . 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  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  .+  ( Y 
gsumg  ( i  e.  {
( s  +  1 ) }  |->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) ) )  =  ( ( ( Y  gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  .+  ( ( 0  .^  ( T `  M ) )  .X.  ( G `  0 ) ) )  .+  (
( ( s  +  1 )  .^  ( T `  M )
)  .X.  ( G `  ( s  +  1 ) ) ) ) )
102 fzfid 12126 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( 1 ... s )  e.  Fin )
103 simpll 754 . . . . . . . 8  |-  ( ( ( ( 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  /\  R  e.  CRing  /\  M  e.  B ) )
104 simplr 756 . . . . . . . 8  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  ( 1 ... s
) )  ->  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )
105 elfznn 11770 . . . . . . . . . 10  |-  ( i  e.  ( 1 ... s )  ->  i  e.  NN )
106105nnnn0d 10895 . . . . . . . . 9  |-  ( i  e.  ( 1 ... s )  ->  i  e.  NN0 )
107106adantl 466 . . . . . . . 8  |-  ( ( ( ( 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 )
108103, 104, 107, 27syl3anc 1232 . . . . . . 7  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  ( 1 ... s
) )  ->  (
( i  .^  ( T `  M )
)  .X.  ( G `  i ) )  e.  ( Base `  Y
) )
109108ralrimiva 2820 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  A. i  e.  ( 1 ... s ) ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) )  e.  ( Base `  Y
) )
1101, 13, 102, 109gsummptcl 17317 . . . . 5  |-  ( ( ( 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  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  e.  ( Base `  Y
) )
1111, 3mndass 16256 . . . . 5  |-  ( ( Y  e.  Mnd  /\  ( ( Y  gsumg  ( i  e.  ( 1 ... s )  |->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  e.  ( Base `  Y
)  /\  ( (
0  .^  ( T `  M ) )  .X.  ( G `  0 ) )  e.  ( Base `  Y )  /\  (
( ( s  +  1 )  .^  ( T `  M )
)  .X.  ( G `  ( s  +  1 ) ) )  e.  ( Base `  Y
) ) )  -> 
( ( ( Y 
gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  .+  ( ( 0  .^  ( T `  M ) )  .X.  ( G `  0 ) ) )  .+  (
( ( s  +  1 )  .^  ( T `  M )
)  .X.  ( G `  ( s  +  1 ) ) ) )  =  ( ( Y 
gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  .+  ( ( ( 0  .^  ( T `  M )
)  .X.  ( G `  0 ) ) 
.+  ( ( ( s  +  1 ) 
.^  ( T `  M ) )  .X.  ( G `  ( s  +  1 ) ) ) ) ) )
11263, 110, 81, 95, 111syl13anc 1234 . . . 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  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  .+  ( ( 0  .^  ( T `  M ) )  .X.  ( G `  0 ) ) )  .+  (
( ( s  +  1 )  .^  ( T `  M )
)  .X.  ( G `  ( s  +  1 ) ) ) )  =  ( ( Y 
gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  .+  ( ( ( 0  .^  ( T `  M )
)  .X.  ( G `  0 ) ) 
.+  ( ( ( s  +  1 ) 
.^  ( T `  M ) )  .X.  ( G `  ( s  +  1 ) ) ) ) ) )
11325a1i 11 . . . . . . . . 9  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  ( 1 ... s
) )  ->  G  =  ( n  e. 
NN0  |->  if ( n  =  0 ,  (  .0.  .-  ( ( T `  M )  .X.  ( T `  (
b `  0 )
) ) ) ,  if ( n  =  ( s  +  1 ) ,  ( T `
 ( b `  s ) ) ,  if ( ( s  +  1 )  < 
n ,  .0.  , 
( ( T `  ( b `  (
n  -  1 ) ) )  .-  (
( T `  M
)  .X.  ( T `  ( b `  n
) ) ) ) ) ) ) ) )
114105nnne0d 10623 . . . . . . . . . . . . . 14  |-  ( i  e.  ( 1 ... s )  ->  i  =/=  0 )
115114ad2antlr 727 . . . . . . . . . . . . 13  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  ->  i  =/=  0 )
116 neeq1 2686 . . . . . . . . . . . . . 14  |-  ( n  =  i  ->  (
n  =/=  0  <->  i  =/=  0 ) )
117116adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  ->  (
n  =/=  0  <->  i  =/=  0 ) )
118115, 117mpbird 234 . . . . . . . . . . . 12  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  ->  n  =/=  0 )
119 eqneqall 2612 . . . . . . . . . . . 12  |-  ( n  =  0  ->  (
n  =/=  0  ->  .0.  =  ( T `  ( b `  (
i  -  1 ) ) ) ) )
120118, 119mpan9 469 . . . . . . . . . . 11  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  /\  n  =  0 )  ->  .0.  =  ( T `  ( b `  (
i  -  1 ) ) ) )
121 simplr 756 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  /\  n  =  0 )  ->  n  =  i )
122 eqeq1 2408 . . . . . . . . . . . . . . . . 17  |-  ( 0  =  n  ->  (
0  =  i  <->  n  =  i ) )
123122eqcoms 2416 . . . . . . . . . . . . . . . 16  |-  ( n  =  0  ->  (
0  =  i  <->  n  =  i ) )
124123adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  /\  n  =  0 )  -> 
( 0  =  i  <-> 
n  =  i ) )
125121, 124mpbird 234 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  /\  n  =  0 )  -> 
0  =  i )
126125fveq2d 5855 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  /\  n  =  0 )  -> 
( b `  0
)  =  ( b `
 i ) )
127126fveq2d 5855 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  /\  n  =  0 )  -> 
( T `  (
b `  0 )
)  =  ( T `
 ( b `  i ) ) )
128127oveq2d 6296 . . . . . . . . . . 11  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  /\  n  =  0 )  -> 
( ( T `  M )  .X.  ( T `  ( b `  0 ) ) )  =  ( ( T `  M ) 
.X.  ( T `  ( b `  i
) ) ) )
129120, 128oveq12d 6298 . . . . . . . . . 10  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  /\  n  =  0 )  -> 
(  .0.  .-  (
( T `  M
)  .X.  ( T `  ( b `  0
) ) ) )  =  ( ( T `
 ( b `  ( i  -  1 ) ) )  .-  ( ( T `  M )  .X.  ( T `  ( b `  i ) ) ) ) )
130 elfz2 11735 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... s )  <->  ( (
1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  /\  (
1  <_  i  /\  i  <_  s ) ) )
131 zleltp1 10957 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( i  e.  ZZ  /\  s  e.  ZZ )  ->  ( i  <_  s  <->  i  <  ( s  +  1 ) ) )
132131ancoms 453 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  e.  ZZ  /\  i  e.  ZZ )  ->  ( i  <_  s  <->  i  <  ( s  +  1 ) ) )
1331323adant1 1017 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  ->  (
i  <_  s  <->  i  <  ( s  +  1 ) ) )
134133biimpcd 226 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  <_  s  ->  (
( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  ->  i  <  ( s  +  1 ) ) )
135134adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  <_  i  /\  i  <_  s )  -> 
( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  ->  i  <  ( s  +  1 ) ) )
136135impcom 430 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  /\  ( 1  <_  i  /\  i  <_  s ) )  ->  i  <  ( s  +  1 ) )
137136orcd 392 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  /\  ( 1  <_  i  /\  i  <_  s ) )  ->  ( i  <  ( s  +  1 )  \/  ( s  +  1 )  < 
i ) )
138 zre 10911 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ZZ  ->  s  e.  RR )
139 1red 9643 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ZZ  ->  1  e.  RR )
140138, 139readdcld 9655 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s  e.  ZZ  ->  (
s  +  1 )  e.  RR )
141 zre 10911 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  e.  ZZ  ->  i  e.  RR )
142140, 141anim12ci 567 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( s  e.  ZZ  /\  i  e.  ZZ )  ->  ( i  e.  RR  /\  ( s  +  1 )  e.  RR ) )
1431423adant1 1017 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  ->  (
i  e.  RR  /\  ( s  +  1 )  e.  RR ) )
144 lttri2 9700 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i  e.  RR  /\  ( s  +  1 )  e.  RR )  ->  ( i  =/=  ( s  +  1 )  <->  ( i  < 
( s  +  1 )  \/  ( s  +  1 )  < 
i ) ) )
145143, 144syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  ->  (
i  =/=  ( s  +  1 )  <->  ( i  <  ( s  +  1 )  \/  ( s  +  1 )  < 
i ) ) )
146145adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  /\  ( 1  <_  i  /\  i  <_  s ) )  ->  ( i  =/=  ( s  +  1 )  <->  ( i  < 
( s  +  1 )  \/  ( s  +  1 )  < 
i ) ) )
147137, 146mpbird 234 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  /\  ( 1  <_  i  /\  i  <_  s ) )  ->  i  =/=  ( s  +  1 ) )
148130, 147sylbi 197 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 1 ... s )  ->  i  =/=  ( s  +  1 ) )
149148ad2antlr 727 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  ->  i  =/=  ( s  +  1 ) )
150 neeq1 2686 . . . . . . . . . . . . . . . . 17  |-  ( n  =  i  ->  (
n  =/=  ( s  +  1 )  <->  i  =/=  ( s  +  1 ) ) )
151150adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  ->  (
n  =/=  ( s  +  1 )  <->  i  =/=  ( s  +  1 ) ) )
152149, 151mpbird 234 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  ->  n  =/=  ( s  +  1 ) )
153152adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  /\  -.  n  =  0 )  ->  n  =/=  (
s  +  1 ) )
154153neneqd 2607 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  /\  -.  n  =  0 )  ->  -.  n  =  ( s  +  1 ) )
155154pm2.21d 108 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  /\  -.  n  =  0 )  ->  ( n  =  ( s  +  1 )  ->  ( T `  ( b `  s
) )  =  ( ( T `  (
b `  ( i  -  1 ) ) )  .-  ( ( T `  M ) 
.X.  ( T `  ( b `  i
) ) ) ) ) )
156155imp 429 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  /\  -.  n  =  0 )  /\  n  =  ( s  +  1 ) )  ->  ( T `  ( b `  s
) )  =  ( ( T `  (
b `  ( i  -  1 ) ) )  .-  ( ( T `  M ) 
.X.  ( T `  ( b `  i
) ) ) ) )
157105nnred 10593 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 1 ... s )  ->  i  e.  RR )
158 eleq1 2476 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  i  ->  (
n  e.  RR  <->  i  e.  RR ) )
159157, 158syl5ibrcom 224 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... s )  ->  (
n  =  i  ->  n  e.  RR )
)
160159adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  ( 1 ... s
) )  ->  (
n  =  i  ->  n  e.  RR )
)
161160imp 429 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  ->  n  e.  RR )
16273nn0red 10896 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  s  e.  RR )
163162ad2antrr 726 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  ->  s  e.  RR )
164 1red 9643 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  ->  1  e.  RR )
165163, 164readdcld 9655 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  ->  (
s  +  1 )  e.  RR )
166130, 136sylbi 197 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... s )  ->  i  <  ( s  +  1 ) )
167166ad2antlr 727 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  ->  i  <  ( s  +  1 ) )
168 breq1 4400 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  i  ->  (
n  <  ( s  +  1 )  <->  i  <  ( s  +  1 ) ) )
169168adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  ->  (
n  <  ( s  +  1 )  <->  i  <  ( s  +  1 ) ) )
170167, 169mpbird 234 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  ->  n  <  ( s  +  1 ) )
171161, 165, 170ltnsymd 9768 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  ->  -.  ( s  +  1 )  <  n )
172171pm2.21d 108 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  ->  (
( s  +  1 )  <  n  ->  .0.  =  ( ( T `
 ( b `  ( i  -  1 ) ) )  .-  ( ( T `  M )  .X.  ( T `  ( b `  i ) ) ) ) ) )
173172ad2antrr 726 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  /\  -.  n  =  0 )  /\  -.  n  =  ( s  +  1 ) )  ->  (
( s  +  1 )  <  n  ->  .0.  =  ( ( T `
 ( b `  ( i  -  1 ) ) )  .-  ( ( T `  M )  .X.  ( T `  ( b `  i ) ) ) ) ) )
174173imp 429 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  ( 1 ... s
) )  /\  n  =  i )  /\  -.  n  =  0
)  /\  -.  n  =  ( s  +  1 ) )  /\  ( s  +  1 )  <  n )  ->  .0.  =  (
( T `  (
b `  ( i  -  1 ) ) )  .-  ( ( T `  M ) 
.X.  ( T `  ( b `  i
) ) ) ) )
175 simp-4r 771 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  ( 1 ... s
) )  /\  n  =  i )  /\  -.  n  =  0
)  /\  -.  n  =  ( s  +  1 ) )  /\  -.  ( s  +  1 )  <  n )  ->  n  =  i )
176175oveq1d 6295 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  ( 1 ... s
) )  /\  n  =  i )  /\  -.  n  =  0
)  /\  -.  n  =  ( s  +  1 ) )  /\  -.  ( s  +  1 )  <  n )  ->  ( n  - 
1 )  =  ( i  -  1 ) )
177176fveq2d 5855 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  ( 1 ... s
) )  /\  n  =  i )  /\  -.  n  =  0
)  /\  -.  n  =  ( s  +  1 ) )  /\  -.  ( s  +  1 )  <  n )  ->  ( b `  ( n  -  1
) )  =  ( b `  ( i  -  1 ) ) )
178177fveq2d 5855 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  ( 1 ... s
) )  /\  n  =  i )  /\  -.  n  =  0
)  /\  -.  n  =  ( s  +  1 ) )  /\  -.  ( s  +  1 )  <  n )  ->  ( T `  ( b `  (
n  -  1 ) ) )  =  ( T `  ( b `
 ( i  - 
1 ) ) ) )
179175fveq2d 5855 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  ( 1 ... s
) )  /\  n  =  i )  /\  -.  n  =  0
)  /\  -.  n  =  ( s  +  1 ) )  /\  -.  ( s  +  1 )  <  n )  ->  ( b `  n )  =  ( b `  i ) )
180179fveq2d 5855 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  ( 1 ... s
) )  /\  n  =  i )  /\  -.  n  =  0
)  /\  -.  n  =  ( s  +  1 ) )  /\  -.  ( s  +  1 )  <  n )  ->  ( T `  ( b `  n
) )  =  ( T `  ( b `
 i ) ) )
181180oveq2d 6296 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  ( 1 ... s
) )  /\  n  =  i )  /\  -.  n  =  0
)  /\  -.  n  =  ( s  +  1 ) )  /\  -.  ( s  +  1 )  <  n )  ->  ( ( T `
 M )  .X.  ( T `  ( b `
 n ) ) )  =  ( ( T `  M ) 
.X.  ( T `  ( b `  i
) ) ) )
182178, 181oveq12d 6298 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  ( 1 ... s
) )  /\  n  =  i )  /\  -.  n  =  0
)  /\  -.  n  =  ( s  +  1 ) )  /\  -.  ( s  +  1 )  <  n )  ->  ( ( T `
 ( b `  ( n  -  1
) ) )  .-  ( ( T `  M )  .X.  ( T `  ( b `  n ) ) ) )  =  ( ( T `  ( b `
 ( i  - 
1 ) ) ) 
.-  ( ( T `
 M )  .X.  ( T `  ( b `
 i ) ) ) ) )
183174, 182ifeqda 3920 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  /\  -.  n  =  0 )  /\  -.  n  =  ( s  +  1 ) )  ->  if ( ( s  +  1 )  <  n ,  .0.  ,  ( ( T `  ( b `
 ( n  - 
1 ) ) ) 
.-  ( ( T `
 M )  .X.  ( T `  ( b `
 n ) ) ) ) )  =  ( ( T `  ( b `  (
i  -  1 ) ) )  .-  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) )
184156, 183ifeqda 3920 . . . . . . . . . 10  |-  ( ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  /\  -.  n  =  0 )  ->  if ( n  =  ( s  +  1 ) ,  ( T `  ( b `
 s ) ) ,  if ( ( s  +  1 )  <  n ,  .0.  ,  ( ( T `  ( b `  (
n  -  1 ) ) )  .-  (
( T `  M
)  .X.  ( T `  ( b `  n
) ) ) ) ) )  =  ( ( T `  (
b `  ( i  -  1 ) ) )  .-  ( ( T `  M ) 
.X.  ( T `  ( b `  i
) ) ) ) )
185129, 184ifeqda 3920 . . . . . . . . 9  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  i  e.  ( 1 ... s ) )  /\  n  =  i )  ->  if ( n  =  0 ,  (  .0.  .-  (
( T `  M
)  .X.  ( T `  ( b `  0
) ) ) ) ,  if ( n  =  ( s  +  1 ) ,  ( T `  ( b `
 s ) ) ,  if ( ( s  +  1 )  <  n ,  .0.  ,  ( ( T `  ( b `  (
n  -  1 ) ) )  .-  (
( T `  M
)  .X.  ( T `  ( b `  n
) ) ) ) ) ) )  =  ( ( T `  ( b `  (
i  -  1 ) ) )  .-  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) )
186 ovex 6308 . . . . . . . . . 10  |-  ( ( T `  ( b `
 ( i  - 
1 ) ) ) 
.-  ( ( T `
 M )  .X.  ( T `  ( b `
 i ) ) ) )  e.  _V
187186a1i 11 . . . . . . . . 9  |-  ( ( ( ( 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 ) ) )  .-  ( ( T `  M ) 
.X.  ( T `  ( b `  i
) ) ) )  e.  _V )
188113, 185, 107, 187fvmptd 5940 . . . . . . . 8  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  ( 1 ... s
) )  ->  ( G `  i )  =  ( ( T `
 ( b `  ( i  -  1 ) ) )  .-  ( ( T `  M )  .X.  ( T `  ( b `  i ) ) ) ) )
189188oveq2d 6296 . . . . . . 7  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  ( 1 ... s
) )  ->  (
( i  .^  ( T `  M )
)  .X.  ( G `  i ) )  =  ( ( i  .^  ( T `  M ) )  .X.  ( ( T `  ( b `  ( i  -  1 ) ) )  .-  ( ( T `  M )  .X.  ( T `  ( b `  i ) ) ) ) ) )
190189mpteq2dva 4483 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( i  e.  ( 1 ... s
)  |->  ( ( i 
.^  ( T `  M ) )  .X.  ( G `  i ) ) )  =  ( i  e.  ( 1 ... s )  |->  ( ( i  .^  ( T `  M )
)  .X.  ( ( T `  ( b `  ( i  -  1 ) ) )  .-  ( ( T `  M )  .X.  ( T `  ( b `  i ) ) ) ) ) ) )
191190oveq2d 6296 . . . . 5  |-  ( ( ( 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  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  =  ( Y  gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  ( T `  M ) )  .X.  ( ( T `  ( b `  ( i  -  1 ) ) )  .-  ( ( T `  M )  .X.  ( T `  ( b `  i ) ) ) ) ) ) ) )
19225a1i 11 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  G  =  ( n  e.  NN0  |->  if ( n  =  0 ,  (  .0.  .-  (
( T `  M
)  .X.  ( T `  ( b `  0
) ) ) ) ,  if ( n  =  ( s  +  1 ) ,  ( T `  ( b `
 s ) ) ,  if ( ( s  +  1 )  <  n ,  .0.  ,  ( ( T `  ( b `  (
n  -  1 ) ) )  .-  (
( T `  M
)  .X.  ( T `  ( b `  n
) ) ) ) ) ) ) ) )
193 nn0p1gt0 10868 . . . . . . . . . . . . . . 15  |-  ( s  e.  NN0  ->  0  < 
( s  +  1 ) )
194 0red 9629 . . . . . . . . . . . . . . . . 17  |-  ( s  e.  NN0  ->  0  e.  RR )
195 ltne 9714 . . . . . . . . . . . . . . . . 17  |-  ( ( 0  e.  RR  /\  0  <  ( s  +  1 ) )  -> 
( s  +  1 )  =/=  0 )
196194, 195sylan 471 . . . . . . . . . . . . . . . 16  |-  ( ( s  e.  NN0  /\  0  <  ( s  +  1 ) )  -> 
( s  +  1 )  =/=  0 )
197 neeq1 2686 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( s  +  1 )  ->  (
n  =/=  0  <->  (
s  +  1 )  =/=  0 ) )
198196, 197syl5ibrcom 224 . . . . . . . . . . . . . . 15  |-  ( ( s  e.  NN0  /\  0  <  ( s  +  1 ) )  -> 
( n  =  ( s  +  1 )  ->  n  =/=  0
) )
199193, 198mpdan 668 . . . . . . . . . . . . . 14  |-  ( s  e.  NN0  ->  ( n  =  ( s  +  1 )  ->  n  =/=  0 ) )
20032, 199syl 17 . . . . . . . . . . . . 13  |-  ( s  e.  NN  ->  (
n  =  ( s  +  1 )  ->  n  =/=  0 ) )
201200ad2antrl 728 . . . . . . . . . . . 12  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( n  =  ( s  +  1 )  ->  n  =/=  0 ) )
202201imp 429 . . . . . . . . . . 11  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  n  =  ( s  +  1 ) )  ->  n  =/=  0 )
203 eqneqall 2612 . . . . . . . . . . 11  |-  ( n  =  0  ->  (
n  =/=  0  -> 
(  .0.  .-  (
( T `  M
)  .X.  ( T `  ( b `  0
) ) ) )  =  ( T `  ( b `  s
) ) ) )
204202, 203mpan9 469 . . . . . . . . . 10  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  n  =  ( s  +  1 ) )  /\  n  =  0 )  ->  (  .0.  .-  ( ( T `
 M )  .X.  ( T `  ( b `
 0 ) ) ) )  =  ( T `  ( b `
 s ) ) )
205 iftrue 3893 . . . . . . . . . . 11  |-  ( n  =  ( s  +  1 )  ->  if ( n  =  (
s  +  1 ) ,  ( T `  ( b `  s
) ) ,  if ( ( s  +  1 )  <  n ,  .0.  ,  ( ( T `  ( b `
 ( n  - 
1 ) ) ) 
.-  ( ( T `
 M )  .X.  ( T `  ( b `
 n ) ) ) ) ) )  =  ( T `  ( b `  s
) ) )
206205ad2antlr 727 . . . . . . . . . 10  |-  ( ( ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  /\  n  =  ( s  +  1 ) )  /\  -.  n  =  0 )  ->  if ( n  =  ( s  +  1 ) ,  ( T `  ( b `  s
) ) ,  if ( ( s  +  1 )  <  n ,  .0.  ,  ( ( T `  ( b `
 ( n  - 
1 ) ) ) 
.-  ( ( T `
 M )  .X.  ( T `  ( b `
 n ) ) ) ) ) )  =  ( T `  ( b `  s
) ) )
207204, 206ifeqda 3920 . . . . . . . . 9  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  n  =  ( s  +  1 ) )  ->  if ( n  =  0 ,  (  .0.  .-  ( ( T `  M )  .X.  ( T `  ( b `  0 ) ) ) ) ,  if ( n  =  (
s  +  1 ) ,  ( T `  ( b `  s
) ) ,  if ( ( s  +  1 )  <  n ,  .0.  ,  ( ( T `  ( b `
 ( n  - 
1 ) ) ) 
.-  ( ( T `
 M )  .X.  ( T `  ( b `
 n ) ) ) ) ) ) )  =  ( T `
 ( b `  s ) ) )
20873, 33syl 17 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( s  +  1 )  e.  NN0 )
209 fvex 5861 . . . . . . . . . 10  |-  ( T `
 ( b `  s ) )  e. 
_V
210209a1i 11 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( T `  ( b `  s
) )  e.  _V )
211192, 207, 208, 210fvmptd 5940 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( G `  ( s  +  1 ) )  =  ( T `  ( b `
 s ) ) )
212211oveq2d 6296 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( ( s  +  1 ) 
.^  ( T `  M ) )  .X.  ( G `  ( s  +  1 ) ) )  =  ( ( ( s  +  1 )  .^  ( T `  M ) )  .X.  ( T `  ( b `
 s ) ) ) )
21324, 20, 21, 7, 8mat2pmatbas 19521 . . . . . . . . . . . . 13  |-  ( ( N  e.  Fin  /\  R  e.  Ring  /\  M  e.  B )  ->  ( T `  M )  e.  ( Base `  Y
) )
2144, 213syl3an2 1266 . . . . . . . . . . . 12  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  ( T `  M )  e.  ( Base `  Y
) )
215 eqid 2404 . . . . . . . . . . . . . 14  |-  (mulGrp `  Y )  =  (mulGrp `  Y )
216215, 1mgpbas 17469 . . . . . . . . . . . . 13  |-  ( Base `  Y )  =  (
Base `  (mulGrp `  Y
) )
217 eqid 2404 . . . . . . . . . . . . 13  |-  ( 0g
`  (mulGrp `  Y )
)  =  ( 0g
`  (mulGrp `  Y )
)
218216, 217, 26mulg0 16473 . . . . . . . . . . . 12  |-  ( ( T `  M )  e.  ( Base `  Y
)  ->  ( 0 
.^  ( T `  M ) )  =  ( 0g `  (mulGrp `  Y ) ) )
219214, 218syl 17 . . . . . . . . . . 11  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  (
0  .^  ( T `  M ) )  =  ( 0g `  (mulGrp `  Y ) ) )
220 eqid 2404 . . . . . . . . . . . 12  |-  ( 1r
`  Y )  =  ( 1r `  Y
)
221215, 220ringidval 17477 . . . . . . . . . . 11  |-  ( 1r
`  Y )  =  ( 0g `  (mulGrp `  Y ) )
222219, 221syl6eqr 2463 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  (
0  .^  ( T `  M ) )  =  ( 1r `  Y
) )
223222adantr 465 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( 0  .^  ( T `  M ) )  =  ( 1r
`  Y ) )
224223oveq1d 6295 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( 0 
.^  ( T `  M ) )  .X.  ( G `  0 ) )  =  ( ( 1r `  Y ) 
.X.  ( G ` 
0 ) ) )
225523adant3 1019 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  Y  e.  Ring )
226225adantr 465 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  Y  e.  Ring )
22720, 21, 7, 8, 22, 23, 2, 24, 25chfacfisf 19649 . . . . . . . . . . 11  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  G : NN0 --> (
Base `  Y )
)
2284, 227syl3anl2 1281 . . . . . . . . . 10  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  G : NN0 --> (
Base `  Y )
)
229228, 79ffvelrnd 6012 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( G ` 
0 )  e.  (
Base `  Y )
)
2301, 22, 220ringlidm 17544 . . . . . . . . 9  |-  ( ( Y  e.  Ring  /\  ( G `  0 )  e.  ( Base `  Y
) )  ->  (
( 1r `  Y
)  .X.  ( G `  0 ) )  =  ( G ` 
0 ) )
231226, 229, 230syl2anc 661 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( 1r
`  Y )  .X.  ( G `  0 ) )  =  ( G `
 0 ) )
232 iftrue 3893 . . . . . . . . . 10  |-  ( n  =  0  ->  if ( n  =  0 ,  (  .0.  .-  (
( T `  M
)  .X.  ( T `  ( b `  0
) ) ) ) ,  if ( n  =  ( s  +  1 ) ,  ( T `  ( b `
 s ) ) ,  if ( ( s  +  1 )  <  n ,  .0.  ,  ( ( T `  ( b `  (
n  -  1 ) ) )  .-  (
( T `  M
)  .X.  ( T `  ( b `  n
) ) ) ) ) ) )  =  (  .0.  .-  (
( T `  M
)  .X.  ( T `  ( b `  0
) ) ) ) )
233232adantl 466 . . . . . . . . 9  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  n  =  0 )  ->  if ( n  =  0 ,  (  .0.  .-  ( ( T `  M )  .X.  ( T `  ( b `  0 ) ) ) ) ,  if ( n  =  (
s  +  1 ) ,  ( T `  ( b `  s
) ) ,  if ( ( s  +  1 )  <  n ,  .0.  ,  ( ( T `  ( b `
 ( n  - 
1 ) ) ) 
.-  ( ( T `
 M )  .X.  ( T `  ( b `
 n ) ) ) ) ) ) )  =  (  .0.  .-  ( ( T `  M )  .X.  ( T `  ( b `  0 ) ) ) ) )
234 ovex 6308 . . . . . . . . . 10  |-  (  .0.  .-  ( ( T `  M )  .X.  ( T `  ( b `  0 ) ) ) )  e.  _V
235234a1i 11 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  (  .0.  .-  ( ( T `  M )  .X.  ( T `  ( b `  0 ) ) ) )  e.  _V )
236192, 233, 79, 235fvmptd 5940 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( G ` 
0 )  =  (  .0.  .-  ( ( T `  M )  .X.  ( T `  (
b `  0 )
) ) ) )
237224, 231, 2363eqtrd 2449 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( 0 
.^  ( T `  M ) )  .X.  ( G `  0 ) )  =  (  .0.  .-  ( ( T `  M )  .X.  ( T `  ( b `  0 ) ) ) ) )
238212, 237oveq12d 6298 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( ( ( s  +  1 )  .^  ( T `  M ) )  .X.  ( G `  ( s  +  1 ) ) )  .+  ( ( 0  .^  ( T `  M ) )  .X.  ( G `  0 ) ) )  =  ( ( ( ( s  +  1 )  .^  ( T `  M ) )  .X.  ( T `  ( b `  s
) ) )  .+  (  .0.  .-  ( ( T `  M )  .X.  ( T `  (
b `  0 )
) ) ) ) )
2391, 3cmncom 17140 . . . . . . 7  |-  ( ( Y  e. CMnd  /\  (
( 0  .^  ( T `  M )
)  .X.  ( G `  0 ) )  e.  ( Base `  Y
)  /\  ( (
( s  +  1 )  .^  ( T `  M ) )  .X.  ( G `  ( s  +  1 ) ) )  e.  ( Base `  Y ) )  -> 
( ( ( 0 
.^  ( T `  M ) )  .X.  ( G `  0 ) )  .+  ( ( ( s  +  1 )  .^  ( T `  M ) )  .X.  ( G `  ( s  +  1 ) ) ) )  =  ( ( ( ( s  +  1 )  .^  ( T `  M ) )  .X.  ( G `  ( s  +  1 ) ) )  .+  ( ( 0  .^  ( T `  M ) )  .X.  ( G `  0 ) ) ) )
24013, 81, 95, 239syl3anc 1232 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( ( 0  .^  ( T `  M ) )  .X.  ( G `  0 ) )  .+  ( ( ( s  +  1 )  .^  ( T `  M ) )  .X.  ( G `  ( s  +  1 ) ) ) )  =  ( ( ( ( s  +  1 )  .^  ( T `  M ) )  .X.  ( G `  ( s  +  1 ) ) )  .+  ( ( 0  .^  ( T `  M ) )  .X.  ( G `  0 ) ) ) )
241 ringgrp 17525 . . . . . . . . 9  |-  ( Y  e.  Ring  ->  Y  e. 
Grp )
24210, 241syl 17 . . . . . . . 8  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  Y  e.  Grp )
243242adantr 465 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  Y  e.  Grp )
244212, 95eqeltrrd 2493 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( ( s  +  1 ) 
.^  ( T `  M ) )  .X.  ( T `  ( b `
 s ) ) )  e.  ( Base `  Y ) )
24510adantr 465 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  Y  e.  Ring )
246214adantr 465 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( T `  M )  e.  (
Base `  Y )
)
247 simpl1 1002 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  N  e.  Fin )
24843ad2ant2 1021 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  R  e.  Ring )
249248adantr 465 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  R  e.  Ring )
250 elmapi 7480 . . . . . . . . . . . 12  |-  ( b  e.  ( B  ^m  ( 0 ... s
) )  ->  b : ( 0 ... s ) --> B )
251250adantl 466 . . . . . . . . . . 11  |-  ( ( s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) )  -> 
b : ( 0 ... s ) --> B )
252251adantl 466 . . . . . . . . . 10  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  b : ( 0 ... s ) --> B )
253 0elfz 11830 . . . . . . . . . . . 12  |-  ( s  e.  NN0  ->  0  e.  ( 0 ... s
) )
25432, 253syl 17 . . . . . . . . . . 11  |-  ( s  e.  NN  ->  0  e.  ( 0 ... s
) )
255254ad2antrl 728 . . . . . . . . . 10  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  0  e.  ( 0 ... s ) )
256252, 255ffvelrnd 6012 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( b ` 
0 )  e.  B
)
25724, 20, 21, 7, 8mat2pmatbas 19521 . . . . . . . . 9  |-  ( ( N  e.  Fin  /\  R  e.  Ring  /\  (
b `  0 )  e.  B )  ->  ( T `  ( b `  0 ) )  e.  ( Base `  Y
) )
258247, 249, 256, 257syl3anc 1232 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( T `  ( b `  0
) )  e.  (
Base `  Y )
)
2591, 22ringcl 17534 . . . . . . . 8  |-  ( ( Y  e.  Ring  /\  ( T `  M )  e.  ( Base `  Y
)  /\  ( T `  ( b `  0
) )  e.  (
Base `  Y )
)  ->  ( ( T `  M )  .X.  ( T `  (
b `  0 )
) )  e.  (
Base `  Y )
)
260245, 246, 258, 259syl3anc 1232 . . . . . . 7  |-  ( ( ( 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 ) )
2611, 2, 23, 3grpsubadd0sub 16451 . . . . . . 7  |-  ( ( Y  e.  Grp  /\  ( ( ( s  +  1 )  .^  ( T `  M ) )  .X.  ( T `  ( b `  s
) ) )  e.  ( Base `  Y
)  /\  ( ( T `  M )  .X.  ( T `  (
b `  0 )
) )  e.  (
Base `  Y )
)  ->  ( (
( ( s  +  1 )  .^  ( T `  M )
)  .X.  ( T `  ( b `  s
) ) )  .-  ( ( T `  M )  .X.  ( T `  ( b `  0 ) ) ) )  =  ( ( ( ( s  +  1 )  .^  ( T `  M ) )  .X.  ( T `  ( b `  s
) ) )  .+  (  .0.  .-  ( ( T `  M )  .X.  ( T `  (
b `  0 )
) ) ) ) )
262243, 244, 260, 261syl3anc 1232 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( ( ( s  +  1 )  .^  ( T `  M ) )  .X.  ( T `  ( b `
 s ) ) )  .-  ( ( T `  M ) 
.X.  ( T `  ( b `  0
) ) ) )  =  ( ( ( ( s  +  1 )  .^  ( T `  M ) )  .X.  ( T `  ( b `
 s ) ) )  .+  (  .0.  .-  ( ( T `  M )  .X.  ( T `  ( b `  0 ) ) ) ) ) )
263238, 240, 2623eqtr4d 2455 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( ( 0  .^  ( T `  M ) )  .X.  ( G `  0 ) )  .+  ( ( ( s  +  1 )  .^  ( T `  M ) )  .X.  ( G `  ( s  +  1 ) ) ) )  =  ( ( ( ( s  +  1 )  .^  ( T `  M ) )  .X.  ( T `  ( b `  s
) ) )  .-  ( ( T `  M )  .X.  ( T `  ( b `  0 ) ) ) ) )
264191, 263oveq12d 6298 . . . 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  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  .+  ( ( ( 0  .^  ( T `  M )
)  .X.  ( G `  0 ) ) 
.+  ( ( ( s  +  1 ) 
.^  ( T `  M ) )  .X.  ( G `  ( s  +  1 ) ) ) ) )  =  ( ( Y  gsumg  ( i  e.  ( 1 ... s )  |->  ( ( i  .^  ( T `  M ) )  .X.  ( ( T `  ( b `  (
i  -  1 ) ) )  .-  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) ) )  .+  ( ( ( ( s  +  1 ) 
.^  ( T `  M ) )  .X.  ( T `  ( b `
 s ) ) )  .-  ( ( T `  M ) 
.X.  ( T `  ( b `  0
) ) ) ) ) )
265112, 264eqtrd 2445 . . 3  |-  ( ( ( 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  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  .+  ( ( 0  .^  ( T `  M ) )  .X.  ( G `  0 ) ) )  .+  (
( ( s  +  1 )  .^  ( T `  M )
)  .X.  ( G `  ( s  +  1 ) ) ) )  =  ( ( Y 
gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  ( T `  M ) )  .X.  ( ( T `  ( b `  ( i  -  1 ) ) )  .-  ( ( T `  M )  .X.  ( T `  ( b `  i ) ) ) ) ) ) ) 
.+  ( ( ( ( s  +  1 )  .^  ( T `  M ) )  .X.  ( T `  ( b `
 s ) ) )  .-  ( ( T `  M ) 
.X.  ( T `  ( b `  0
) ) ) ) ) )
26674, 101, 2653eqtrd 2449 . 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  +  1 ) )  |->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  =  ( ( Y  gsumg  ( i  e.  ( 1 ... s )  |->  ( ( i  .^  ( T `  M ) )  .X.  ( ( T `  ( b `  (
i  -  1 ) ) )  .-  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) ) )  .+  ( ( ( ( s  +  1 ) 
.^  ( T `  M ) )  .X.  ( T `  ( b `
 s ) ) )  .-  ( ( T `  M ) 
.X.  ( T `  ( b `  0
) ) ) ) ) )
26738, 72, 2663eqtrd 2449 1  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( i  e.  NN0  |->  ( ( i  .^  ( T `  M ) )  .X.  ( G `  i ) ) ) )  =  ( ( Y  gsumg  ( i  e.  ( 1 ... s )  |->  ( ( i  .^  ( T `  M ) )  .X.  ( ( T `  ( b `  (
i  -  1 ) ) )  .-  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) ) )  .+  ( ( ( ( s  +  1 ) 
.^  ( T `  M ) )  .X.  ( T `  ( b `
 s ) ) )  .-  ( ( T `  M ) 
.X.  ( T `  ( b `  0
) ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 186    \/ wo 368    /\ wa 369    /\ w3a 976    = wceq 1407    e. wcel 1844    =/= wne 2600   _Vcvv 3061    u. cun 3414    i^i cin 3415   (/)c0 3740   ifcif 3887   {csn 3974   class class class wbr 4397    |-> cmpt 4455   -->wf 5567   ` cfv 5571  (class class class)co 6280    ^m cmap 7459   Fincfn 7556   CCcc 9522   RRcr 9523   0cc0 9524   1c1 9525    + caddc 9527    < clt 9660    <_ cle 9661    - cmin 9843   NNcn 10578   2c2 10628   NN0cn0 10838   ZZcz 10907   ZZ>=cuz 11129   ...cfz 11728   Basecbs 14843   +g cplusg 14911   .rcmulr 14912   0gc0g 15056    gsumg cgsu 15057   Mndcmnd 16245   Grpcgrp 16379   -gcsg 16381  .gcmg 16382  CMndccmn 17124  mulGrpcmgp 17463   1rcur 17475   Ringcrg 17520   CRingccrg 17521  Poly1cpl1 18538   Mat cmat 19203   matToPolyMat cmat2pmat 19499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-8 1846  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-rep 4509  ax-sep 4519  ax-nul 4527  ax-pow<