Metamath Proof Explorer

Theorem chfacfpmmulgsum

Description: Breaking up a sum of values of the "characteristic factor function" multiplied with a constant polynomial matrix. (Contributed by AV, 23-Nov-2019)

Ref Expression
Hypotheses cayhamlem1.a 
|- A = ( N Mat R )
cayhamlem1.b 
|- B = ( Base ` A )
cayhamlem1.p 
|- P = ( Poly1 ` R )
cayhamlem1.y 
|- Y = ( N Mat P )
cayhamlem1.r 
|- .X. = ( .r ` Y )
cayhamlem1.s 
|- .- = ( -g ` Y )
cayhamlem1.0 
|- .0. = ( 0g ` Y )
cayhamlem1.t 
|- T = ( N matToPolyMat R )
cayhamlem1.g 
|- G = ( n e. NN0 |-> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) )
cayhamlem1.e 
|- .^ = ( .g ` ( mulGrp ` Y ) )
chfacfpmmulgsum.p 
|- .+ = ( +g ` Y )
Assertion chfacfpmmulgsum 
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. NN0 |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cayhamlem1.a 
 |-  A = ( N Mat R )
2 cayhamlem1.b 
 |-  B = ( Base ` A )
3 cayhamlem1.p 
 |-  P = ( Poly1 ` R )
4 cayhamlem1.y 
 |-  Y = ( N Mat P )
5 cayhamlem1.r 
 |-  .X. = ( .r ` Y )
6 cayhamlem1.s 
 |-  .- = ( -g ` Y )
7 cayhamlem1.0 
 |-  .0. = ( 0g ` Y )
8 cayhamlem1.t 
 |-  T = ( N matToPolyMat R )
9 cayhamlem1.g 
 |-  G = ( n e. NN0 |-> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) )
10 cayhamlem1.e 
 |-  .^ = ( .g ` ( mulGrp ` Y ) )
11 chfacfpmmulgsum.p 
 |-  .+ = ( +g ` Y )
12 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
13 crngring 
 |-  ( R e. CRing -> R e. Ring )
14 13 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
15 14 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ R e. Ring ) )
16 3 4 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Y e. Ring )
17 15 16 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Ring )
18 ringcmn 
 |-  ( Y e. Ring -> Y e. CMnd )
19 17 18 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. CMnd )
20 19 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. CMnd )
21 nn0ex 
 |-  NN0 e. _V
22 21 a1i 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> NN0 e. _V )
23 simpll 
 |-  ( ( ( ( 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 ) )
24 simplr 
 |-  ( ( ( ( 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 ) ) ) )
25 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. NN0 ) -> i e. NN0 )
26 23 24 25 3jca 
 |-  ( ( ( ( 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 ) )
27 1 2 3 4 5 6 7 8 9 10 chfacfpmmulcl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ i e. NN0 ) -> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) e. ( Base ` Y ) )
28 26 27 syl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. NN0 ) -> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) e. ( Base ` Y ) )
29 1 2 3 4 5 6 7 8 9 10 chfacfpmmulfsupp 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( i e. NN0 |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) finSupp .0. )
30 nn0disj 
 |-  ( ( 0 ... ( s + 1 ) ) i^i ( ZZ>= ` ( ( s + 1 ) + 1 ) ) ) = (/)
31 30 a1i 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 0 ... ( s + 1 ) ) i^i ( ZZ>= ` ( ( s + 1 ) + 1 ) ) ) = (/) )
32 nnnn0 
 |-  ( s e. NN -> s e. NN0 )
33 peano2nn0 
 |-  ( s e. NN0 -> ( s + 1 ) e. NN0 )
34 32 33 syl 
 |-  ( s e. NN -> ( s + 1 ) e. NN0 )
35 nn0split 
 |-  ( ( s + 1 ) e. NN0 -> NN0 = ( ( 0 ... ( s + 1 ) ) u. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) ) )
36 34 35 syl 
 |-  ( s e. NN -> NN0 = ( ( 0 ... ( s + 1 ) ) u. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) ) )
37 36 ad2antrl 
 |-  ( ( ( 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 ) ) ) )
38 12 7 11 20 22 28 29 31 37 gsumsplit2 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. NN0 |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( Y gsum ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( Y gsum ( i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) ) )
39 simpll 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) ) -> ( N e. Fin /\ R e. CRing /\ M e. B ) )
40 simplr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) ) -> ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) )
41 nncn 
 |-  ( s e. NN -> s e. CC )
