Metamath Proof Explorer

Theorem chfacfpmmulgsum2

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 chfacfpmmulgsum2 
|- ( ( ( 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 ) ) ) ) .- ( ( ( 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 1 2 3 4 5 6 7 8 9 10 11 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 ) ) ) ) ) )
13 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
14 crngring 
 |-  ( R e. CRing -> R e. Ring )
15 14 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( 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 ) -> Y e. Ring )
18 17 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Ring )
19 18 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> Y e. Ring )
20 eqid 
 |-  ( mulGrp ` Y ) = ( mulGrp ` Y )
21 20 ringmgp 
 |-  ( Y e. Ring -> ( mulGrp ` Y ) e. Mnd )
22 mndmgm 
 |-  ( ( mulGrp ` Y ) e. Mnd -> ( mulGrp ` Y ) e. Mgm )
23 21 22 syl 
 |-  ( Y e. Ring -> ( mulGrp ` Y ) e. Mgm )
24 18 23 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( mulGrp ` Y ) e. Mgm )
25 24 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( mulGrp ` Y ) e. Mgm )
26 elfznn 
 |-  ( i e. ( 1 ... s ) -> i e. NN )
27 26 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. NN )
28 8 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
29 14 28 syl3an2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
30 29 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( T ` M ) e. ( Base ` Y ) )
31 20 13 mgpbas 
 |-  ( Base ` Y ) = ( Base ` ( mulGrp ` Y ) )
32 31 10 mulgnncl 
 |-  ( ( ( mulGrp ` Y ) e. Mgm /\ i e. NN /\ ( T ` M ) e. ( Base ` Y ) ) -> ( i .^ ( T ` M ) ) e. ( Base ` Y ) )
33 25 27 30 32 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 ) ) e. ( Base ` Y ) )
34 15 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ R e. Ring ) )
35 34 ad2antrr 
 |-  ( ( ( ( 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. Ring ) )
36 elmapi 
 |-  ( b e. ( B ^m ( 0 ... s ) ) -> b : ( 0 ... s ) --> B )
37 36 adantl 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> b : ( 0 ... s ) --> B )
38 37 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> b : ( 0 ... s ) --> B )
39 38 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> b : ( 0 ... s ) --> B )
40 1nn0 
 |-  1 e. NN0
41 40 a1i 
 |-  ( ( s e. NN /\ i e. ( 1 ... s ) ) -> 1 e. NN0 )
42 nnnn0 
 |-  ( s e. NN -> s e. NN0 )
43 42 adantr 
 |-  ( ( s e. NN /\ i e. ( 1 ... s ) ) -> s e. NN0 )
44 nnge1 
 |-  ( s e. NN -> 1 <_ s )
45 44 adantr 
 |-  ( ( s e. NN /\ i e. ( 1 ... s ) ) -> 1 <_ s )
46 elfz2nn0 
 |-  ( 1 e. ( 0 ... s ) <-> ( 1 e. NN0 /\ s e. NN0 /\ 1 <_ s ) )
47 41 43 45 46 syl3anbrc 
 |-  ( ( s e. NN /\ i e. ( 1 ... s ) ) -> 1 e. ( 0 ... s ) )
48 simpr 
 |-  ( ( s e. NN /\ i e. ( 1 ... s ) ) -> i e. ( 1 ... s ) )
49 fz0fzdiffz0 
 |-  ( ( 1 e. ( 0 ... s ) /\ i e. ( 1 ... s ) ) -> ( i - 1 ) e. ( 0 ... s ) )
50 47 48 49 syl2anc 
 |-  ( ( s e. NN /\ i e. ( 1 ... s ) ) -> ( i - 1 ) e. ( 0 ... s ) )
51 50 ex 
 |-  ( s e. NN -> ( i e. ( 1 ... s ) -> ( i - 1 ) e. ( 0 ... s ) ) )
52 51 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( i e. ( 1 ... s ) -> ( i - 1 ) e. ( 0 ... s ) ) )
53 52 imp 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( i - 1 ) e. ( 0 ... s ) )
54 39 53 ffvelrnd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( b ` ( i - 1 ) ) e. B )
55 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` ( i - 1 ) ) e. B ) <-> ( ( N e. Fin /\ R e. Ring ) /\ ( b ` ( i - 1 ) ) e. B ) )
56 35 54 55 sylanbrc 
 |-  ( ( ( ( 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. Ring /\ ( b ` ( i - 1 ) ) e. B ) )
57 8 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` ( i - 1 ) ) e. B ) -> ( T ` ( b ` ( i - 1 ) ) ) e. ( Base ` Y ) )
58 56 57 syl 
 |-  ( ( ( ( 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 ) ) ) e. ( Base ` Y ) )
59 34 16 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Ring )
60 59 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> Y e. Ring )
61 simpl1 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> N e. Fin )
62 14 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R e. Ring )
63 62 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> R e. Ring )
64 42 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> s e. NN0 )
65 61 63 64 3jca 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( N e. Fin /\ R e. Ring /\ s e. NN0 ) )
66 65 adantr 
 |-  ( ( ( ( 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. Ring /\ s e. NN0 ) )
67 simpr 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> b e. ( B ^m ( 0 ... s ) ) )
68 67 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> b e. ( B ^m ( 0 ... s ) ) )
69 fz1ssfz0 
 |-  ( 1 ... s ) C_ ( 0 ... s )
