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

Theorem chfacfscmulgsum 19877
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 2450 . . 3  |-  ( Base `  Y )  =  (
Base `  Y )
2 chfacfisf.0 . . 3  |-  .0.  =  ( 0g `  Y )
3 chfacfscmulgsum.p . . 3  |-  .+  =  ( +g  `  Y )
4 crngring 17784 . . . . . . . 8  |-  ( R  e.  CRing  ->  R  e.  Ring )
54anim2i 572 . . . . . . 7  |-  ( ( N  e.  Fin  /\  R  e.  CRing )  -> 
( N  e.  Fin  /\  R  e.  Ring )
)
653adant3 1027 . . . . . 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 19710 . . . . . 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 17804 . . . . 5  |-  ( Y  e.  Ring  ->  Y  e. CMnd
)
1210, 11syl 17 . . . 4  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  Y  e. CMnd )
1312adantr 467 . . 3  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  Y  e. CMnd )
14 nn0ex 10872 . . . 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 759 . . . . 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 761 . . . . 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 463 . . . . 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 1187 . . . 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 19874 . . . 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 19876 . . 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 11904 . . . 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 10873 . . . . . 6  |-  ( s  e.  NN  ->  s  e.  NN0 )
35 peano2nn0 10907 . . . . . 6  |-  ( s  e.  NN0  ->  ( s  +  1 )  e. 
NN0 )
3634, 35syl 17 . . . . 5  |-  ( s  e.  NN  ->  (
s  +  1 )  e.  NN0 )
37 nn0split 11903 . . . . 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 733 . . 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 17555 . 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 759 . . . . . . . 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 761 . . . . . . . 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 10614 . . . . . . . . . . . . 13  |-  ( s  e.  NN  ->  s  e.  CC )
44 add1p1 10859 . . . . . . . . . . . . 13  |-  ( s  e.  CC  ->  (
( s  +  1 )  +  1 )  =  ( s  +  2 ) )
4543, 44syl 17 . . . . . . . . . . . 12  |-  ( s  e.  NN  ->  (
( s  +  1 )  +  1 )  =  ( s  +  2 ) )
4645ad2antrl 733 . . . . . . . . . . 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 5867 . . . . . . . . . 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 2513 . . . . . . . . 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 487 . . . . . . . 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 19875 . . . . . . . 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 1267 . . . . . . 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 4488 . . . . . 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 6304 . . . . 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 477 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  R  e.  CRing )  ->  Y  e.  Ring )
55 ringmnd 17782 . . . . . . . . . 10  |-  ( Y  e.  Ring  ->  Y  e. 
Mnd )
5654, 55syl 17 . . . . . . . . 9  |-  ( ( N  e.  Fin  /\  R  e.  CRing )  ->  Y  e.  Mnd )
57563adant3 1027 . . . . . . . 8  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  Y  e.  Mnd )
58 fvex 5873 . . . . . . . 8  |-  ( ZZ>= `  ( ( s  +  1 )  +  1 ) )  e.  _V
5957, 58jctir 541 . . . . . . 7  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  ( Y  e.  Mnd  /\  ( ZZ>=
`  ( ( s  +  1 )  +  1 ) )  e. 
_V ) )
6059adantr 467 . . . . . 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 16614 . . . . . 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 2484 . . . 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 6304 . . 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 467 . . . 4  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  Y  e.  Mnd )
66 fzfid 12183 . . . . 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 11884 . . . . . . . 8  |-  ( i  e.  ( 0 ... ( s  +  1 ) )  ->  i  e.  NN0 )
6867, 19sylan2 477 . . . . . . 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 2801 . . . . 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 17592 . . . 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 16551 . . . 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 666 . . 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 2484 . 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 733 . . . 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 17558 . . 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 11884 . . . . . . 7  |-  ( i  e.  ( 0 ... s )  ->  i  e.  NN0 )
7877, 30sylan2 477 . . . . . 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 17559 . . . . 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 10881 . . . . . . . 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 19874 . . . . . . . 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 1364 . . . . . . 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 6295 . . . . . . . . 9  |-  ( i  =  0  ->  (
i  .^  X )  =  ( 0  .^  X ) )
85 fveq2 5863 . . . . . . . . 9  |-  ( i  =  0  ->  ( G `  i )  =  ( G ` 
0 ) )
8684, 85oveq12d 6306 . . . . . . . 8  |-  ( i  =  0  ->  (
( i  .^  X
)  .x.  ( G `  i ) )  =  ( ( 0  .^  X )  .x.  ( G `  0 )
) )
871, 86gsumsn 17580 . . . . . . 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 1267 . . . . . 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 6304 . . . . 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 2484 . . . 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 6316 . . . . . 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 10882 . . . . . . . 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 10926 . . . . . 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 19874 . . . . . 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 1364 . . . . 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 6295 . . . . . . 7  |-  ( i  =  ( s  +  1 )  ->  (
i  .^  X )  =  ( ( s  +  1 )  .^  X ) )
99 fveq2 5863 . . . . . . 7  |-  ( i  =  ( s  +  1 )  ->  ( G `  i )  =  ( G `  ( s  +  1 ) ) )
10098, 99oveq12d 6306 . . . . . 6  |-  ( i  =  ( s  +  1 )  ->  (
( i  .^  X
)  .x.  ( G `  i ) )  =  ( ( ( s  +  1 )  .^  X )  .x.  ( G `  ( s  +  1 ) ) ) )
1011, 100gsumsn 17580 . . . . 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 1267 . . . 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 6306 . . 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 12183 . . . . . 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 759 . . . . . . . 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 761 . . . . . . . 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 11825 . . . . . . . . . 10  |-  ( i  e.  ( 1 ... s )  ->  i  e.  NN )
108107nnnn0d 10922 . . . . . . . . 9  |-  ( i  e.  ( 1 ... s )  ->  i  e.  NN0 )
109108adantl 468 . . . . . . . 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 1267 . . . . . . 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 2801 . . . . . 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 17592 . . . . 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 16539 . . . . 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 1269 . . . 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 10651 . . . . . . . . . . . . . 14  |-  ( i  e.  ( 1 ... s )  ->  i  =/=  0 )
117116ad2antlr 732 . . . . . . . . . . . . 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 2685 . . . . . . . . . . . . . 14  |-  ( n  =  i  ->  (
n  =/=  0  <->  i  =/=  0 ) )
119118adantl 468 . . . . . . . . . . . . 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 236 . . . . . . . . . . . 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 2633 . . . . . . . . . . . 12  |-  ( n  =  0  ->  (
n  =/=  0  ->  .0.  =  ( T `  ( b `  (
i  -  1 ) ) ) ) )
122120, 121mpan9 472 . . . . . . . . . . 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 761 . . . . . . . . . . . . . . 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 2454 . . . . . . . . . . . . . . . . 17  |-  ( 0  =  n  ->  (
0  =  i  <->  n  =  i ) )
125124eqcoms 2458 . . . . . . . . . . . . . . . 16  |-  ( n  =  0  ->  (
0  =  i  <->  n  =  i ) )
126125adantl 468 . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . 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 5867 . . . . . . . . . . . . 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 5867 . . . . . . . . . . . 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 6304 . . . . . . . . . . 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 6306 . . . . . . . . . 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 11788 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... s )  <->  ( (
1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  /\  (
1  <_  i  /\  i  <_  s ) ) )
133 zleltp1 10984 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( i  e.  ZZ  /\  s  e.  ZZ )  ->  ( i  <_  s  <->  i  <  ( s  +  1 ) ) )
134133ancoms 455 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  e.  ZZ  /\  i  e.  ZZ )  ->  ( i  <_  s  <->  i  <  ( s  +  1 ) ) )
1351343adant1 1025 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  ->  (
i  <_  s  <->  i  <  ( s  +  1 ) ) )
136135biimpcd 228 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  <_  s  ->  (
( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  ->  i  <  ( s  +  1 ) ) )
137136adantl 468 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  <_  i  /\  i  <_  s )  -> 
( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  ->  i  <  ( s  +  1 ) ) )
138137impcom 432 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  /\  ( 1  <_  i  /\  i  <_  s ) )  ->  i  <  ( s  +  1 ) )
139138orcd 394 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  /\  ( 1  <_  i  /\  i  <_  s ) )  ->  ( i  <  ( s  +  1 )  \/  ( s  +  1 )  < 
i ) )
140 zre 10938 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ZZ  ->  s  e.  RR )
141 1red 9655 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ZZ  ->  1  e.  RR )
142140, 141readdcld 9667 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s  e.  ZZ  ->  (
s  +  1 )  e.  RR )
143 zre 10938 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  e.  ZZ  ->  i  e.  RR )
144142, 143anim12ci 570 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( s  e.  ZZ  /\  i  e.  ZZ )  ->  ( i  e.  RR  /\  ( s  +  1 )  e.  RR ) )
1451443adant1 1025 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  ->  (
i  e.  RR  /\  ( s  +  1 )  e.  RR ) )
146 lttri2 9713 . . . . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  i  e.  ZZ )  /\  ( 1  <_  i  /\  i  <_  s ) )  ->  i  =/=  ( s  +  1 ) )
150132, 149sylbi 199 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( 1 ... s )  ->  i  =/=  ( s  +  1 ) )
151150ad2antlr 732 . . . . . . . . . . . . . . . 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 2685 . . . . . . . . . . . . . . . . 17  |-  ( n  =  i  ->  (
n  =/=  ( s  +  1 )  <->  i  =/=  ( s  +  1 ) ) )
153152adantl 468 . . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . 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 2628 . . . . . . . . . . . . 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 110 . . . . . . . . . . . 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 431 . . . . . . . . . . 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 10621 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( 1 ... s )  ->  i  e.  RR )
160 eleq1 2516 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  i  ->  (
n  e.  RR  <->  i  e.  RR ) )
161159, 160syl5ibrcom 226 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... s )  ->  (
n  =  i  ->  n  e.  RR )
)
162161adantl 468 . . . . . . . . . . . . . . . . 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 431 . . . . . . . . . . . . . . . 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 10923 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  s  e.  RR )
165164ad2antrr 731 . . . . . . . . . . . . . . . . 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 9655 . . . . . . . . . . . . . . . . 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 9667 . . . . . . . . . . . . . . . 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 199 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 1 ... s )  ->  i  <  ( s  +  1 ) )
169168ad2antlr 732 . . . . . . . . . . . . . . . . 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 4404 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  i  ->  (
n  <  ( s  +  1 )  <->  i  <  ( s  +  1 ) ) )
171170adantl 468 . . . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . . . 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 9781 . . . . . . . . . . . . . . 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 110 . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . 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 431 . . . . . . . . . . . 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 776 . . . . . . . . . . . . . . . 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 6303 . . . . . . . . . . . . . . 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 5867 . . . . . . . . . . . . . 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 5867 . . . . . . . . . . . . 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 5867 . . . . . . . . . . . . . . 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 5867 . . . . . . . . . . . . . 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 6304 . . . . . . . . . . . . 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 6306 . . . . . . . . . . . 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 3913 . . . . . . . . . . 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 3913 . . . . . . . . . 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 3913 . . . . . . . . 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 6316 . . . . . . . . . 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 5952 . . . . . . . 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 6304 . . . . . . 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 4488 . . . . . 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 6304 . . . . 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 10896 . . . . . . . . . . . . . . 15  |-  ( s  e.  NN0  ->  0  < 
( s  +  1 ) )
196 0red 9641 . . . . . . . . . . . . . . . . 17  |-  ( s  e.  NN0  ->  0  e.  RR )
197 ltne 9727 . . . . . . . . . . . . . . . . 17  |-  ( ( 0  e.  RR  /\  0  <  ( s  +  1 ) )  -> 
( s  +  1 )  =/=  0 )
198196, 197sylan 474 . . . . . . . . . . . . . . . 16  |-  ( ( s  e.  NN0  /\  0  <  ( s  +  1 ) )  -> 
( s  +  1 )  =/=  0 )
199 neeq1 2685 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( s  +  1 )  ->  (
n  =/=  0  <->  (
s  +  1 )  =/=  0 ) )
200198, 199syl5ibrcom 226 . . . . . . . . . . . . . . 15  |-  ( ( s  e.  NN0  /\  0  <  ( s  +  1 ) )  -> 
( n  =  ( s  +  1 )  ->  n  =/=  0
) )
201195, 200mpdan 673 . . . . . . . . . . . . . 14  |-  ( s  e.  NN0  ->  ( n  =  ( s  +  1 )  ->  n  =/=  0 ) )
20234, 201syl 17 . . . . . . . . . . . . 13  |-  ( s  e.  NN  ->  (
n  =  ( s  +  1 )  ->  n  =/=  0 ) )
203202ad2antrl 733 . . . . . . . . . . . 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 431 . . . . . . . . . . 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 2633 . . . . . . . . . . 11  |-  ( n  =  0  ->  (
n  =/=  0  -> 
(  .0.  .-  (
( T `  M
)  .X.  ( T `  ( b `  0
) ) ) )  =  ( T `  ( b `  s
) ) ) )
206204, 205mpan9 472 . . . . . . . . . 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 3886 . . . . . . . . . . 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 732 . . . . . . . . . 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 3913 . . . . . . . . 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 5873 . . . . . . . . . 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 5952 . . . . . . . 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 6304 . . . . . . 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 1029 . . . . . . . . . . . . 13  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  R  e.  Ring )
216 eqid 2450 . . . . . . . . . . . . . 14  |-  ( Base `  P )  =  (
Base `  P )
21726, 7, 216vr1cl 18803 . . . . . . . . . . . . 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 2450 . . . . . . . . . . . . . 14  |-  (mulGrp `  P )  =  (mulGrp `  P )
220219, 216mgpbas 17722 . . . . . . . . . . . . 13  |-  ( Base `  P )  =  (
Base `  (mulGrp `  P
) )
221 eqid 2450 . . . . . . . . . . . . . 14  |-  ( 1r
`  P )  =  ( 1r `  P
)
222219, 221ringidval 17730 . . . . . . . . . . . . 13  |-  ( 1r
`  P )  =  ( 0g `  (mulGrp `  P ) )
223220, 222, 28mulg0 16756 . . . . . . . . . . . 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 18784 . . . . . . . . . . . . . . 15  |-  ( R  e.  CRing  ->  P  e.  CRing
)
226225anim2i 572 . . . . . . . . . . . . . 14  |-  ( ( N  e.  Fin  /\  R  e.  CRing )  -> 
( N  e.  Fin  /\  P  e.  CRing ) )
2272263adant3 1027 . . . . . . . . . . . . 13  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  ( N  e.  Fin  /\  P  e.  CRing ) )
2288matsca2 19438 . . . . . . . . . . . . 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 5867 . . . . . . . . . . 11  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  ( 1r `  P )  =  ( 1r `  (Scalar `  Y ) ) )
231224, 230eqtrd 2484 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  (
0  .^  X )  =  ( 1r `  (Scalar `  Y ) ) )
232231adantr 467 . . . . . . . . 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 6303 . . . . . . . 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 19711 . . . . . . . . . . . 12  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  ->  Y  e.  LMod )
2354, 234sylan2 477 . . . . . . . . . . 11  |-  ( ( N  e.  Fin  /\  R  e.  CRing )  ->  Y  e.  LMod )
2362353adant3 1027 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  Y  e.  LMod )
237236adantr 467 . . . . . . . . 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 19871 . . . . . . . . . . 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 1316 . . . . . . . . . 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 6021 . . . . . . . . 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 2450 . . . . . . . . . 10  |-  (Scalar `  Y )  =  (Scalar `  Y )
242 eqid 2450 . . . . . . . . . 10  |-  ( 1r
`  (Scalar `  Y )
)  =  ( 1r
`  (Scalar `  Y )
)
2431, 241, 27, 242lmodvs1 18112 . . . . . . . . 9  |-  ( ( Y  e.  LMod  /\  ( G `  0 )  e.  ( Base `  Y
) )  ->  (
( 1r `  (Scalar `  Y ) )  .x.  ( G `  0 ) )  =  ( G `
 0 ) )