42 add1p1 
 |-  ( s e. CC -> ( ( s + 1 ) + 1 ) = ( s + 2 ) )
43 41 42 syl 
 |-  ( s e. NN -> ( ( s + 1 ) + 1 ) = ( s + 2 ) )
44 43 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( s + 1 ) + 1 ) = ( s + 2 ) )
45 44 fveq2d 
 |-  ( ( ( 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 ) ) )
46 45 eleq2d 
 |-  ( ( ( 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 ) ) ) )
47 46 biimpa 
 |-  ( ( ( ( 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 ) ) )
48 1 2 3 4 5 6 7 8 9 10 chfacfpmmul0 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ i e. ( ZZ>= ` ( s + 2 ) ) ) -> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) = .0. )
49 39 40 47 48 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) ) -> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) = .0. )
50 49 mpteq2dva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) = ( i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) |-> .0. ) )
51 50 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( Y gsum ( i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) |-> .0. ) ) )
52 13 16 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. Ring )
53 ringmnd 
 |-  ( Y e. Ring -> Y e. Mnd )
54 52 53 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. Mnd )
55 54 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Mnd )
56 fvex 
 |-  ( ZZ>= ` ( ( s + 1 ) + 1 ) ) e. _V
57 55 56 jctir 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Y e. Mnd /\ ( ZZ>= ` ( ( s + 1 ) + 1 ) ) e. _V ) )
58 57 adantr 
 |-  ( ( ( 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 ) )
59 7 gsumz 
 |-  ( ( Y e. Mnd /\ ( ZZ>= ` ( ( s + 1 ) + 1 ) ) e. _V ) -> ( Y gsum ( i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) |-> .0. ) ) = .0. )
60 58 59 syl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) |-> .0. ) ) = .0. )
61 51 60 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = .0. )
62 61 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsum ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( Y gsum ( i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) ) = ( ( Y gsum ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ .0. ) )
63 fzfid 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0 ... ( s + 1 ) ) e. Fin )
64 elfznn0 
 |-  ( i e. ( 0 ... ( s + 1 ) ) -> i e. NN0 )
65 64 26 sylan2 
 |-  ( ( ( ( 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 ) )
66 65 27 syl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( s + 1 ) ) ) -> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) e. ( Base ` Y ) )
67 66 ralrimiva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> A. i e. ( 0 ... ( s + 1 ) ) ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) e. ( Base ` Y ) )
68 12 20 63 67 gsummptcl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) e. ( Base ` Y ) )
69 12 11 7 mndrid 
 |-  ( ( Y e. Mnd /\ ( Y gsum ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) e. ( Base ` Y ) ) -> ( ( Y gsum ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ .0. ) = ( Y gsum ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) )
70 55 68 69 syl2an2r 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsum ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ .0. ) = ( Y gsum ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) )
71 62 70 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsum ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( Y gsum ( i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) ) = ( Y gsum ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) )
72 32 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> s e. NN0 )
73 12 11 20 72 66 gsummptfzsplit 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( Y gsum ( i e. { ( s + 1 ) } |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) ) )
74 elfznn0 
 |-  ( i e. ( 0 ... s ) -> i e. NN0 )
75 74 28 sylan2 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... s ) ) -> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) e. ( Base ` Y ) )
76 12 11 20 72 75 gsummptfzsplitl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( Y gsum ( i e. { 0 } |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) ) )
77 55 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Mnd )
78 0nn0 
 |-  0 e. NN0
79 78 a1i 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> 0 e. NN0 )
80 1 2 3 4 5 6 7 8 9 10 chfacfpmmulcl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ 0 e. NN0 ) -> ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) e. ( Base ` Y ) )
81 79 80 mpd3an3 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) e. ( Base ` Y ) )
82 oveq1 
 |-  ( i = 0 -> ( i .^ ( T ` M ) ) = ( 0 .^ ( T ` M ) ) )
83 fveq2 
 |-  ( i = 0 -> ( G ` i ) = ( G ` 0 ) )
84 82 83 oveq12d 
 |-  ( i = 0 -> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) = ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) )
85 12 84 gsumsn 
 |-  ( ( Y e. Mnd /\ 0 e. NN0 /\ ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) e. ( Base ` Y ) ) -> ( Y gsum ( i e. { 0 } |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) )
86 77 79 81 85 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. { 0 } |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) )
87 86 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( Y gsum ( i e. { 0 } |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) ) )
88 76 87 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) ) )
89 ovexd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( s + 1 ) e. _V )
90 1nn0 
 |-  1 e. NN0
91 90 a1i 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> 1 e. NN0 )
92 72 91 nn0addcld 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( s + 1 ) e. NN0 )
93 1 2 3 4 5 6 7 8 9 10 chfacfpmmulcl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ ( s + 1 ) e. NN0 ) -> ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) e. ( Base ` Y ) )
94 92 93 mpd3an3 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) e. ( Base ` Y ) )
95 oveq1 
 |-  ( i = ( s + 1 ) -> ( i .^ ( T ` M ) ) = ( ( s + 1 ) .^ ( T ` M ) ) )
96 fveq2 
 |-  ( i = ( s + 1 ) -> ( G ` i ) = ( G ` ( s + 1 ) ) )
97 95 96 oveq12d 
 |-  ( i = ( s + 1 ) -> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) = ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) )
98 12 97 gsumsn 
 |-  ( ( Y e. Mnd /\ ( s + 1 ) e. _V /\ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) e. ( Base ` Y ) ) -> ( Y gsum ( i e. { ( s + 1 ) } |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) )
99 77 89 94 98 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. { ( s + 1 ) } |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) )
100 88 99 oveq12d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsum ( i e. ( 0 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( Y gsum ( i e. { ( s + 1 ) } |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) ) = ( ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) ) .+ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) ) )
101 fzfid 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 1 ... s ) e. Fin )
102 simpll 
 |-  ( ( ( ( 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 ) )
103 simplr 
 |-  ( ( ( ( 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 ) ) ) )
104 elfznn 
 |-  ( i e. ( 1 ... s ) -> i e. NN )
105 104 nnnn0d 
 |-  ( i e. ( 1 ... s ) -> i e. NN0 )
106 105 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> i e. NN0 )
107 102 103 106 27 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) e. ( Base ` Y ) )
108 107 ralrimiva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> A. i e. ( 1 ... s ) ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) e. ( Base ` Y ) )
109 12 20 101 108 gsummptcl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) e. ( Base ` Y ) )
110 12 11 mndass 
 |-  ( ( Y e. Mnd /\ ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) e. ( Base ` Y ) /\ ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) e. ( Base ` Y ) /\ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) e. ( Base ` Y ) ) ) -> ( ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) ) .+ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) .+ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) ) ) )
111 77 109 81 94 110 syl13anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) ) .+ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) .+ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) ) ) )
112 104 nnne0d 
 |-  ( i e. ( 1 ... s ) -> i =/= 0 )
113 112 ad2antlr 
 |-  ( ( ( ( ( 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 )
114 neeq1 
 |-  ( n = i -> ( n =/= 0 <-> i =/= 0 ) )
115 114 adantl 
 |-  ( ( ( ( ( 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 ) )
116 113 115 mpbird 
 |-  ( ( ( ( ( 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 )
117 eqneqall 
 |-  ( n = 0 -> ( n =/= 0 -> .0. = ( T ` ( b ` ( i - 1 ) ) ) ) )
118 116 117 mpan9 
 |-  ( ( ( ( ( ( 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 ) ) ) )
119 simplr 
 |-  ( ( ( ( ( ( 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 )
120 eqeq1 
 |-  ( 0 = n -> ( 0 = i <-> n = i ) )
121 120 eqcoms 
 |-  ( n = 0 -> ( 0 = i <-> n = i ) )
122 121 adantl 
 |-  ( ( ( ( ( ( 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 ) )
123 119 122 mpbird 
 |-  ( ( ( ( ( ( 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 )
124 123 fveq2d 
 |-  ( ( ( ( ( ( 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 ) )
125 124 fveq2d 
 |-  ( ( ( ( ( ( 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 ) ) )
126 125 oveq2d 
 |-  ( ( ( ( ( ( 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 ) ) ) )
127 118 126 oveq12d 
 |-  ( ( ( ( ( ( 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 ) ) ) ) )
128 elfz2 
 |-  ( i e. ( 1 ... s ) <-> ( ( 1 e. ZZ /\ s e. ZZ /\ i e. ZZ ) /\ ( 1 <_ i /\ i <_ s ) ) )
129 zleltp1 
 |-  ( ( i e. ZZ /\ s e. ZZ ) -> ( i <_ s <-> i < ( s + 1 ) ) )
130 129 ancoms 
 |-  ( ( s e. ZZ /\ i e. ZZ ) -> ( i <_ s <-> i < ( s + 1 ) ) )
131 130 3adant1 
 |-  ( ( 1 e. ZZ /\ s e. ZZ /\ i e. ZZ ) -> ( i <_ s <-> i < ( s + 1 ) ) )
132 131 biimpcd 
 |-  ( i <_ s -> ( ( 1 e. ZZ /\ s e. ZZ /\ i e. ZZ ) -> i < ( s + 1 ) ) )
133 132 adantl 
 |-  ( ( 1 <_ i /\ i <_ s ) -> ( ( 1 e. ZZ /\ s e. ZZ /\ i e. ZZ ) -> i < ( s + 1 ) ) )
134 133 impcom 
 |-  ( ( ( 1 e. ZZ /\ s e. ZZ /\ i e. ZZ ) /\ ( 1 <_ i /\ i <_ s ) ) -> i < ( s + 1 ) )
135 134 orcd 
 |-  ( ( ( 1 e. ZZ /\ s e. ZZ /\ i e. ZZ ) /\ ( 1 <_ i /\ i <_ s ) ) -> ( i < ( s + 1 ) \/ ( s + 1 ) < i ) )
136 zre 
 |-  ( s e. ZZ -> s e. RR )
137 1red 
 |-  ( s e. ZZ -> 1 e. RR )
138 136 137 readdcld 
 |-  ( s e. ZZ -> ( s + 1 ) e. RR )
139 zre 
 |-  ( i e. ZZ -> i e. RR )
140 138 139 anim12ci 
 |-  ( ( s e. ZZ /\ i e. ZZ ) -> ( i e. RR /\ ( s + 1 ) e. RR ) )
141 140 3adant1 
 |-  ( ( 1 e. ZZ /\ s e. ZZ /\ i e. ZZ ) -> ( i e. RR /\ ( s + 1 ) e. RR ) )
142 lttri2 
 |-  ( ( i e. RR /\ ( s + 1 ) e. RR ) -> ( i =/= ( s + 1 ) <-> ( i < ( s + 1 ) \/ ( s + 1 ) < i ) ) )
143 141 142 syl 
 |-  ( ( 1 e. ZZ /\ s e. ZZ /\ i e. ZZ ) -> ( i =/= ( s + 1 ) <-> ( i < ( s + 1 ) \/ ( s + 1 ) < i ) ) )
144 143 adantr 
 |-  ( ( ( 1 e. ZZ /\ s e. ZZ /\ i e. ZZ ) /\ ( 1 <_ i /\ i <_ s ) ) -> ( i =/= ( s + 1 ) <-> ( i < ( s + 1 ) \/ ( s + 1 ) < i ) ) )
145 135 144 mpbird 
 |-  ( ( ( 1 e. ZZ /\ s e. ZZ /\ i e. ZZ ) /\ ( 1 <_ i /\ i <_ s ) ) -> i =/= ( s + 1 ) )
146 128 145 sylbi 
 |-  ( i e. ( 1 ... s ) -> i =/= ( s + 1 ) )
147 146 ad2antlr 
 |-  ( ( ( ( ( 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 ) )
148 neeq1 
 |-  ( n = i -> ( n =/= ( s + 1 ) <-> i =/= ( s + 1 ) ) )
149 148 adantl 
 |-  ( ( ( ( ( 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 ) ) )
150 147 149 mpbird 
 |-  ( ( ( ( ( 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 ) )
151 150 adantr 
 |-  ( ( ( ( ( ( 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 ) )
152 151 neneqd 
 |-  ( ( ( ( ( ( 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 ) )
153 152 pm2.21d 
 |-  ( ( ( ( ( ( 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 ) ) ) ) ) )
154 153 imp 
 |-  ( ( ( ( ( ( ( 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 ) ) ) ) )
155 104 nnred 
 |-  ( i e. ( 1 ... s ) -> i e. RR )
156 eleq1w 
 |-  ( n = i -> ( n e. RR <-> i e. RR ) )
157 155 156 syl5ibrcom 
 |-  ( i e. ( 1 ... s ) -> ( n = i -> n e. RR ) )
158 157 adantl 
 |-  ( ( ( ( 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 ) )
159 158 imp 
 |-  ( ( ( ( ( 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 )
160 72 nn0red 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> s e. RR )
161 160 ad2antrr 
 |-  ( ( ( ( ( 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 )
162 1red 
 |-  ( ( ( ( ( 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 )
163 161 162 readdcld 
 |-  ( ( ( ( ( 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 )
164 128 134 sylbi 
 |-  ( i e. ( 1 ... s ) -> i < ( s + 1 ) )
165 164 ad2antlr 
 |-  ( ( ( ( ( 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 ) )
166 breq1 
 |-  ( n = i -> ( n < ( s + 1 ) <-> i < ( s + 1 ) ) )
167 166 adantl 
 |-  ( ( ( ( ( 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 ) ) )
168 165 167 mpbird 
 |-  ( ( ( ( ( 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 ) )
169 159 163 168 ltnsymd 
 |-  ( ( ( ( ( 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 )
170 169 pm2.21d 
 |-  ( ( ( ( ( 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 ) ) ) ) ) )
171 170 ad2antrr 
 |-  ( ( ( ( ( ( ( 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 ) ) ) ) ) )
172 171 imp 
 |-  ( ( ( ( ( ( ( ( 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 ) ) ) ) )
173 simp-4r 
 |-  ( ( ( ( ( ( ( ( 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 )
174 173 fvoveq1d 
 |-  ( ( ( ( ( ( ( ( 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 ) ) )
175 174 fveq2d 
 |-  ( ( ( ( ( ( ( ( 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 ) ) ) )
176 173 fveq2d 
 |-  ( ( ( ( ( ( ( ( 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 ) )
177 176 fveq2d 
 |-  ( ( ( ( ( ( ( ( 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 ) ) )
178 177 oveq2d 
 |-  ( ( ( ( ( ( ( ( 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 ) ) ) )
179 175 178 oveq12d 
 |-  ( ( ( ( ( ( ( ( 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 ) ) ) ) )
180 172 179 ifeqda 
 |-  ( ( ( ( ( ( ( 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 ) ) ) ) )
181 154 180 ifeqda 
 |-  ( ( ( ( ( ( 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 ) ) ) ) )
182 127 181 ifeqda 
 |-  ( ( ( ( ( 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 ) ) ) ) )
183 ovexd 
 |-  ( ( ( ( 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 )
184 9 182 106 183 fvmptd2 
 |-  ( ( ( ( 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 ) ) ) ) )
185 184 oveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) = ( ( i .^ ( T ` M ) ) .X. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) )
186 185 mpteq2dva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) = ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) )
187 186 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) )
188 nn0p1gt0 
 |-  ( s e. NN0 -> 0 < ( s + 1 ) )
189 0red 
 |-  ( s e. NN0 -> 0 e. RR )
190 ltne 
 |-  ( ( 0 e. RR /\ 0 < ( s + 1 ) ) -> ( s + 1 ) =/= 0 )
191 189 190 sylan 
 |-  ( ( s e. NN0 /\ 0 < ( s + 1 ) ) -> ( s + 1 ) =/= 0 )
192 neeq1 
 |-  ( n = ( s + 1 ) -> ( n =/= 0 <-> ( s + 1 ) =/= 0 ) )
193 191 192 syl5ibrcom 
 |-  ( ( s e. NN0 /\ 0 < ( s + 1 ) ) -> ( n = ( s + 1 ) -> n =/= 0 ) )
194 32 188 193 syl2anc2 
 |-  ( s e. NN -> ( n = ( s + 1 ) -> n =/= 0 ) )
195 194 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( n = ( s + 1 ) -> n =/= 0 ) )
196 195 imp 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n = ( s + 1 ) ) -> n =/= 0 )
197 eqneqall 
 |-  ( n = 0 -> ( n =/= 0 -> ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( T ` ( b ` s ) ) ) )
198 196 197 mpan9 
 |-  ( ( ( ( ( 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 ) ) )
199 iftrue 
 |-  ( 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 ) ) )
200 199 ad2antlr 
 |-  ( ( ( ( ( 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 ) ) )
201 198 200 ifeqda 
 |-  ( ( ( ( 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 ) ) )
202 72 33 syl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( s + 1 ) e. NN0 )
203 fvexd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` ( b ` s ) ) e. _V )
204 9 201 202 203 fvmptd2 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( G ` ( s + 1 ) ) = ( T ` ( b ` s ) ) )
205 204 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) = ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) )
206 8 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
207 13 206 syl3an2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
208 eqid 
 |-  ( mulGrp ` Y ) = ( mulGrp ` Y )
209 208 12 mgpbas 
 |-  ( Base ` Y ) = ( Base ` ( mulGrp ` Y ) )
210 eqid 
 |-  ( 0g ` ( mulGrp ` Y ) ) = ( 0g ` ( mulGrp ` Y ) )
211 209 210 10 mulg0 
 |-  ( ( T ` M ) e. ( Base ` Y ) -> ( 0 .^ ( T ` M ) ) = ( 0g ` ( mulGrp ` Y ) ) )
212 207 211 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( 0 .^ ( T ` M ) ) = ( 0g ` ( mulGrp ` Y ) ) )
213 eqid 
 |-  ( 1r ` Y ) = ( 1r ` Y )
214 208 213 ringidval 
 |-  ( 1r ` Y ) = ( 0g ` ( mulGrp ` Y ) )
215 212 214 eqtr4di 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( 0 .^ ( T ` M ) ) = ( 1r ` Y ) )
216 215 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0 .^ ( T ` M ) ) = ( 1r ` Y ) )
217 216 oveq1d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) = ( ( 1r ` Y ) .X. ( G ` 0 ) ) )
218 52 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Ring )
219 1 2 3 4 5 6 7 8 9 chfacfisf 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> G : NN0 --> ( Base ` Y ) )
220 13 219 syl3anl2 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> G : NN0 --> ( Base ` Y ) )
221 220 79 ffvelrnd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( G ` 0 ) e. ( Base ` Y ) )
222 12 5 213 ringlidm 
 |-  ( ( Y e. Ring /\ ( G ` 0 ) e. ( Base ` Y ) ) -> ( ( 1r ` Y ) .X. ( G ` 0 ) ) = ( G ` 0 ) )
223 218 221 222 syl2an2r 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 1r ` Y ) .X. ( G ` 0 ) ) = ( G ` 0 ) )
224 iftrue 
 |-  ( 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 ) ) ) ) )
225 ovexd 
 |-  ( ( ( 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 )
226 9 224 79 225 fvmptd3 
 |-  ( ( ( 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 ) ) ) ) )
227 217 223 226 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) = ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
228 205 227 oveq12d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) .+ ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) ) = ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .+ ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
229 12 11 cmncom 
 |-  ( ( Y e. CMnd /\ ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) e. ( Base ` Y ) /\ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) e. ( Base ` Y ) ) -> ( ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) .+ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) ) = ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) .+ ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) ) )
230 20 81 94 229 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) .+ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) ) = ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) .+ ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) ) )
231 ringgrp 
 |-  ( Y e. Ring -> Y e. Grp )
232 17 231 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Grp )
233 232 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Grp )
234 205 94 eqeltrrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) e. ( Base ` Y ) )
235 17 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Ring )
236 207 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` M ) e. ( Base ` Y ) )
237 simpl1 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> N e. Fin )
238 13 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R e. Ring )
239 238 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> R e. Ring )
240 elmapi 
 |-  ( b e. ( B ^m ( 0 ... s ) ) -> b : ( 0 ... s ) --> B )
241 240 adantl 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> b : ( 0 ... s ) --> B )
242 241 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> b : ( 0 ... s ) --> B )
243 0elfz 
 |-  ( s e. NN0 -> 0 e. ( 0 ... s ) )
244 32 243 syl 
 |-  ( s e. NN -> 0 e. ( 0 ... s ) )
245 244 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> 0 e. ( 0 ... s ) )
246 242 245 ffvelrnd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( b ` 0 ) e. B )
247 8 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` 0 ) e. B ) -> ( T ` ( b ` 0 ) ) e. ( Base ` Y ) )
248 237 239 246 247 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` ( b ` 0 ) ) e. ( Base ` Y ) )
249 12 5 ringcl 
 |-  ( ( Y e. Ring /\ ( T ` M ) e. ( Base ` Y ) /\ ( T ` ( b ` 0 ) ) e. ( Base ` Y ) ) -> ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) e. ( Base ` Y ) )
250 235 236 248 249 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) e. ( Base ` Y ) )
251 12 7 6 11 grpsubadd0sub 
 |-  ( ( Y e. Grp /\ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) e. ( Base ` Y ) /\ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) e. ( Base ` Y ) ) -> ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .+ ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
252 233 234 250 251 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .+ ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
253 228 230 252 3eqtr4d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) .+ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) ) = ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
254 187 253 oveq12d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) .+ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
255 111 254 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) ) .+ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
256 73 100 255 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
257 38 71 256 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. NN0 |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )