Metamath Proof Explorer

Theorem chfacfscmulgsum

Description: Breaking up a sum of values of the "characteristic factor function" scaled by a polynomial. (Contributed by AV, 9-Nov-2019)

Ref Expression
Hypotheses 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 chfacfscmulgsum 
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. NN0 |-> ( ( i .^ X ) .x. ( G ` i ) ) ) ) = ( ( Y gsum ( 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 ) ) ) ) ) )

Proof

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