70 69 sseli 
 |-  ( i e. ( 1 ... s ) -> i e. ( 0 ... s ) )
71 68 70 anim12i 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( b e. ( B ^m ( 0 ... s ) ) /\ i e. ( 0 ... s ) ) )
72 1 2 3 4 8 m2pmfzmap 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ s e. NN0 ) /\ ( b e. ( B ^m ( 0 ... s ) ) /\ i e. ( 0 ... s ) ) ) -> ( T ` ( b ` i ) ) e. ( Base ` Y ) )
73 66 71 72 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( T ` ( b ` i ) ) e. ( Base ` Y ) )
74 13 5 ringcl 
 |-  ( ( Y e. Ring /\ ( T ` M ) e. ( Base ` Y ) /\ ( T ` ( b ` i ) ) e. ( Base ` Y ) ) -> ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
75 60 30 73 74 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) e. ( Base ` Y ) )
76 13 5 6 19 33 58 75 ringsubdi 
 |-  ( ( ( ( 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. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) = ( ( ( i .^ ( T ` M ) ) .X. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ ( T ` M ) ) .X. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) )
77 13 5 ringass 
 |-  ( ( Y e. Ring /\ ( ( i .^ ( T ` M ) ) e. ( Base ` Y ) /\ ( T ` M ) e. ( Base ` Y ) /\ ( T ` ( b ` i ) ) e. ( Base ` Y ) ) ) -> ( ( ( i .^ ( T ` M ) ) .X. ( T ` M ) ) .X. ( T ` ( b ` i ) ) ) = ( ( i .^ ( T ` M ) ) .X. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) )
78 60 33 30 73 77 syl13anc 
 |-  ( ( ( ( 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. ( T ` M ) ) .X. ( T ` ( b ` i ) ) ) = ( ( i .^ ( T ` M ) ) .X. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) )
79 78 eqcomd 
 |-  ( ( ( ( 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. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) = ( ( ( i .^ ( T ` M ) ) .X. ( T ` M ) ) .X. ( T ` ( b ` i ) ) ) )
80 29 31 eleqtrdi 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( T ` M ) e. ( Base ` ( mulGrp ` Y ) ) )
81 80 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` M ) e. ( Base ` ( mulGrp ` Y ) ) )
82 eqid 
 |-  ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( mulGrp ` Y ) )
83 eqid 
 |-  ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( mulGrp ` Y ) )
84 82 10 83 mulgnnp1 
 |-  ( ( i e. NN /\ ( T ` M ) e. ( Base ` ( mulGrp ` Y ) ) ) -> ( ( i + 1 ) .^ ( T ` M ) ) = ( ( i .^ ( T ` M ) ) ( +g ` ( mulGrp ` Y ) ) ( T ` M ) ) )
85 26 81 84 syl2anr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( ( i + 1 ) .^ ( T ` M ) ) = ( ( i .^ ( T ` M ) ) ( +g ` ( mulGrp ` Y ) ) ( T ` M ) ) )
86 20 5 mgpplusg 
 |-  .X. = ( +g ` ( mulGrp ` Y ) )
87 86 eqcomi 
 |-  ( +g ` ( mulGrp ` Y ) ) = .X.
88 87 a1i 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( +g ` ( mulGrp ` Y ) ) = .X. )
89 88 oveqd 
 |-  ( ( ( ( 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 ) ) ( +g ` ( mulGrp ` Y ) ) ( T ` M ) ) = ( ( i .^ ( T ` M ) ) .X. ( T ` M ) ) )
90 85 89 eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( ( i + 1 ) .^ ( T ` M ) ) = ( ( i .^ ( T ` M ) ) .X. ( T ` M ) ) )
91 90 eqcomd 
 |-  ( ( ( ( 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. ( T ` M ) ) = ( ( i + 1 ) .^ ( T ` M ) ) )
92 91 oveq1d 
 |-  ( ( ( ( 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. ( T ` M ) ) .X. ( T ` ( b ` i ) ) ) = ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` i ) ) ) )
93 79 92 eqtrd 
 |-  ( ( ( ( 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. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) = ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` i ) ) ) )
94 93 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. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( i .^ ( T ` M ) ) .X. ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) = ( ( ( i .^ ( T ` M ) ) .X. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` i ) ) ) ) )
95 76 94 eqtrd 
 |-  ( ( ( ( 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. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) = ( ( ( i .^ ( T ` M ) ) .X. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` i ) ) ) ) )
96 95 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. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) = ( i e. ( 1 ... s ) |-> ( ( ( i .^ ( T ` M ) ) .X. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` i ) ) ) ) ) )
97 96 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. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) = ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ ( T ` M ) ) .X. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` i ) ) ) ) ) ) )
98 97 oveq1d 
 |-  ( ( ( 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. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ ( T ` M ) ) .X. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
99 12 98 eqtrd 
 |-  ( ( ( 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 ) ) ) ) .- ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` i ) ) ) ) ) ) .+ ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )