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

Theorem chfacfscmulgsum 19961
Description: Breaking up a sum of values of the "characteristic factor function" scaled by a polynomial. (Contributed by AV, 9-Nov-2019.)
Hypotheses
Ref Expression
chfacfisf.a  |-  A  =  ( N Mat  R )
chfacfisf.b  |-  B  =  ( Base `  A
)
chfacfisf.p  |-  P  =  (Poly1 `  R )
chfacfisf.y  |-  Y  =  ( N Mat  P )
chfacfisf.r  |-  .X.  =  ( .r `  Y )
chfacfisf.s  |-  .-  =  ( -g `  Y )
chfacfisf.0  |-  .0.  =  ( 0g `  Y )
chfacfisf.t  |-  T  =  ( N matToPolyMat  R )
chfacfisf.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 ) ) ) ) ) ) ) )
chfacfscmulcl.x  |-  X  =  (var1 `  R )
chfacfscmulcl.m  |-  .x.  =  ( .s `  Y )
chfacfscmulcl.e  |-  .^  =  (.g
`  (mulGrp `  P )
)
chfacfscmulgsum.p  |-  .+  =  ( +g  `  Y )
Assertion
Ref Expression
chfacfscmulgsum  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( Y  gsumg  ( i  e.  NN0  |->  ( ( i  .^  X )  .x.  ( G `  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, n    n, M    n, N    R, n    n, Y    n, b    n, s, B    .0. , n    B, i, s    i, G   
i, M    i, N    R, i    i, X    i, Y   
.^ , i    .x. , b, i    T, n    .- , n    .X. , n    i, n
Allowed substitution hints:    A( i, n, s, b)    B( b)    P( i, n, s, b)    .+ ( i, n, s, b)    R( s, b)    T( i, s, b)    .x. ( n, s)    .X. ( i, s, b)    .^ ( n, s, b)    G( n, s, b)    M( s, b)    .- ( i,
s, b)    N( s,
b)    X( n, s, b)    Y( s, b)    .0. ( i,
s, b)

Proof of Theorem chfacfscmulgsum
StepHypRef Expression
1 eqid 2471 . . 3  |-  ( Base `  Y )  =  (
Base `  Y )
2 chfacfisf.0 . . 3  |-  .0.  =  ( 0g `  Y )
3 chfacfscmulgsum.p . . 3  |-  .+  =  ( +g  `  Y )
4 crngring 17869 . . . . . . . 8  |-  ( R  e.  CRing  ->  R  e.  Ring )
54anim2i 579 . . . . . . 7  |-  ( ( N  e.  Fin  /\  R  e.  CRing )  -> 
( N  e.  Fin  /\  R  e.  Ring )
)
653adant3 1050 . . . . . 6  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  ( N  e.  Fin  /\  R  e.  Ring ) )
7 chfacfisf.p . . . . . . 7  |-  P  =  (Poly1 `  R )
8 chfacfisf.y . . . . . . 7  |-  Y  =  ( N Mat  P )
97, 8pmatring 19794 . . . . . 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 17889 . . . . 5  |-  ( Y  e.  Ring  ->  Y  e. CMnd
)
1210, 11syl 17 . . . 4  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  Y  e. CMnd )
1312adantr 472 . . 3  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  Y  e. CMnd )
14 nn0ex 10899 . . . 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 768 . . . . 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 770 . . . . 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 468 . . . . 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 1210 . . . 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 chfacfisf.a . . . . 5  |-  A  =  ( N Mat  R )
21 chfacfisf.b . . . . 5  |-  B  =  ( Base `  A
)
22 chfacfisf.r . . . . 5  |-  .X.  =  ( .r `  Y )
23 chfacfisf.s . . . . 5  |-  .-  =  ( -g `  Y )
24 chfacfisf.t . . . . 5  |-  T  =  ( N matToPolyMat  R )
25 chfacfisf.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 chfacfscmulcl.x . . . . 5  |-  X  =  (var1 `  R )
27 chfacfscmulcl.m . . . . 5  |-  .x.  =  ( .s `  Y )
28 chfacfscmulcl.e . . . . 5  |-  .^  =  (.g
`  (mulGrp `  P )
)
2920, 21, 7, 8, 22, 23, 2, 24, 25, 26, 27, 28chfacfscmulcl 19958 . . . 4  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) )  /\  i  e.  NN0 )  -> 
( ( i  .^  X )  .x.  ( G `  i )
)  e.  ( Base `  Y ) )
3019, 29syl 17 . . 3  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  i  e.  NN0 )  ->  (
( i  .^  X
)  .x.  ( G `  i ) )  e.  ( Base `  Y
) )
3120, 21, 7, 8, 22, 23, 2, 24, 25, 26, 27, 28chfacfscmulfsupp 19960 . . 3  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( i  e. 
NN0  |->  ( ( i 
.^  X )  .x.  ( G `  i ) ) ) finSupp  .0.  )
32 nn0disj 11932 . . . 4  |-  ( ( 0 ... ( s  +  1 ) )  i^i  ( ZZ>= `  (
( s  +  1 )  +  1 ) ) )  =  (/)
3332a1i 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 ) ) )  =  (/) )
34 nnnn0 10900 . . . . . 6  |-  ( s  e.  NN  ->  s  e.  NN0 )
35 peano2nn0 10934 . . . . . 6  |-  ( s  e.  NN0  ->  ( s  +  1 )  e. 
NN0 )
3634, 35syl 17 . . . . 5  |-  ( s  e.  NN  ->  (
s  +  1 )  e.  NN0 )
37 nn0split 11931 . . . . 5  |-  ( ( s  +  1 )  e.  NN0  ->  NN0  =  ( ( 0 ... ( s  +  1 ) )  u.  ( ZZ>=
`  ( ( s  +  1 )  +  1 ) ) ) )
3836, 37syl 17 . . . 4  |-  ( s  e.  NN  ->  NN0  =  ( ( 0 ... ( s  +  1 ) )  u.  ( ZZ>=
`  ( ( s  +  1 )  +  1 ) ) ) )
3938ad2antrl 742 . . 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 ) ) ) )
401, 2, 3, 13, 15, 30, 31, 33, 39gsumsplit2 17640 . 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  .^  X )  .x.  ( G `  i
) ) ) )  =  ( ( Y 
gsumg  ( i  e.  ( 0 ... ( s  +  1 ) ) 
|->  ( ( i  .^  X )  .x.  ( G `  i )
) ) )  .+  ( Y  gsumg  ( i  e.  (
ZZ>= `  ( ( s  +  1 )  +  1 ) )  |->  ( ( i  .^  X
)  .x.  ( G `  i ) ) ) ) ) )
41 simpll 768 . . . . . . . 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
) )
42 simplr 770 . . . . . . . 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 ) ) ) )
43 nncn 10639 . . . . . . . . . . . . 13  |-  ( s  e.  NN  ->  s  e.  CC )
44 add1p1 10886 . . . . . . . . . . . . 13  |-  ( s  e.  CC  ->  (
( s  +  1 )  +  1 )  =  ( s  +  2 ) )
4543, 44syl 17 . . . . . . . . . . . 12  |-  ( s  e.  NN  ->  (
( s  +  1 )  +  1 )  =  ( s  +  2 ) )
4645ad2antrl 742 . . . . . . . . . . 11  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( s  +  1 )  +  1 )  =  ( s  +  2 ) )
4746fveq2d 5883 . . . . . . . . . 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 ) ) )
4847eleq2d 2534 . . . . . . . . 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 ) ) ) )
4948biimpa 492 . . . . . . . 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 ) ) )
5020, 21, 7, 8, 22, 23, 2, 24, 25, 26, 27, 28chfacfscmul0 19959 . . . . . . . 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  .^  X )  .x.  ( G `  i )
)  =  .0.  )
5141, 42, 49, 50syl3anc 1292 . . . . . . 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  .^  X )  .x.  ( G `  i
) )  =  .0.  )
5251mpteq2dva 4482 . . . . . 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  .^  X )  .x.  ( G `  i )
) )  =  ( i  e.  ( ZZ>= `  ( ( s  +  1 )  +  1 ) )  |->  .0.  )
)
5352oveq2d 6324 . . . . 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 
.^  X )  .x.  ( G `  i ) ) ) )  =  ( Y  gsumg  ( i  e.  (
ZZ>= `  ( ( s  +  1 )  +  1 ) )  |->  .0.  ) ) )
544, 9sylan2 482 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  R  e.  CRing )  ->  Y  e.  Ring )
55 ringmnd 17867 . . . . . . . . . 10  |-  ( Y  e.  Ring  ->  Y  e. 
Mnd )
5654, 55syl 17 . . . . . . . . 9  |-  ( ( N  e.  Fin  /\  R  e.  CRing )  ->  Y  e.  Mnd )
57563adant3 1050 . . . . . . . 8  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  Y  e.  Mnd )
58 fvex 5889 . . . . . . . 8  |-  ( ZZ>= `  ( ( s  +  1 )  +  1 ) )  e.  _V
5957, 58jctir 547 . . . . . . 7  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  ( Y  e.  Mnd  /\  ( ZZ>=
`  ( ( s  +  1 )  +  1 ) )  e. 
_V ) )
6059adantr 472 . . . . . 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 ) )
612gsumz 16699 . . . . . 6  |-  ( ( Y  e.  Mnd  /\  ( ZZ>= `  ( (
s  +  1 )  +  1 ) )  e.  _V )  -> 
( Y  gsumg  ( i  e.  (
ZZ>= `  ( ( s  +  1 )  +  1 ) )  |->  .0.  ) )  =  .0.  )
6260, 61syl 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.  )
6353, 62eqtrd 2505 . . . 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 
.^  X )  .x.  ( G `  i ) ) ) )  =  .0.  )
6463oveq2d 6324 . . 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  .^  X )  .x.  ( G `  i )
) ) )  .+  ( Y  gsumg  ( i  e.  (
ZZ>= `  ( ( s  +  1 )  +  1 ) )  |->  ( ( i  .^  X
)  .x.  ( G `  i ) ) ) ) )  =  ( ( Y  gsumg  ( i  e.  ( 0 ... ( s  +  1 ) ) 
|->  ( ( i  .^  X )  .x.  ( G `  i )
) ) )  .+  .0.  ) )
6557adantr 472 . . . 4  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  Y  e.  Mnd )
66 fzfid 12224 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( 0 ... ( s  +  1 ) )  e.  Fin )
67 elfznn0 11913 . . . . . . . 8  |-  ( i  e.  ( 0 ... ( s  +  1 ) )  ->  i  e.  NN0 )
6867, 19sylan2 482 . . . . . . 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 ) )
6968, 29syl 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  .^  X
)  .x.  ( G `  i ) )  e.  ( Base `  Y
) )
7069ralrimiva 2809 . . . . 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  .^  X )  .x.  ( G `  i )
)  e.  ( Base `  Y ) )
711, 13, 66, 70gsummptcl 17677 . . . 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  .^  X )  .x.  ( G `  i
) ) ) )  e.  ( Base `  Y
) )
721, 3, 2mndrid 16636 . . . 4  |-  ( ( Y  e.  Mnd  /\  ( Y  gsumg  ( i  e.  ( 0 ... ( s  +  1 ) ) 
|->  ( ( i  .^  X )  .x.  ( G `  i )
) ) )  e.  ( Base `  Y
) )  ->  (
( Y  gsumg  ( i  e.  ( 0 ... ( s  +  1 ) ) 
|->  ( ( i  .^  X )  .x.  ( G `  i )
) ) )  .+  .0.  )  =  ( Y  gsumg  ( i  e.  ( 0 ... ( s  +  1 ) ) 
|->  ( ( i  .^  X )  .x.  ( G `  i )
) ) ) )
7365, 71, 72syl2anc 673 . . 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  .^  X )  .x.  ( G `  i )
) ) )  .+  .0.  )  =  ( Y  gsumg  ( i  e.  ( 0 ... ( s  +  1 ) ) 
|->  ( ( i  .^  X )  .x.  ( G `  i )
) ) ) )
7464, 73eqtrd 2505 . 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  .^  X )  .x.  ( G `  i )
) ) )  .+  ( Y  gsumg  ( i  e.  (
ZZ>= `  ( ( s  +  1 )  +  1 ) )  |->  ( ( i  .^  X
)  .x.  ( G `  i ) ) ) ) )  =  ( Y  gsumg  ( i  e.  ( 0 ... ( s  +  1 ) ) 
|->  ( ( i  .^  X )  .x.  ( G `  i )
) ) ) )
7534ad2antrl 742 . . . 4  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  s  e.  NN0 )
761, 3, 13, 75, 69gsummptfzsplit 17643 . . 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  .^  X )  .x.  ( G `  i
) ) ) )  =  ( ( Y 
gsumg  ( i  e.  ( 0 ... s ) 
|->  ( ( i  .^  X )  .x.  ( G `  i )
) ) )  .+  ( Y  gsumg  ( i  e.  {
( s  +  1 ) }  |->  ( ( i  .^  X )  .x.  ( G `  i
) ) ) ) ) )
77 elfznn0 11913 . . . . . . 7  |-  ( i  e.  ( 0 ... s )  ->  i  e.  NN0 )
7877, 30sylan2 482 . . . . . 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
)  .x.  ( G `  i ) )  e.  ( Base `  Y
) )
791, 3, 13, 75, 78gsummptfzsplitl 17644 . . . . 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  .^  X )  .x.  ( G `  i
) ) ) )  =  ( ( Y 
gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  X )  .x.  ( G `  i )
) ) )  .+  ( Y  gsumg  ( i  e.  {
0 }  |->  ( ( i  .^  X )  .x.  ( G `  i
) ) ) ) ) )
80 0nn0 10908 . . . . . . . 8  |-  0  e.  NN0
8180a1i 11 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  0  e.  NN0 )
8220, 21, 7, 8, 22, 23, 2, 24, 25, 26, 27, 28chfacfscmulcl 19958 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) )  /\  0  e.  NN0 )  -> 
( ( 0  .^  X )  .x.  ( G `  0 )
)  e.  ( Base `  Y ) )
8381, 82mpd3an3 1391 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( 0 
.^  X )  .x.  ( G `  0 ) )  e.  ( Base `  Y ) )
84 oveq1 6315 . . . . . . . . 9  |-  ( i  =  0  ->  (
i  .^  X )  =  ( 0  .^  X ) )
85 fveq2 5879 . . . . . . . . 9  |-  ( i  =  0  ->  ( G `  i )  =  ( G ` 
0 ) )
8684, 85oveq12d 6326 . . . . . . . 8  |-  ( i  =  0  ->  (
( i  .^  X
)  .x.  ( G `  i ) )  =  ( ( 0  .^  X )  .x.  ( G `  0 )
) )
871, 86gsumsn 17665 . . . . . . 7  |-  ( ( Y  e.  Mnd  /\  0  e.  NN0  /\  (
( 0  .^  X
)  .x.  ( G `  0 ) )  e.  ( Base `  Y
) )  ->  ( Y  gsumg  ( i  e.  {
0 }  |->  ( ( i  .^  X )  .x.  ( G `  i
) ) ) )  =  ( ( 0 
.^  X )  .x.  ( G `  0 ) ) )
8865, 81, 83, 87syl3anc 1292 . . . . . 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.  ( G `  i )
) ) )  =  ( ( 0  .^  X )  .x.  ( G `  0 )
) )
8988oveq2d 6324 . . . . 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  .^  X )  .x.  ( G `  i )
) ) )  .+  ( Y  gsumg  ( i  e.  {
0 }  |->  ( ( i  .^  X )  .x.  ( G `  i
) ) ) ) )  =  ( ( Y  gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  X )  .x.  ( G `  i )
) ) )  .+  ( ( 0  .^  X )  .x.  ( G `  0 )
) ) )
9079, 89eqtrd 2505 . . . 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.  ( G `  i
) ) ) )  =  ( ( Y 
gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  X )  .x.  ( G `  i )
) ) )  .+  ( ( 0  .^  X )  .x.  ( G `  0 )
) ) )
91 ovex 6336 . . . . . 6  |-  ( s  +  1 )  e. 
_V
9291a1i 11 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( s  +  1 )  e.  _V )
93 1nn0 10909 . . . . . . . 8  |-  1  e.  NN0
9493a1i 11 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  1  e.  NN0 )
9575, 94nn0addcld 10953 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( s  +  1 )  e.  NN0 )
9620, 21, 7, 8, 22, 23, 2, 24, 25, 26, 27, 28chfacfscmulcl 19958 . . . . . 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 )  .^  X )  .x.  ( G `  ( s  +  1 ) ) )  e.  ( Base `  Y ) )
9795, 96mpd3an3 1391 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( ( s  +  1 ) 
.^  X )  .x.  ( G `  ( s  +  1 ) ) )  e.  ( Base `  Y ) )
98 oveq1 6315 . . . . . . 7  |-  ( i  =  ( s  +  1 )  ->  (
i  .^  X )  =  ( ( s  +  1 )  .^  X ) )
99 fveq2 5879 . . . . . . 7  |-  ( i  =  ( s  +  1 )  ->  ( G `  i )  =  ( G `  ( s  +  1 ) ) )
10098, 99oveq12d 6326 . . . . . 6  |-  ( i  =  ( s  +  1 )  ->  (
( i  .^  X
)  .x.  ( G `  i ) )  =  ( ( ( s  +  1 )  .^  X )  .x.  ( G `  ( s  +  1 ) ) ) )
1011, 100gsumsn 17665 . . . . 5  |-  ( ( Y  e.  Mnd  /\  ( s  +  1 )  e.  _V  /\  ( ( ( s  +  1 )  .^  X )  .x.  ( G `  ( s  +  1 ) ) )  e.  ( Base `  Y ) )  -> 
( Y  gsumg  ( i  e.  {
( s  +  1 ) }  |->  ( ( i  .^  X )  .x.  ( G `  i
) ) ) )  =  ( ( ( s  +  1 ) 
.^  X )  .x.  ( G `  ( s  +  1 ) ) ) )
10265, 92, 97, 101syl3anc 1292 . . . 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  .^  X )  .x.  ( G `  i )
) ) )  =  ( ( ( s  +  1 )  .^  X )  .x.  ( G `  ( s  +  1 ) ) ) )
10390, 102oveq12d 6326 . . 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.  ( G `  i )
) ) )  .+  ( Y  gsumg  ( i  e.  {
( s  +  1 ) }  |->  ( ( i  .^  X )  .x.  ( G `  i
) ) ) ) )  =  ( ( ( Y  gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  X )  .x.  ( G `  i )
) ) )  .+  ( ( 0  .^  X )  .x.  ( G `  0 )
) )  .+  (
( ( s  +  1 )  .^  X
)  .x.  ( G `  ( s  +  1 ) ) ) ) )
104 fzfid 12224 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( 1 ... s )  e.  Fin )
105 simpll 768 . . . . . . . 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 ) )
106 simplr 770 . . . . . . . 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
) ) ) )
107 elfznn 11854 . . . . . . . . . 10  |-  ( i  e.  ( 1 ... s )  ->  i  e.  NN )
108107nnnn0d 10949 . . . . . . . . 9  |-  ( i  e.  ( 1 ... s )  ->  i  e.  NN0 )
109108adantl 473 . . . . . . . 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 )
110105, 106, 109, 29syl3anc 1292 . . . . . . 7  |-  ( ( ( ( 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.  ( G `  i ) )  e.  ( Base `  Y
) )
111110ralrimiva 2809 . . . . . 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  .^  X )  .x.  ( G `  i )
)  e.  ( Base `  Y ) )
1121, 13, 104, 111gsummptcl 17677 . . . . 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  .^  X )  .x.  ( G `  i
) ) ) )  e.  ( Base `  Y
) )
1131, 3mndass 16624 . . . . 5  |-  ( ( Y  e.  Mnd  /\  ( ( Y  gsumg  ( i  e.  ( 1 ... s )  |->  ( ( i  .^  X )  .x.  ( G `  i
) ) ) )  e.  ( Base `  Y
)  /\  ( (
0  .^  X )  .x.  ( G `  0
) )  e.  (
Base `  Y )  /\  ( ( ( s  +  1 )  .^  X )  .x.  ( G `  ( s  +  1 ) ) )  e.  ( Base `  Y ) ) )  ->  ( ( ( Y  gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  X )  .x.  ( G `  i )
) ) )  .+  ( ( 0  .^  X )  .x.  ( G `  0 )
) )  .+  (
( ( s  +  1 )  .^  X
)  .x.  ( G `  ( s  +  1 ) ) ) )  =  ( ( Y 
gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  X )  .x.  ( G `  i )
) ) )  .+  ( ( ( 0 
.^  X )  .x.  ( G `  0 ) )  .+  ( ( ( s  +  1 )  .^  X )  .x.  ( G `  (
s  +  1 ) ) ) ) ) )
11465, 112, 83, 97, 113syl13anc 1294 . . . 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.  ( G `  i )
) ) )  .+  ( ( 0  .^  X )  .x.  ( G `  0 )
) )  .+  (
( ( s  +  1 )  .^  X
)  .x.  ( G `  ( s  +  1 ) ) ) )  =  ( ( Y 
gsumg  ( i  e.  ( 1 ... s ) 
|->  ( ( i  .^  X )  .x.  ( G `  i )
) ) )  .+  ( ( ( 0 
.^  X )  .x.  ( G `  0 ) )  .+  ( ( ( s  +  1 )  .^  X )  .x.  ( G `  (
s  +  1 ) ) ) ) ) )
11525a1i 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
) ) ) ) ) ) ) ) )
116107nnne0d 10676 . . . . . . . . . . . . . 14  |-  ( i  e.  ( 1 ... s )  ->  i  =/=  0 )
117116ad2antlr 741 . . . . . . . . . . . . 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 )
118 neeq1 2705 . . . . . . . . . . . . . 14  |-  ( n  =  i  ->  (
n  =/=  0  <->  i  =/=  0 ) )
119118adantl 473 . . . . . . . . . . . . 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 ) )
120117, 119mpbird 240 . . . . . . . . . . . 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 )
121 eqneqall 2654 . . . . . . . . . . . 12  |-  ( n  =  0  ->  (
n  =/=  0  ->  .0.  =  ( T `  ( b `  (
i  -  1 ) ) ) ) )
122120, 121mpan9 477 . . . . . . . . . . 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 ) ) ) )
123 simplr 770 . . . . . . . . . . . . . . 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 )
124 eqeq1 2475 . . . . . . . . . . . . . . . . 17  |-  ( 0  =  n  ->  (
0  =  i  <->  n  =  i ) )
125124eqcoms 2479 . . . . . . . . . . . . . . . 16  |-  ( n  =  0  ->  (
0  =  i  <->  n  =  i ) )
126125adantl 473 . . . . . . . . . . . . . . 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 ) )
127123, 126mpbird 240 . . . . . . . . . . . . . 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 )
128127fveq2d 5883 . . . . . . . . . . . . 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 ) )
129128fveq2d 5883 . . . . . . . . . . . 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 ) ) )
130129oveq2d 6324 . . . . . . . . . . 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
) ) ) )
131122, 130oveq12d 6326 . . . . . . . . . 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 ) ) ) ) )
132 elfz2 11817 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... s )  <->  ( (
1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  /\  (
1  <_  i  /\  i  <_  s ) ) )
133 zleltp1 11011 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( i  e.  ZZ  /\  s  e.  ZZ )  ->  ( i  <_  s  <->  i  <  ( s  +  1 ) ) )
134133ancoms 460 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  e.  ZZ  /\  i  e.  ZZ )  ->  ( i  <_  s  <->  i  <  ( s  +  1 ) ) )
1351343adant1 1048 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  ->  (
i  <_  s  <->  i  <  ( s  +  1 ) ) )
136135biimpcd 232 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  <_  s  ->  (
( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  ->  i  <  ( s  +  1 ) ) )
137136adantl 473 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  <_  i  /\  i  <_  s )  -> 
( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  ->  i  <  ( s  +  1 ) ) )
138137impcom 437 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  /\  ( 1  <_  i  /\  i  <_  s ) )  ->  i  <  ( s  +  1 ) )
139138orcd 399 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  /\  ( 1  <_  i  /\  i  <_  s ) )  ->  ( i  <  ( s  +  1 )  \/  ( s  +  1 )  < 
i ) )
140 zre 10965 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ZZ  ->  s  e.  RR )
141 1red 9676 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ZZ  ->  1  e.  RR )
142140, 141readdcld 9688 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s  e.  ZZ  ->  (
s  +  1 )  e.  RR )
143 zre 10965 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  e.  ZZ  ->  i  e.  RR )
144142, 143anim12ci 577 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( s  e.  ZZ  /\  i  e.  ZZ )  ->  ( i  e.  RR  /\  ( s  +  1 )  e.  RR ) )
1451443adant1 1048 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  ->  (
i  e.  RR  /\  ( s  +  1 )  e.  RR ) )
146 lttri2 9734 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i  e.  RR  /\  ( s  +  1 )  e.  RR )  ->  ( i  =/=  ( s  +  1 )  <->  ( i  < 
( s  +  1 )  \/  ( s  +  1 )  < 
i ) ) )
147145, 146syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  ->  (
i  =/=  ( s  +  1 )  <->  ( i  <  ( s  +  1 )  \/  ( s  +  1 )  < 
i ) ) )
148147adantr 472 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  /\  ( 1  <_  i  /\  i  <_  s ) )  ->  ( i  =/=  ( s  +  1 )  <->  ( i  < 
( s  +  1 )  \/  ( s  +  1 )  < 
i ) ) )
149139, 148mpbird 240 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  /\  ( 1  <_  i  /\  i  <_  s ) )  ->  i  =/=  ( s  +  1 ) )
150132, 149sylbi 200 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 1 ... s )  ->  i  =/=  ( s  +  1 ) )
151150ad2antlr 741 . . . . . . . . . . . . . . . 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 ) )
152 neeq1 2705 . . . . . . . . . . . . . . . . 17  |-  ( n  =  i  ->  (
n  =/=  ( s  +  1 )  <->  i  =/=  ( s  +  1 ) ) )
153152adantl 473 . . . . . . . . . . . . . . . 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 ) ) )
154151, 153mpbird 240 . . . . . . . . . . . . . . 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 ) )
155154adantr 472 . . . . . . . . . . . . . 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 ) )
156155neneqd 2648 . . . . . . . . . . . . 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 ) )
157156pm2.21d 109 . . . . . . . . . . . 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
) ) ) ) ) )
158157imp 436 . . . . . . . . . . 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
) ) ) ) )
159107nnred 10646 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 1 ... s )  ->  i  e.  RR )
160 eleq1 2537 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  i  ->  (
n  e.  RR  <->  i  e.  RR ) )
161159, 160syl5ibrcom 230 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... s )  ->  (
n  =  i  ->  n  e.  RR )
)
162161adantl 473 . . . . . . . . . . . . . . . . 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 )
)
163162imp 436 . . . . . . . . . . . . . . . 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 )
16475nn0red 10950 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  s  e.  RR )
165164ad2antrr 740 . . . . . . . . . . . . . . . . 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 )
166 1red 9676 . . . . . . . . . . . . . . . . 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 )
167165, 166readdcld 9688 . . . . . . . . . . . . . . . 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 )
168132, 138sylbi 200 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... s )  ->  i  <  ( s  +  1 ) )
169168ad2antlr 741 . . . . . . . . . . . . . . . . 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 ) )
170 breq1 4398 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  i  ->  (
n  <  ( s  +  1 )  <->  i  <  ( s  +  1 ) ) )
171170adantl 473 . . . . . . . . . . . . . . . . 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 ) ) )
172169, 171mpbird 240 . . . . . . . . . . . . . . . 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 ) )
173163, 167, 172ltnsymd 9801 . . . . . . . . . . . . . . 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 )
174173pm2.21d 109 . . . . . . . . . . . . . 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 ) ) ) ) ) )
175174ad2antrr 740 . . . . . . . . . . . . 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 ) ) ) ) ) )
176175imp 436 . . . . . . . . . . . 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
) ) ) ) )
177 simp-4r 785 . . . . . . . . . . . . . . . 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 )
178177oveq1d 6323 . . . . . . . . . . . . . . 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 ) )
179178fveq2d 5883 . . . . . . . . . . . . . 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 ) ) )
180179fveq2d 5883 . . . . . . . . . . . . 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 ) ) ) )
181177fveq2d 5883 . . . . . . . . . . . . . . 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 ) )
182181fveq2d 5883 . . . . . . . . . . . . . 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 ) ) )
183182oveq2d 6324 . . . . . . . . . . . . 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
) ) ) )
184180, 183oveq12d 6326 . . . . . . . . . . . 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 ) ) ) ) )
185176, 184ifeqda 3905 . . . . . . . . . . 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
) ) ) ) )
186158, 185ifeqda 3905 . . . . . . . . . 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
) ) ) ) )
187131, 186ifeqda 3905 . . . . . . . . 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
) ) ) ) )
188 ovex 6336 . . . . . . . . . 10  |-  ( ( T `  ( b `
 ( i  - 
1 ) ) ) 
.-  ( ( T `
 M )  .X.  ( T `  ( b `
 i ) ) ) )  e.  _V
189188a1i 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 )
190115, 187, 109, 189fvmptd 5969 . . . . . . . 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 ) ) ) ) )
191190oveq2d 6324 . . . . . . 7  |-  ( ( ( ( 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.  ( G `  i ) )  =  ( ( i  .^  X )  .x.  (
( T `  (
b `  ( i  -  1 ) ) )  .-  ( ( T `  M ) 
.X.  ( T `  ( b `  i
) ) ) ) ) )
192191mpteq2dva 4482 . . . . . 6  |-  ( ( ( 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.  ( G `  i ) ) )  =  ( i  e.  ( 1 ... s )  |->  ( ( i  .^  X
)  .x.  ( ( T `  ( b `  ( i  -  1 ) ) )  .-  ( ( T `  M )  .X.  ( T `  ( b `  i ) ) ) ) ) ) )
193192oveq2d 6324 . . . . 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  .^  X )  .x.  ( G `  i
) ) ) )  =  ( Y  gsumg  ( i  e.  ( 1 ... s )  |->  ( ( i  .^  X )  .x.  ( ( T `  ( b `  (
i  -  1 ) ) )  .-  (
( T `  M
)  .X.  ( T `  ( b `  i
) ) ) ) ) ) ) )
19425a1i 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
) ) ) ) ) ) ) ) )
195 nn0p1gt0 10923 . . . . . . . . . . . . . . 15  |-  ( s  e.  NN0  ->  0  < 
( s  +  1 ) )
196 0red 9662 . . . . . . . . . . . . . . . . 17  |-  ( s  e.  NN0  ->  0  e.  RR )
197 ltne 9748 . . . . . . . . . . . . . . . . 17  |-  ( ( 0  e.  RR  /\  0  <  ( s  +  1 ) )  -> 
( s  +  1 )  =/=  0 )
198196, 197sylan 479 . . . . . . . . . . . . . . . 16  |-  ( ( s  e.  NN0  /\  0  <  ( s  +  1 ) )  -> 
( s  +  1 )  =/=  0 )
199 neeq1 2705 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( s  +  1 )  ->  (
n  =/=  0  <->  (
s  +  1 )  =/=  0 ) )
200198, 199syl5ibrcom 230 . . . . . . . . . . . . . . 15  |-  ( ( s  e.  NN0  /\  0  <  ( s  +  1 ) )  -> 
( n  =  ( s  +  1 )  ->  n  =/=  0
) )
201195, 200mpdan 681 . . . . . . . . . . . . . 14  |-  ( s  e.  NN0  ->  ( n  =  ( s  +  1 )  ->  n  =/=  0 ) )
20234, 201syl 17 . . . . . . . . . . . . 13  |-  ( s  e.  NN  ->  (
n  =  ( s  +  1 )  ->  n  =/=  0 ) )
203202ad2antrl 742 . . . . . . . . . . . 12  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( n  =  ( s  +  1 )  ->  n  =/=  0 ) )
204203imp 436 . . . . . . . . . . 11  |-  ( ( ( ( N  e. 
Fin  /\  R  e.  CRing  /\  M  e.  B
)  /\  ( s  e.  NN  /\  b  e.  ( B  ^m  (
0 ... s ) ) ) )  /\  n  =  ( s  +  1 ) )  ->  n  =/=  0 )
205 eqneqall 2654 . . . . . . . . . . 11  |-  ( n  =  0  ->  (
n  =/=  0  -> 
(  .0.  .-  (
( T `  M
)  .X.  ( T `  ( b `  0
) ) ) )  =  ( T `  ( b `  s
) ) ) )
206204, 205mpan9 477 . . . . . . . . . 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 ) ) )
207 iftrue 3878 . . . . . . . . . . 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
) ) )
208207ad2antlr 741 . . . . . . . . . 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
) ) )
209206, 208ifeqda 3905 . . . . . . . . 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 ) ) )
21075, 35syl 17 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( s  +  1 )  e.  NN0 )
211 fvex 5889 . . . . . . . . . 10  |-  ( T `
 ( b `  s ) )  e. 
_V
212211a1i 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 )
213194, 209, 210, 212fvmptd 5969 . . . . . . . 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 ) ) )
214213oveq2d 6324 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( ( s  +  1 ) 
.^  X )  .x.  ( G `  ( s  +  1 ) ) )  =  ( ( ( s  +  1 )  .^  X )  .x.  ( T `  (
b `  s )
) ) )
21543ad2ant2 1052 . . . . . . . . . . . . 13  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  R  e.  Ring )
216 eqid 2471 . . . . . . . . . . . . . 14  |-  ( Base `  P )  =  (
Base `  P )
21726, 7, 216vr1cl 18887 . . . . . . . . . . . . 13  |-  ( R  e.  Ring  ->  X  e.  ( Base `  P
) )
218215, 217syl 17 . . . . . . . . . . . 12  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  X  e.  ( Base `  P
) )
219 eqid 2471 . . . . . . . . . . . . . 14  |-  (mulGrp `  P )  =  (mulGrp `  P )
220219, 216mgpbas 17807 . . . . . . . . . . . . 13  |-  ( Base `  P )  =  (
Base `  (mulGrp `  P
) )
221 eqid 2471 . . . . . . . . . . . . . 14  |-  ( 1r
`  P )  =  ( 1r `  P
)
222219, 221ringidval 17815 . . . . . . . . . . . . 13  |-  ( 1r
`  P )  =  ( 0g `  (mulGrp `  P ) )
223220, 222, 28mulg0 16841 . . . . . . . . . . . 12  |-  ( X  e.  ( Base `  P
)  ->  ( 0 
.^  X )  =  ( 1r `  P
) )
224218, 223syl 17 . . . . . . . . . . 11  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  (
0  .^  X )  =  ( 1r `  P ) )
2257ply1crng 18868 . . . . . . . . . . . . . . 15  |-  ( R  e.  CRing  ->  P  e.  CRing
)
226225anim2i 579 . . . . . . . . . . . . . 14  |-  ( ( N  e.  Fin  /\  R  e.  CRing )  -> 
( N  e.  Fin  /\  P  e.  CRing ) )
2272263adant3 1050 . . . . . . . . . . . . 13  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  ( N  e.  Fin  /\  P  e.  CRing ) )
2288matsca2 19522 . . . . . . . . . . . . 13  |-  ( ( N  e.  Fin  /\  P  e.  CRing )  ->  P  =  (Scalar `  Y
) )
229227, 228syl 17 . . . . . . . . . . . 12  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  P  =  (Scalar `  Y )
)
230229fveq2d 5883 . . . . . . . . . . 11  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  ( 1r `  P )  =  ( 1r `  (Scalar `  Y ) ) )
231224, 230eqtrd 2505 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  (
0  .^  X )  =  ( 1r `  (Scalar `  Y ) ) )
232231adantr 472 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( 0  .^  X )  =  ( 1r `  (Scalar `  Y ) ) )
233232oveq1d 6323 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( 0 
.^  X )  .x.  ( G `  0 ) )  =  ( ( 1r `  (Scalar `  Y ) )  .x.  ( G `  0 ) ) )
2347, 8pmatlmod 19795 . . . . . . . . . . . 12  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  Y  e.  LMod )
2354, 234sylan2 482 . . . . . . . . . . 11  |-  ( ( N  e.  Fin  /\  R  e.  CRing )  ->  Y  e.  LMod )
2362353adant3 1050 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  Y  e.  LMod )
237236adantr 472 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  Y  e.  LMod )
23820, 21, 7, 8, 22, 23, 2, 24, 25chfacfisf 19955 . . . . . . . . . . 11  |-  ( ( ( N  e.  Fin  /\  R  e.  Ring  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  G : NN0 --> (
Base `  Y )
)
2394, 238syl3anl2 1341 . . . . . . . . . 10  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  G : NN0 --> (
Base `  Y )
)
240239, 81ffvelrnd 6038 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( G ` 
0 )  e.  (
Base `  Y )
)
241 eqid 2471 . . . . . . . . . 10  |-  (Scalar `  Y )  =  (Scalar `  Y )
242 eqid 2471 . . . . . . . . . 10  |-  ( 1r
`  (Scalar `  Y )
)  =  ( 1r
`  (Scalar `  Y )
)
2431, 241, 27, 242lmodvs1 18197 . . . . . . . . 9  |-  ( ( Y  e.  LMod  /\  ( G `  0 )  e.  ( Base `  Y
) )  ->  (
( 1r `  (Scalar `  Y ) )  .x.  ( G `  0 ) )  =  ( G `
 0 ) )
244237, 240, 243syl2anc 673 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( 1r
`  (Scalar `  Y )
)  .x.  ( G `  0 ) )  =  ( G ` 
0 ) )
245 iftrue 3878 . . . . . . . . . 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
) ) ) ) )
246245adantl 473 . . . . . . . . 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 ) ) ) ) )
247 ovex 6336 . . . . . . . . . 10  |-  (  .0.  .-  ( ( T `  M )  .X.  ( T `  ( b `  0 ) ) ) )  e.  _V
248247a1i 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 )
249194, 246, 81, 248fvmptd 5969 . . . . . . . 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 )
) ) ) )
250233, 244, 2493eqtrd 2509 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( 0 
.^  X )  .x.  ( G `  0 ) )  =  (  .0.  .-  ( ( T `  M )  .X.  ( T `  ( b `  0 ) ) ) ) )
251214, 250oveq12d 6326 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( ( ( s  +  1 )  .^  X )  .x.  ( G `  (
s  +  1 ) ) )  .+  (
( 0  .^  X
)  .x.  ( G `  0 ) ) )  =  ( ( ( ( s  +  1 )  .^  X
)  .x.  ( T `  ( b `  s
) ) )  .+  (  .0.  .-  ( ( T `  M )  .X.  ( T `  (
b `  0 )
) ) ) ) )
2521, 3cmncom 17524 . . . . . . 7  |-  ( ( Y  e. CMnd  /\  (
( 0  .^  X
)  .x.  ( G `  0 ) )  e.  ( Base `  Y
)  /\  ( (
( s  +  1 )  .^  X )  .x.  ( G `  (
s  +  1 ) ) )  e.  (
Base `  Y )
)  ->  ( (
( 0  .^  X
)  .x.  ( G `  0 ) ) 
.+  ( ( ( s  +  1 ) 
.^  X )  .x.  ( G `  ( s  +  1 ) ) ) )  =  ( ( ( ( s  +  1 )  .^  X )  .x.  ( G `  ( s  +  1 ) ) )  .+  ( ( 0  .^  X )  .x.  ( G `  0
) ) ) )
25313, 83, 97, 252syl3anc 1292 . . . . . 6  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( ( 0  .^  X )  .x.  ( G `  0
) )  .+  (
( ( s  +  1 )  .^  X
)  .x.  ( G `  ( s  +  1 ) ) ) )  =  ( ( ( ( s  +  1 )  .^  X )  .x.  ( G `  (
s  +  1 ) ) )  .+  (
( 0  .^  X
)  .x.  ( G `  0 ) ) ) )
254 ringgrp 17863 . . . . . . . . 9  |-  ( Y  e.  Ring  ->  Y  e. 
Grp )
25510, 254syl 17 . . . . . . . 8  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  Y  e.  Grp )
256255adantr 472 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  Y  e.  Grp )
257214, 97eqeltrrd 2550 . . . . . . 7  |-  ( ( ( 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 ) )
25810adantr 472 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  Y  e.  Ring )
25924, 20, 21, 7, 8mat2pmatbas 19827 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  R  e.  Ring  /\  M  e.  B )  ->  ( T `  M )  e.  ( Base `  Y
) )
2604, 259syl3an2 1326 . . . . . . . . 9  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  ( T `  M )  e.  ( Base `  Y
) )
261260adantr 472 . . . . . . . 8  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( T `  M )  e.  (
Base `  Y )
)
262 simpl1 1033 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  N  e.  Fin )
263215adantr 472 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  R  e.  Ring )
264 elmapi 7511 . . . . . . . . . . . 12  |-  ( b  e.  ( B  ^m  ( 0 ... s
) )  ->  b : ( 0 ... s ) --> B )
265264adantl 473 . . . . . . . . . . 11  |-  ( ( s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) )  -> 
b : ( 0 ... s ) --> B )
266265adantl 473 . . . . . . . . . 10  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  b : ( 0 ... s ) --> B )
267 0elfz 11915 . . . . . . . . . . . 12  |-  ( s  e.  NN0  ->  0  e.  ( 0 ... s
) )
26834, 267syl 17 . . . . . . . . . . 11  |-  ( s  e.  NN  ->  0  e.  ( 0 ... s
) )
269268ad2antrl 742 . . . . . . . . . 10  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  0  e.  ( 0 ... s ) )
270266, 269ffvelrnd 6038 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( b ` 
0 )  e.  B
)
27124, 20, 21, 7, 8mat2pmatbas 19827 . . . . . . . . 9  |-  ( ( N  e.  Fin  /\  R  e.  Ring  /\  (
b `  0 )  e.  B )  ->  ( T `  ( b `  0 ) )  e.  ( Base `  Y
) )
272262, 263, 270, 271syl3anc 1292 . . . . . . . 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 )
)
2731, 22ringcl 17872 . . . . . . . 8  |-  ( ( Y  e.  Ring  /\  ( T `  M )  e.  ( Base `  Y
)  /\  ( T `  ( b `  0
) )  e.  (
Base `  Y )
)  ->  ( ( T `  M )  .X.  ( T `  (
b `  0 )
) )  e.  (
Base `  Y )
)
274258, 261, 272, 273syl3anc 1292 . . . . . . 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 ) )
2751, 2, 23, 3grpsubadd0sub 16819 . . . . . . 7  |-  ( ( Y  e.  Grp  /\  ( ( ( s  +  1 )  .^  X )  .x.  ( T `  ( b `  s ) ) )  e.  ( Base `  Y
)  /\  ( ( T `  M )  .X.  ( T `  (
b `  0 )
) )  e.  (
Base `  Y )
)  ->  ( (
( ( s  +  1 )  .^  X
)  .x.  ( T `  ( b `  s
) ) )  .-  ( ( T `  M )  .X.  ( T `  ( b `  0 ) ) ) )  =  ( ( ( ( s  +  1 )  .^  X )  .x.  ( T `  ( b `  s ) ) ) 
.+  (  .0.  .-  ( ( T `  M )  .X.  ( T `  ( b `  0 ) ) ) ) ) )
276256, 257, 274, 275syl3anc 1292 . . . . . 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 )
) )  .-  (
( T `  M
)  .X.  ( T `  ( b `  0
) ) ) )  =  ( ( ( ( s  +  1 )  .^  X )  .x.  ( T `  (
b `  s )
) )  .+  (  .0.  .-  ( ( T `
 M )  .X.  ( T `  ( b `
 0 ) ) ) ) ) )
277251, 253, 2763eqtr4d 2515 . . . . 5  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  ( ( ( 0  .^  X )  .x.  ( G `  0
) )  .+  (
( ( s  +  1 )  .^  X
)  .x.  ( G `  ( s  +  1 ) ) ) )  =  ( ( ( ( s  +  1 )  .^  X )  .x.  ( T `  (
b `  s )
) )  .-  (
( T `  M
)  .X.  ( T `  ( b `  0
) ) ) ) )
278193, 277oveq12d 6326 . . . 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.  ( G `  i )
) ) )  .+  ( ( ( 0 
.^  X )  .x.  ( G `  0 ) )  .+  ( ( ( s  +  1 )  .^  X )  .x.  ( G `  (
s  +  1 ) ) ) ) )  =  ( ( 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
) ) ) ) ) )
279114, 278eqtrd 2505 . . 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  .^  X )  .x.  ( G `  i )
) ) )  .+  ( ( 0  .^  X )  .x.  ( G `  0 )
) )  .+  (
( ( s  +  1 )  .^  X
)  .x.  ( G `  ( s  +  1 ) ) ) )  =  ( ( 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
) ) ) ) ) )
28076, 103, 2793eqtrd 2509 . 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  .^  X )  .x.  ( G `  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
) ) ) ) ) )
28140, 74, 2803eqtrd 2509 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  .^  X )  .x.  ( G `  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
) ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    \/ wo 375    /\ wa 376    /\ w3a 1007    = wceq 1452    e. wcel 1904    =/= wne 2641   _Vcvv 3031    u. cun 3388    i^i cin 3389   (/)c0 3722   ifcif 3872   {csn 3959   class class class wbr 4395    |-> cmpt 4454   -->wf 5585   ` cfv 5589  (class class class)co 6308    ^m cmap 7490   Fincfn 7587   CCcc 9555   RRcr 9556   0cc0 9557   1c1 9558    + caddc 9560    < clt 9693    <_ cle 9694    - cmin 9880   NNcn 10631   2c2 10681   NN0cn0 10893   ZZcz 10961   ZZ>=cuz 11182   ...cfz 11810   Basecbs 15199   +g cplusg 15268   .rcmulr 15269  Scalarcsca 15271   .scvsca 15272   0gc0g 15416    gsumg cgsu 15417   Mndcmnd 16613   Grpcgrp 16747   -gcsg 16749  .gcmg 16750  CMndccmn 17508  mulGrpcmgp 17801   1rcur 17813   Ringcrg 17858   CRingccrg 17859   LModclmod 18169  var1cv1 18846  Poly1cpl1 18847   Mat cmat 19509   matToPolyMat cmat2pmat 19805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-ot 3968  df-uni 4191  df-int 4227  df-iun 4271  df-iin 4272  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-of 6550  df-ofr 6551  df-om 6712  df-1st 6812  df-2nd 6813  df-supp 6934  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-er 7381  df-map 7492  df-pm<