244237, 240, 243syl2anc 666 . . . . . . . 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 3886 . . . . . . . . . 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 468 . . . . . . . . 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 6316 . . . . . . . . . 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 5952 . . . . . . . 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 2488 . . . . . . 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 6306 . . . . . 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 17439 . . . . . . 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 1267 . . . . . 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 17778 . . . . . . . . 9  |-  ( Y  e.  Ring  ->  Y  e. 
Grp )
25510, 254syl 17 . . . . . . . 8  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  Y  e.  Grp )
256255adantr 467 . . . . . . 7  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  Y  e.  Grp )
257214, 97eqeltrrd 2529 . . . . . . 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 467 . . . . . . . 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 19743 . . . . . . . . . 10  |-  ( ( N  e.  Fin  /\  R  e.  Ring  /\  M  e.  B )  ->  ( T `  M )  e.  ( Base `  Y
) )
2604, 259syl3an2 1301 . . . . . . . . 9  |-  ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  ->  ( T `  M )  e.  ( Base `  Y
) )
261260adantr 467 . . . . . . . 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 1010 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  N  e.  Fin )
263215adantr 467 . . . . . . . . 9  |-  ( ( ( N  e.  Fin  /\  R  e.  CRing  /\  M  e.  B )  /\  (
s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) ) )  ->  R  e.  Ring )
264 elmapi 7490 . . . . . . . . . . . 12  |-  ( b  e.  ( B  ^m  ( 0 ... s
) )  ->  b : ( 0 ... s ) --> B )
265264adantl 468 . . . . . . . . . . 11  |-  ( ( s  e.  NN  /\  b  e.  ( B  ^m  ( 0 ... s
) ) )  -> 
b : ( 0 ... s ) --> B )
266265adantl 468 . . . . . . . . . 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 11886 . . . . . . . . . . . 12  |-  ( s  e.  NN0  ->  0  e.  ( 0 ... s
) )
26834, 267syl 17 . . . . . . . . . . 11  |-  ( s  e.  NN  ->  0  e.  ( 0 ... s
) )
269268ad2antrl 733 . . . . . . . . . 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 6021 . . . . . . . . 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 19743 . . . . . . . . 9  |-  ( ( N  e.  Fin  /\  R  e.  Ring  /\  (
b `  0 )  e.  B )  ->  ( T `  ( b `  0 ) )  e.  ( Base `  Y
) )
272262, 263, 270, 271syl3anc 1267 . . . . . . . 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 17787 . . . . . . . 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 1267 . . . . . . 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 16734 . . . . . . 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 1267 . . . . . 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 2494 . . . . 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 6306 . . . 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 2484 . . 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 2488 . 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 2488 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 188    \/ wo 370    /\ wa 371    /\ w3a 984    = wceq 1443    e. wcel 1886    =/= wne 2621   _Vcvv 3044    u. cun 3401    i^i cin 3402   (/)c0 3730   ifcif 3880   {csn 3967   class class class wbr 4401    |-> cmpt 4460   -->wf 5577   ` cfv 5581  (class class class)co 6288    ^m cmap 7469   Fincfn 7566   CCcc 9534   RRcr 9535   0cc0 9536   1c1 9537    + caddc 9539    < clt 9672    <_ cle 9673    - cmin 9857   NNcn 10606   2c2 10656   NN0cn0 10866   ZZcz 10934   ZZ>=cuz 11156   ...cfz 11781   Basecbs 15114   +g cplusg 15183   .rcmulr 15184  Scalarcsca 15186   .scvsca 15187   0gc0g 15331    gsumg cgsu 15332   Mndcmnd 16528   Grpcgrp 16662   -gcsg 16664  .gcmg 16665  CMndccmn 17423  mulGrpcmgp 17716   1rcur 17728   Ringcrg 17773   CRingccrg 17774   LModclmod 18084  var1cv1 18762  Poly1cpl1 18763   Mat cmat 19425   matToPolyMat cmat2pmat 19721
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-inf2 8143  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-fal 1449  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-ot 3976  df-uni 4198  df-int 4234  df-iun 4279  df-iin 4280  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-se 4793  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-isom 5590  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-of 6528  df-ofr 6529  df-om 6690  df-1st 6790  df-2nd 6791  df-supp 6912  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-1o 7179  df-2o 7180  df-oadd 7183  df-er 7360  df-map 7471  df-pm