MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  chfacfpmmulgsum Structured version   Unicode version
Theorem chfacfpmmulgsum 19148
Description: Breaking up a sum of values of the "characteristic factor function" multiplied with a constant polynomial matrix. (Contributed by AV, 23-Nov-2019.)
Hypotheses
Ref Expression
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
Ref Expression
chfacfpmmulgsum |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. NN0 |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( Y gsumg ( 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 ) ) ) ) ) )
Distinct variable groups:   B, n   n, M   n, N   R, n   n, Y   n, b   n, s   .0. , n   B, i   i, G   i, M   i, N   R, i   T, i   .X. , i   .^ , i   i, s   i, b   T, n, i   i, Y   .X. , n   .- , n
Allowed substitution hints:   A( i, n, s, b)   B( s, b)   P( i, n, s, b)   .+ ( i, n, s, b)   R( s, b)   T( s, b)   .X. ( s, b)   .^ ( n, s, b)   G( n, s, b)   M( s, b)   .- ( i, s, b)   N( s, b)   Y( s, b)   .0. ( i, s, b)
Proof of Theorem chfacfpmmulgsum
StepHypRef Expression
1 eqid 2467 . . 3 |- ( Base ` Y ) = ( Base ` Y )
2 cayhamlem1.0 . . 3 |- .0. = ( 0g ` Y )
3 chfacfpmmulgsum.p . . 3 |- .+ = ( +g ` Y )
4 crngrng 17005 . . . . . . . 8 |- ( R e. CRing -> R e. Ring )
54anim2i 569 . . . . . . 7 |- ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
653adant3 1016 . . . . . 6 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ R e. Ring ) )
7 cayhamlem1.p . . . . . . 7 |- P = (Poly1 ` R )
8 cayhamlem1.y . . . . . . 7 |- Y = ( N Mat P )
97, 8pmatrng 18977 . . . . . 6 |- ( ( N e. Fin /\ R e. Ring ) -> Y e. Ring )
106, 9syl 16 . . . . 5 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Ring )
11 rngcmn 17025 . . . . 5 |- ( Y e. Ring -> Y e. CMnd )
1210, 11syl 16 . . . 4 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. CMnd )
1312adantr 465 . . 3 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. CMnd )
14 nn0ex 10800 . . . 4 |- NN0 e. _V
1514a1i 11 . . 3 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> NN0 e. _V )
16 simpll 753 . . . . 5 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. NN0 ) -> ( N e. Fin /\ R e. CRing /\ M e. B ) )
17 simplr 754 . . . . 5 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. NN0 ) -> ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) )
18 simpr 461 . . . . 5 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. NN0 ) -> i e. NN0 )
1916, 17, 183jca 1176 . . . 4 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. NN0 ) -> ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ i e. NN0 ) )
20 cayhamlem1.a . . . . 5 |- A = ( N Mat R )
21 cayhamlem1.b . . . . 5 |- B = ( Base ` A )
22 cayhamlem1.r . . . . 5 |- .X. = ( .r ` Y )
23 cayhamlem1.s . . . . 5 |- .- = ( -g ` Y )
24 cayhamlem1.t . . . . 5 |- T = ( N matToPolyMat R )
25 cayhamlem1.g . . . . 5 |- G = ( n e. NN0 |-> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) )
26 cayhamlem1.e . . . . 5 |- .^ = (.g ` (mulGrp ` Y ) )
2720, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmulcl 19145 . . . 4 |- ( ( ( 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 ) )
2819, 27syl 16 . . 3 |- ( ( ( ( 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 ) )
2920, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmulfsupp 19147 . . 3 |- ( ( ( 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 11787 . . . 4 |- ( ( 0 ... ( s + 1 ) ) i^i ( ZZ>= ` ( ( s + 1 ) + 1 ) ) ) = (/)
3130a1i 11 . . 3 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 0 ... ( s + 1 ) ) i^i ( ZZ>= ` ( ( s + 1 ) + 1 ) ) ) = (/) )
32 nnnn0 10801 . . . . . 6 |- ( s e. NN -> s e. NN0 )
33 peano2nn0 10835 . . . . . 6 |- ( s e. NN0 -> ( s + 1 ) e. NN0 )
3432, 33syl 16 . . . . 5 |- ( s e. NN -> ( s + 1 ) e. NN0 )
35 nn0split 11786 . . . . 5 |- ( ( s + 1 ) e. NN0 -> NN0 = ( ( 0 ... ( s + 1 ) ) u. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) ) )
3634, 35syl 16 . . . 4 |- ( s e. NN -> NN0 = ( ( 0 ... ( s + 1 ) ) u. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) ) )
3736ad2antrl 727 . . 3 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> NN0 = ( ( 0 ... ( s + 1 ) ) u. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) ) )
381, 2, 3, 13, 15, 28, 29, 31, 37gsumsplit2 16748 . 2 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. NN0 |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( Y gsumg ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( Y gsumg ( i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) ) )
39 simpll 753 . . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) ) -> ( N e. Fin /\ R e. CRing /\ M e. B ) )
40 simplr 754 . . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) ) -> ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) )
41 nncn 10543 . . . . . . . . . . . . 13 |- ( s e. NN -> s e. CC )
42 add1p1 10787 . . . . . . . . . . . . 13 |- ( s e. CC -> ( ( s + 1 ) + 1 ) = ( s + 2 ) )
4341, 42syl 16 . . . . . . . . . . . 12 |- ( s e. NN -> ( ( s + 1 ) + 1 ) = ( s + 2 ) )
4443ad2antrl 727 . . . . . . . . . . 11 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( s + 1 ) + 1 ) = ( s + 2 ) )
4544fveq2d 5869 . . . . . . . . . 10 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ZZ>= ` ( ( s + 1 ) + 1 ) ) = ( ZZ>= ` ( s + 2 ) ) )
4645eleq2d 2537 . . . . . . . . 9 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) <-> i e. ( ZZ>= ` ( s + 2 ) ) ) )
4746biimpa 484 . . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) ) -> i e. ( ZZ>= ` ( s + 2 ) ) )
4820, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmul0 19146 . . . . . . . 8 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ i e. ( ZZ>= ` ( s + 2 ) ) ) -> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) = .0. )
4939, 40, 47, 48syl3anc 1228 . . . . . . 7 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) ) -> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) = .0. )
5049mpteq2dva 4533 . . . . . 6 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) = ( i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) |-> .0. ) )
5150oveq2d 6299 . . . . 5 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( Y gsumg ( i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) |-> .0. ) ) )
524, 9sylan2 474 . . . . . . . . . 10 |- ( ( N e. Fin /\ R e. CRing ) -> Y e. Ring )
53 rngmnd 17004 . . . . . . . . . 10 |- ( Y e. Ring -> Y e. Mnd )
5452, 53syl 16 . . . . . . . . 9 |- ( ( N e. Fin /\ R e. CRing ) -> Y e. Mnd )
55543adant3 1016 . . . . . . . 8 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Mnd )
56 fvex 5875 . . . . . . . 8 |- ( ZZ>= ` ( ( s + 1 ) + 1 ) ) e. _V
5755, 56jctir 538 . . . . . . 7 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Y e. Mnd /\ ( ZZ>= ` ( ( s + 1 ) + 1 ) ) e. _V ) )
5857adantr 465 . . . . . 6 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y e. Mnd /\ ( ZZ>= ` ( ( s + 1 ) + 1 ) ) e. _V ) )
592gsumz 15830 . . . . . 6 |- ( ( Y e. Mnd /\ ( ZZ>= ` ( ( s + 1 ) + 1 ) ) e. _V ) -> ( Y gsumg ( i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) |-> .0. ) ) = .0. )
6058, 59syl 16 . . . . 5 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) |-> .0. ) ) = .0. )
6151, 60eqtrd 2508 . . . 4 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = .0. )
6261oveq2d 6299 . . 3 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsumg ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( Y gsumg ( i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) ) = ( ( Y gsumg ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ .0. ) )
6355adantr 465 . . . 4 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Mnd )
64 fzfid 12050 . . . . 5 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0 ... ( s + 1 ) ) e. Fin )
65 elfznn0 11769 . . . . . . . 8 |- ( i e. ( 0 ... ( s + 1 ) ) -> i e. NN0 )
6665, 19sylan2 474 . . . . . . 7 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( s + 1 ) ) ) -> ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ i e. NN0 ) )
6766, 27syl 16 . . . . . 6 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 0 ... ( s + 1 ) ) ) -> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) e. ( Base ` Y ) )
6867ralrimiva 2878 . . . . 5 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> A. i e. ( 0 ... ( s + 1 ) ) ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) e. ( Base ` Y ) )
691, 13, 64, 68gsummptcl 16794 . . . 4 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) e. ( Base ` Y ) )
701, 3, 2mndrid 15758 . . . 4 |- ( ( Y e. Mnd /\ ( Y gsumg ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) e. ( Base ` Y ) ) -> ( ( Y gsumg ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ .0. ) = ( Y gsumg ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) )
7163, 69, 70syl2anc 661 . . 3 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsumg ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ .0. ) = ( Y gsumg ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) )
7262, 71eqtrd 2508 . 2 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsumg ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( Y gsumg ( i e. ( ZZ>= ` ( ( s + 1 ) + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) ) = ( Y gsumg ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) )
7332ad2antrl 727 . . . 4 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> s e. NN0 )
741, 3, 13, 73, 67gsummptfzsplit 16752 . . 3 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( Y gsumg ( i e. { ( s + 1 ) } |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) ) )
75 elfznn0 11769 . . . . . . 7 |- ( i e. ( 0 ... s ) -> i e. NN0 )
7675, 28sylan2 474 . . . . . 6 |- ( ( ( ( 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 ) )
771, 3, 13, 73, 76gsummptfzsplitl 16753 . . . . 5 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( Y gsumg ( i e. { 0 } |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) ) )
78 0nn0 10809 . . . . . . . 8 |- 0 e. NN0
7978a1i 11 . . . . . . 7 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> 0 e. NN0 )
8020, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmulcl 19145 . . . . . . . 8 |- ( ( ( 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 ) )
8179, 80mpd3an3 1325 . . . . . . 7 |- ( ( ( 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 6290 . . . . . . . . 9 |- ( i = 0 -> ( i .^ ( T ` M ) ) = ( 0 .^ ( T ` M ) ) )
83 fveq2 5865 . . . . . . . . 9 |- ( i = 0 -> ( G ` i ) = ( G ` 0 ) )
8482, 83oveq12d 6301 . . . . . . . 8 |- ( i = 0 -> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) = ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) )
851, 84gsumsn 16781 . . . . . . 7 |- ( ( Y e. Mnd /\ 0 e. NN0 /\ ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) e. ( Base ` Y ) ) -> ( Y gsumg ( i e. { 0 } |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) )
8663, 79, 81, 85syl3anc 1228 . . . . . 6 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. { 0 } |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) )
8786oveq2d 6299 . . . . 5 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( Y gsumg ( i e. { 0 } |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) ) = ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) ) )
8877, 87eqtrd 2508 . . . 4 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) ) )
89 ovex 6308 . . . . . 6 |- ( s + 1 ) e. _V
9089a1i 11 . . . . 5 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( s + 1 ) e. _V )
91 1nn0 10810 . . . . . . . 8 |- 1 e. NN0
9291a1i 11 . . . . . . 7 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> 1 e. NN0 )
9373, 92nn0addcld 10855 . . . . . 6 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( s + 1 ) e. NN0 )
9420, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmulcl 19145 . . . . . 6 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ ( s + 1 ) e. NN0 ) -> ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) e. ( Base ` Y ) )
9593, 94mpd3an3 1325 . . . . 5 |- ( ( ( 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 ) )
96 oveq1 6290 . . . . . . 7 |- ( i = ( s + 1 ) -> ( i .^ ( T ` M ) ) = ( ( s + 1 ) .^ ( T ` M ) ) )
97 fveq2 5865 . . . . . . 7 |- ( i = ( s + 1 ) -> ( G ` i ) = ( G ` ( s + 1 ) ) )
9896, 97oveq12d 6301 . . . . . 6 |- ( i = ( s + 1 ) -> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) = ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) )
991, 98gsumsn 16781 . . . . 5 |- ( ( Y e. Mnd /\ ( s + 1 ) e. _V /\ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) e. ( Base ` Y ) ) -> ( Y gsumg ( i e. { ( s + 1 ) } |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) )
10063, 90, 95, 99syl3anc 1228 . . . 4 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. { ( s + 1 ) } |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) )
10188, 100oveq12d 6301 . . 3 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsumg ( i e. ( 0 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( Y gsumg ( i e. { ( s + 1 ) } |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) ) = ( ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) ) .+ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) ) )
102 fzfid 12050 . . . . . 6 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 1 ... s ) e. Fin )
103 simpll 753 . . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( N e. Fin /\ R e. CRing /\ M e. B ) )
104 simplr 754 . . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) )
105 elfznn 11713 . . . . . . . . . 10 |- ( i e. ( 1 ... s ) -> i e. NN )
106105nnnn0d 10851 . . . . . . . . 9 |- ( i e. ( 1 ... s ) -> i e. NN0 )
107106adantl 466 . . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> i e. NN0 )
108103, 104, 107, 27syl3anc 1228 . . . . . . 7 |- ( ( ( ( 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 ) )
109108ralrimiva 2878 . . . . . 6 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> A. i e. ( 1 ... s ) ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) e. ( Base ` Y ) )
1101, 13, 102, 109gsummptcl 16794 . . . . 5 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) e. ( Base ` Y ) )
1111, 3mndass 15737 . . . . 5 |- ( ( Y e. Mnd /\ ( ( Y gsumg ( 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 gsumg ( 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 gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) .+ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) ) ) )
11263, 110, 81, 95, 111syl13anc 1230 . . . 4 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) ) .+ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) ) = ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) .+ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) ) ) )
11325a1i 11 . . . . . . . . 9 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> G = ( n e. NN0 |-> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) ) )
114105nnne0d 10579 . . . . . . . . . . . . . 14 |- ( i e. ( 1 ... s ) -> i =/= 0 )
115114ad2antlr 726 . . . . . . . . . . . . 13 |- ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) -> i =/= 0 )
116 neeq1 2748 . . . . . . . . . . . . . 14 |- ( n = i -> ( n =/= 0 <-> i =/= 0 ) )
117116adantl 466 . . . . . . . . . . . . 13 |- ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) -> ( n =/= 0 <-> i =/= 0 ) )
118115, 117mpbird 232 . . . . . . . . . . . 12 |- ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) -> n =/= 0 )
119 eqneqall 2674 . . . . . . . . . . . 12 |- ( n = 0 -> ( n =/= 0 -> .0. = ( T ` ( b ` ( i - 1 ) ) ) ) )
120118, 119mpan9 469 . . . . . . . . . . 11 |- ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ n = 0 ) -> .0. = ( T ` ( b ` ( i - 1 ) ) ) )
121 simplr 754 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ n = 0 ) -> n = i )
122 eqeq1 2471 . . . . . . . . . . . . . . . . 17 |- ( 0 = n -> ( 0 = i <-> n = i ) )
123122eqcoms 2479 . . . . . . . . . . . . . . . 16 |- ( n = 0 -> ( 0 = i <-> n = i ) )
124123adantl 466 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ n = 0 ) -> ( 0 = i <-> n = i ) )
125121, 124mpbird 232 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ n = 0 ) -> 0 = i )
126125fveq2d 5869 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ n = 0 ) -> ( b ` 0 ) = ( b ` i ) )
127126fveq2d 5869 . . . . . . . . . . . 12 |- ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ n = 0 ) -> ( T ` ( b ` 0 ) ) = ( T ` ( b ` i ) ) )
128127oveq2d 6299 . . . . . . . . . . 11 |- ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ n = 0 ) -> ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) = ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) )
129120, 128oveq12d 6301 . . . . . . . . . 10 |- ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ n = 0 ) -> ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) )
130 elfz2 11678 . . . . . . . . . . . . . . . . . 18 |- ( i e. ( 1 ... s ) <-> ( ( 1 e. ZZ /\ s e. ZZ /\ i e. ZZ ) /\ ( 1 <_ i /\ i <_ s ) ) )
131 zleltp1 10912 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( i e. ZZ /\ s e. ZZ ) -> ( i <_ s <-> i < ( s + 1 ) ) )
132131ancoms 453 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( s e. ZZ /\ i e. ZZ ) -> ( i <_ s <-> i < ( s + 1 ) ) )
1331323adant1 1014 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 1 e. ZZ /\ s e. ZZ /\ i e. ZZ ) -> ( i <_ s <-> i < ( s + 1 ) ) )
134133biimpcd 224 . . . . . . . . . . . . . . . . . . . . . 22 |- ( i <_ s -> ( ( 1 e. ZZ /\ s e. ZZ /\ i e. ZZ ) -> i < ( s + 1 ) ) )
135134adantl 466 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( 1 <_ i /\ i <_ s ) -> ( ( 1 e. ZZ /\ s e. ZZ /\ i e. ZZ ) -> i < ( s + 1 ) ) )
136135impcom 430 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 1 e. ZZ /\ s e. ZZ /\ i e. ZZ ) /\ ( 1 <_ i /\ i <_ s ) ) -> i < ( s + 1 ) )
137136orcd 392 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( 1 e. ZZ /\ s e. ZZ /\ i e. ZZ ) /\ ( 1 <_ i /\ i <_ s ) ) -> ( i < ( s + 1 ) \/ ( s + 1 ) < i ) )
138 zre 10867 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s e. ZZ -> s e. RR )
139 1red 9610 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s e. ZZ -> 1 e. RR )
140138, 139readdcld 9622 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( s e. ZZ -> ( s + 1 ) e. RR )
141 zre 10867 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( i e. ZZ -> i e. RR )
142140, 141anim12ci 567 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( s e. ZZ /\ i e. ZZ ) -> ( i e. RR /\ ( s + 1 ) e. RR ) )
1431423adant1 1014 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( 1 e. ZZ /\ s e. ZZ /\ i e. ZZ ) -> ( i e. RR /\ ( s + 1 ) e. RR ) )
144 lttri2 9666 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( i e. RR /\ ( s + 1 ) e. RR ) -> ( i =/= ( s + 1 ) <-> ( i < ( s + 1 ) \/ ( s + 1 ) < i ) ) )
145143, 144syl 16 . . . . . . . . . . . . . . . . . . . 20 |- ( ( 1 e. ZZ /\ s e. ZZ /\ i e. ZZ ) -> ( i =/= ( s + 1 ) <-> ( i < ( s + 1 ) \/ ( s + 1 ) < i ) ) )
146145adantr 465 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( 1 e. ZZ /\ s e. ZZ /\ i e. ZZ ) /\ ( 1 <_ i /\ i <_ s ) ) -> ( i =/= ( s + 1 ) <-> ( i < ( s + 1 ) \/ ( s + 1 ) < i ) ) )
147137, 146mpbird 232 . . . . . . . . . . . . . . . . . 18 |- ( ( ( 1 e. ZZ /\ s e. ZZ /\ i e. ZZ ) /\ ( 1 <_ i /\ i <_ s ) ) -> i =/= ( s + 1 ) )
148130, 147sylbi 195 . . . . . . . . . . . . . . . . 17 |- ( i e. ( 1 ... s ) -> i =/= ( s + 1 ) )
149148ad2antlr 726 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) -> i =/= ( s + 1 ) )
150 neeq1 2748 . . . . . . . . . . . . . . . . 17 |- ( n = i -> ( n =/= ( s + 1 ) <-> i =/= ( s + 1 ) ) )
151150adantl 466 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) -> ( n =/= ( s + 1 ) <-> i =/= ( s + 1 ) ) )
152149, 151mpbird 232 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) -> n =/= ( s + 1 ) )
153152adantr 465 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ -. n = 0 ) -> n =/= ( s + 1 ) )
154153neneqd 2669 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ -. n = 0 ) -> -. n = ( s + 1 ) )
155154pm2.21d 106 . . . . . . . . . . . 12 |- ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ -. n = 0 ) -> ( n = ( s + 1 ) -> ( T ` ( b ` s ) ) = ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) )
156155imp 429 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ -. n = 0 ) /\ n = ( s + 1 ) ) -> ( T ` ( b ` s ) ) = ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) )
157105nnred 10550 . . . . . . . . . . . . . . . . . . 19 |- ( i e. ( 1 ... s ) -> i e. RR )
158 eleq1 2539 . . . . . . . . . . . . . . . . . . 19 |- ( n = i -> ( n e. RR <-> i e. RR ) )
159157, 158syl5ibrcom 222 . . . . . . . . . . . . . . . . . 18 |- ( i e. ( 1 ... s ) -> ( n = i -> n e. RR ) )
160159adantl 466 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( n = i -> n e. RR ) )
161160imp 429 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) -> n e. RR )
16273nn0red 10852 . . . . . . . . . . . . . . . . . 18 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> s e. RR )
163162ad2antrr 725 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) -> s e. RR )
164 1red 9610 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) -> 1 e. RR )
165163, 164readdcld 9622 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) -> ( s + 1 ) e. RR )
166130, 136sylbi 195 . . . . . . . . . . . . . . . . . 18 |- ( i e. ( 1 ... s ) -> i < ( s + 1 ) )
167166ad2antlr 726 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) -> i < ( s + 1 ) )
168 breq1 4450 . . . . . . . . . . . . . . . . . 18 |- ( n = i -> ( n < ( s + 1 ) <-> i < ( s + 1 ) ) )
169168adantl 466 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) -> ( n < ( s + 1 ) <-> i < ( s + 1 ) ) )
170167, 169mpbird 232 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) -> n < ( s + 1 ) )
171161, 165, 170ltnsymd 9732 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) -> -. ( s + 1 ) < n )
172171pm2.21d 106 . . . . . . . . . . . . . 14 |- ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) -> ( ( s + 1 ) < n -> .0. = ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) )
173172ad2antrr 725 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ -. n = 0 ) /\ -. n = ( s + 1 ) ) -> ( ( s + 1 ) < n -> .0. = ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) )
174173imp 429 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ -. n = 0 ) /\ -. n = ( s + 1 ) ) /\ ( s + 1 ) < n ) -> .0. = ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) )
175 simp-4r 766 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ -. n = 0 ) /\ -. n = ( s + 1 ) ) /\ -. ( s + 1 ) < n ) -> n = i )
176175oveq1d 6298 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ -. n = 0 ) /\ -. n = ( s + 1 ) ) /\ -. ( s + 1 ) < n ) -> ( n - 1 ) = ( i - 1 ) )
177176fveq2d 5869 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ -. n = 0 ) /\ -. n = ( s + 1 ) ) /\ -. ( s + 1 ) < n ) -> ( b ` ( n - 1 ) ) = ( b ` ( i - 1 ) ) )
178177fveq2d 5869 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ -. n = 0 ) /\ -. n = ( s + 1 ) ) /\ -. ( s + 1 ) < n ) -> ( T ` ( b ` ( n - 1 ) ) ) = ( T ` ( b ` ( i - 1 ) ) ) )
179175fveq2d 5869 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ -. n = 0 ) /\ -. n = ( s + 1 ) ) /\ -. ( s + 1 ) < n ) -> ( b ` n ) = ( b ` i ) )
180179fveq2d 5869 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ -. n = 0 ) /\ -. n = ( s + 1 ) ) /\ -. ( s + 1 ) < n ) -> ( T ` ( b ` n ) ) = ( T ` ( b ` i ) ) )
181180oveq2d 6299 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ -. n = 0 ) /\ -. n = ( s + 1 ) ) /\ -. ( s + 1 ) < n ) -> ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) = ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) )
182178, 181oveq12d 6301 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ -. n = 0 ) /\ -. n = ( s + 1 ) ) /\ -. ( s + 1 ) < n ) -> ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) = ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) )
183174, 182ifeqda 3972 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ -. n = 0 ) /\ -. n = ( s + 1 ) ) -> if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) = ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) )
184156, 183ifeqda 3972 . . . . . . . . . 10 |- ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) /\ -. n = 0 ) -> if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) = ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) )
185129, 184ifeqda 3972 . . . . . . . . 9 |- ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) /\ n = i ) -> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) = ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) )
186 ovex 6308 . . . . . . . . . 10 |- ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) e. _V
187186a1i 11 . . . . . . . . 9 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) e. _V )
188113, 185, 107, 187fvmptd 5954 . . . . . . . 8 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ i e. ( 1 ... s ) ) -> ( G ` i ) = ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) )
189188oveq2d 6299 . . . . . . 7 |- ( ( ( ( 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 ) ) ) ) ) )
190189mpteq2dva 4533 . . . . . 6 |- ( ( ( 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 ) ) ) ) ) ) )
191190oveq2d 6299 . . . . 5 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( ( T ` ( b ` ( i - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` i ) ) ) ) ) ) ) )
19225a1i 11 . . . . . . . . 9 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> G = ( n e. NN0 |-> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) ) )
193 nn0p1gt0 10824 . . . . . . . . . . . . . . 15 |- ( s e. NN0 -> 0 < ( s + 1 ) )
194 0red 9596 . . . . . . . . . . . . . . . . 17 |- ( s e. NN0 -> 0 e. RR )
195 ltne 9680 . . . . . . . . . . . . . . . . 17 |- ( ( 0 e. RR /\ 0 < ( s + 1 ) ) -> ( s + 1 ) =/= 0 )
196194, 195sylan 471 . . . . . . . . . . . . . . . 16 |- ( ( s e. NN0 /\ 0 < ( s + 1 ) ) -> ( s + 1 ) =/= 0 )
197 neeq1 2748 . . . . . . . . . . . . . . . 16 |- ( n = ( s + 1 ) -> ( n =/= 0 <-> ( s + 1 ) =/= 0 ) )
198196, 197syl5ibrcom 222 . . . . . . . . . . . . . . 15 |- ( ( s e. NN0 /\ 0 < ( s + 1 ) ) -> ( n = ( s + 1 ) -> n =/= 0 ) )
199193, 198mpdan 668 . . . . . . . . . . . . . 14 |- ( s e. NN0 -> ( n = ( s + 1 ) -> n =/= 0 ) )
20032, 199syl 16 . . . . . . . . . . . . 13 |- ( s e. NN -> ( n = ( s + 1 ) -> n =/= 0 ) )
201200ad2antrl 727 . . . . . . . . . . . 12 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( n = ( s + 1 ) -> n =/= 0 ) )
202201imp 429 . . . . . . . . . . 11 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n = ( s + 1 ) ) -> n =/= 0 )
203 eqneqall 2674 . . . . . . . . . . 11 |- ( n = 0 -> ( n =/= 0 -> ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( T ` ( b ` s ) ) ) )
204202, 203mpan9 469 . . . . . . . . . 10 |- ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n = ( s + 1 ) ) /\ n = 0 ) -> ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) = ( T ` ( b ` s ) ) )
205 iftrue 3945 . . . . . . . . . . 11 |- ( n = ( s + 1 ) -> if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) = ( T ` ( b ` s ) ) )
206205ad2antlr 726 . . . . . . . . . 10 |- ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n = ( s + 1 ) ) /\ -. n = 0 ) -> if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) = ( T ` ( b ` s ) ) )
207204, 206ifeqda 3972 . . . . . . . . 9 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n = ( s + 1 ) ) -> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) = ( T ` ( b ` s ) ) )
20873, 33syl 16 . . . . . . . . 9 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( s + 1 ) e. NN0 )
209 fvex 5875 . . . . . . . . . 10 |- ( T ` ( b ` s ) ) e. _V
210209a1i 11 . . . . . . . . 9 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` ( b ` s ) ) e. _V )
211192, 207, 208, 210fvmptd 5954 . . . . . . . 8 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( G ` ( s + 1 ) ) = ( T ` ( b ` s ) ) )
212211oveq2d 6299 . . . . . . 7 |- ( ( ( 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 ) ) ) )
21324, 20, 21, 7, 8mat2pmatbas 19010 . . . . . . . . . . . . 13 |- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
2144, 213syl3an2 1262 . . . . . . . . . . . 12 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
215 eqid 2467 . . . . . . . . . . . . . 14 |- (mulGrp ` Y ) = (mulGrp ` Y )
216215, 1mgpbas 16946 . . . . . . . . . . . . 13 |- ( Base ` Y ) = ( Base ` (mulGrp ` Y ) )
217 eqid 2467 . . . . . . . . . . . . 13 |- ( 0g ` (mulGrp ` Y ) ) = ( 0g ` (mulGrp ` Y ) )
218216, 217, 26mulg0 15954 . . . . . . . . . . . 12 |- ( ( T ` M ) e. ( Base ` Y ) -> ( 0 .^ ( T ` M ) ) = ( 0g ` (mulGrp ` Y ) ) )
219214, 218syl 16 . . . . . . . . . . 11 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( 0 .^ ( T ` M ) ) = ( 0g ` (mulGrp ` Y ) ) )
220 eqid 2467 . . . . . . . . . . . 12 |- ( 1r ` Y ) = ( 1r ` Y )
221215, 220rngidval 16954 . . . . . . . . . . 11 |- ( 1r ` Y ) = ( 0g ` (mulGrp ` Y ) )
222219, 221syl6eqr 2526 . . . . . . . . . 10 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( 0 .^ ( T ` M ) ) = ( 1r ` Y ) )
223222adantr 465 . . . . . . . . 9 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 0 .^ ( T ` M ) ) = ( 1r ` Y ) )
224223oveq1d 6298 . . . . . . . 8 |- ( ( ( 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 ) ) )
225523adant3 1016 . . . . . . . . . 10 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Ring )
226225adantr 465 . . . . . . . . 9 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Ring )
22720, 21, 7, 8, 22, 23, 2, 24, 25chfacfisf 19138 . . . . . . . . . . 11 |- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> G : NN0 --> ( Base ` Y ) )
2284, 227syl3anl2 1277 . . . . . . . . . 10 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> G : NN0 --> ( Base ` Y ) )
229228, 79ffvelrnd 6021 . . . . . . . . 9 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( G ` 0 ) e. ( Base ` Y ) )
2301, 22, 220rnglidm 17018 . . . . . . . . 9 |- ( ( Y e. Ring /\ ( G ` 0 ) e. ( Base ` Y ) ) -> ( ( 1r ` Y ) .X. ( G ` 0 ) ) = ( G ` 0 ) )
231226, 229, 230syl2anc 661 . . . . . . . 8 |- ( ( ( 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 ) )
232 iftrue 3945 . . . . . . . . . 10 |- ( n = 0 -> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) = ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
233232adantl 466 . . . . . . . . 9 |- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n = 0 ) -> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) = ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
234 ovex 6308 . . . . . . . . . 10 |- ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) e. _V
235234a1i 11 . . . . . . . . 9 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) e. _V )
236192, 233, 79, 235fvmptd 5954 . . . . . . . 8 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( G ` 0 ) = ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) )
237224, 231, 2363eqtrd 2512 . . . . . . 7 |- ( ( ( 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 ) ) ) ) )
238212, 237oveq12d 6301 . . . . . 6 |- ( ( ( 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 ) ) ) ) ) )
2391, 3cmncom 16617 . . . . . . 7 |- ( ( 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 ) ) ) )
24013, 81, 95, 239syl3anc 1228 . . . . . 6 |- ( ( ( 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 ) ) ) )
241 rnggrp 17000 . . . . . . . . 9 |- ( Y e. Ring -> Y e. Grp )
24210, 241syl 16 . . . . . . . 8 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Grp )
243242adantr 465 . . . . . . 7 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Grp )
244212, 95eqeltrrd 2556 . . . . . . 7 |- ( ( ( 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 ) )
24510adantr 465 . . . . . . . 8 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Ring )
246214adantr 465 . . . . . . . 8 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` M ) e. ( Base ` Y ) )
247 simpl1 999 . . . . . . . . 9 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> N e. Fin )
24843ad2ant2 1018 . . . . . . . . . 10 |- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R e. Ring )
249248adantr 465 . . . . . . . . 9 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> R e. Ring )
250 elmapi 7440 . . . . . . . . . . . 12 |- ( b e. ( B ^m ( 0 ... s ) ) -> b : ( 0 ... s ) --> B )
251250adantl 466 . . . . . . . . . . 11 |- ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> b : ( 0 ... s ) --> B )
252251adantl 466 . . . . . . . . . 10 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> b : ( 0 ... s ) --> B )
253 0elfz 11771 . . . . . . . . . . . 12 |- ( s e. NN0 -> 0 e. ( 0 ... s ) )
25432, 253syl 16 . . . . . . . . . . 11 |- ( s e. NN -> 0 e. ( 0 ... s ) )
255254ad2antrl 727 . . . . . . . . . 10 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> 0 e. ( 0 ... s ) )
256252, 255ffvelrnd 6021 . . . . . . . . 9 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( b ` 0 ) e. B )
25724, 20, 21, 7, 8mat2pmatbas 19010 . . . . . . . . 9 |- ( ( N e. Fin /\ R e. Ring /\ ( b ` 0 ) e. B ) -> ( T ` ( b ` 0 ) ) e. ( Base ` Y ) )
258247, 249, 256, 257syl3anc 1228 . . . . . . . 8 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` ( b ` 0 ) ) e. ( Base ` Y ) )
2591, 22rngcl 17008 . . . . . . . 8 |- ( ( Y e. Ring /\ ( T ` M ) e. ( Base ` Y ) /\ ( T ` ( b ` 0 ) ) e. ( Base ` Y ) ) -> ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) e. ( Base ` Y ) )
260245, 246, 258, 259syl3anc 1228 . . . . . . 7 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) e. ( Base ` Y ) )
2611, 2, 23, 3grpsubadd0sub 15932 . . . . . . 7 |- ( ( 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 ) ) ) ) ) )
262243, 244, 260, 261syl3anc 1228 . . . . . 6 |- ( ( ( 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 ) ) ) ) ) )
263238, 240, 2623eqtr4d 2518 . . . . 5 |- ( ( ( 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 ) ) ) ) )
264191, 263oveq12d 6301 . . . 4 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) .+ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) ) ) = ( ( Y gsumg ( 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 ) ) ) ) ) )
265112, 264eqtrd 2508 . . 3 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( Y gsumg ( i e. ( 1 ... s ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) .+ ( ( 0 .^ ( T ` M ) ) .X. ( G ` 0 ) ) ) .+ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( G ` ( s + 1 ) ) ) ) = ( ( Y gsumg ( 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 ) ) ) ) ) )
26674, 101, 2653eqtrd 2512 . 2 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. ( 0 ... ( s + 1 ) ) |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( Y gsumg ( 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 ) ) ) ) ) )
26738, 72, 2663eqtrd 2512 1 |- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsumg ( i e. NN0 |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( Y gsumg ( 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 ) ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   /\ w3a 973   = wceq 1379   e. wcel 1767   =/= wne 2662   _Vcvv 3113   u. cun 3474   i^i cin 3475   (/)c0 3785   ifcif 3939   {csn 4027   class class class wbr 4447   |-> cmpt 4505   -->wf 5583   ` cfv 5587  (class class class)co 6283   ^m cmap 7420   Fincfn 7516   CCcc 9489   RRcr 9490   0cc0 9491   1c1 9492   + caddc 9494   < clt 9627   <_ cle 9628   - cmin 9804   NNcn 10535   2c2 10584   NN0cn0 10794   ZZcz 10863   ZZ>=cuz 11081   ...cfz 11671   Basecbs 14489   +g cplusg 14554   .rcmulr 14555   0gc0g 14694   gsumg cgsu 14695   Mndcmnd 15725   Grpcgrp 15726   -gcsg 15729  .gcmg 15730  CMndccmn 16601  mulGrpcmgp 16940   1rcur 16952   Ringcrg 16995   CRingccrg 16996  Poly1cpl1 18003   Mat cmat 18692   matToPolyMat cmat2pmat 18988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr