Metamath Proof Explorer

Theorem cayhamlem1

Description: Lemma 1 for cayleyhamilton . (Contributed by AV, 11-Nov-2019)

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

Proof

Step Hyp Ref Expression
1 cayhamlem1.a 
 |-  A = ( N Mat R )
2 cayhamlem1.b 
 |-  B = ( Base ` A )
3 cayhamlem1.p 
 |-  P = ( Poly1 ` R )
4 cayhamlem1.y 
 |-  Y = ( N Mat P )
5 cayhamlem1.r 
 |-  .X. = ( .r ` Y )
6 cayhamlem1.s 
 |-  .- = ( -g ` Y )
7 cayhamlem1.0 
 |-  .0. = ( 0g ` Y )
8 cayhamlem1.t 
 |-  T = ( N matToPolyMat R )
9 cayhamlem1.g 
 |-  G = ( n e. NN0 |-> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) )
10 cayhamlem1.e 
 |-  .^ = ( .g ` ( mulGrp ` Y ) )
11 eqid 
 |-  ( +g ` Y ) = ( +g ` Y )
12 1 2 3 4 5 6 7 8 9 10 11 chfacfpmmulgsum2 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. NN0 |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ ( T ` M ) ) .X. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` i ) ) ) ) ) ) ( +g ` Y ) ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
13 elfzelz 
 |-  ( i e. ( 1 ... s ) -> i e. ZZ )
14 13 zcnd 
 |-  ( i e. ( 1 ... s ) -> i e. CC )
15 pncan1 
 |-  ( i e. CC -> ( ( i + 1 ) - 1 ) = i )
16 14 15 syl 
 |-  ( i e. ( 1 ... s ) -> ( ( i + 1 ) - 1 ) = i )
17 16 eqcomd 
 |-  ( i e. ( 1 ... s ) -> i = ( ( i + 1 ) - 1 ) )
18 17 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ i e. ( 1 ... s ) ) -> i = ( ( i + 1 ) - 1 ) )
19 18 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ i e. ( 1 ... s ) ) -> ( b ` i ) = ( b ` ( ( i + 1 ) - 1 ) ) )
20 19 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ i e. ( 1 ... s ) ) -> ( T ` ( b ` i ) ) = ( T ` ( b ` ( ( i + 1 ) - 1 ) ) ) )
21 20 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ i e. ( 1 ... s ) ) -> ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` i ) ) ) = ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` ( ( i + 1 ) - 1 ) ) ) ) )
22 21 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ i e. ( 1 ... s ) ) -> ( ( ( i .^ ( T ` M ) ) .X. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` i ) ) ) ) = ( ( ( i .^ ( T ` M ) ) .X. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` ( ( i + 1 ) - 1 ) ) ) ) ) )
23 22 mpteq2dva 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( i e. ( 1 ... s ) |-> ( ( ( i .^ ( T ` M ) ) .X. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` i ) ) ) ) ) = ( i e. ( 1 ... s ) |-> ( ( ( i .^ ( T ` M ) ) .X. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` ( ( i + 1 ) - 1 ) ) ) ) ) ) )
24 23 oveq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ ( T ` M ) ) .X. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` i ) ) ) ) ) ) = ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ ( T ` M ) ) .X. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` ( ( i + 1 ) - 1 ) ) ) ) ) ) ) )
25 24 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ ( T ` M ) ) .X. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` i ) ) ) ) ) ) = ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ ( T ` M ) ) .X. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` ( ( i + 1 ) - 1 ) ) ) ) ) ) ) )
26 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
27 crngring 
 |-  ( R e. CRing -> R e. Ring )
28 27 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
29 28 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ R e. Ring ) )
30 3 4 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Y e. Ring )
31 29 30 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Ring )
32 ringabl 
 |-  ( Y e. Ring -> Y e. Abel )
33 31 32 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Abel )
34 33 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Abel )
35 elnnuz 
 |-  ( s e. NN <-> s e. ( ZZ>= ` 1 ) )
36 35 biimpi 
 |-  ( s e. NN -> s e. ( ZZ>= ` 1 ) )
37 36 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> s e. ( ZZ>= ` 1 ) )
38 31 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Ring )
39 38 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. ( 1 ... ( s + 1 ) ) ) -> Y e. Ring )
40 28 30 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. Ring )
41 40 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Ring )
42 eqid 
 |-  ( mulGrp ` Y ) = ( mulGrp ` Y )
43 42 ringmgp 
 |-  ( Y e. Ring -> ( mulGrp ` Y ) e. Mnd )
44 41 43 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( mulGrp ` Y ) e. Mnd )
45 44 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( mulGrp ` Y ) e. Mnd )
46 45 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. ( 1 ... ( s + 1 ) ) ) -> ( mulGrp ` Y ) e. Mnd )
47 mndmgm 
 |-  ( ( mulGrp ` Y ) e. Mnd -> ( mulGrp ` Y ) e. Mgm )
48 46 47 syl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. ( 1 ... ( s + 1 ) ) ) -> ( mulGrp ` Y ) e. Mgm )
49 elfznn 
 |-  ( k e. ( 1 ... ( s + 1 ) ) -> k e. NN )
50 49 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. ( 1 ... ( s + 1 ) ) ) -> k e. NN )
51 8 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
52 27 51 syl3an2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
53 52 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` M ) e. ( Base ` Y ) )
54 53 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. ( 1 ... ( s + 1 ) ) ) -> ( T ` M ) e. ( Base ` Y ) )
55 42 26 mgpbas 
 |-  ( Base ` Y ) = ( Base ` ( mulGrp ` Y ) )
56 55 10 mulgnncl 
 |-  ( ( ( mulGrp ` Y ) e. Mgm /\ k e. NN /\ ( T ` M ) e. ( Base ` Y ) ) -> ( k .^ ( T ` M ) ) e. ( Base ` Y ) )
57 48 50 54 56 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. ( 1 ... ( s + 1 ) ) ) -> ( k .^ ( T ` M ) ) e. ( Base ` Y ) )
58 simpl1 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> N e. Fin )
59 58 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. ( 1 ... ( s + 1 ) ) ) -> N e. Fin )
60 27 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R e. Ring )
61 60 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> R e. Ring )
62 61 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. ( 1 ... ( s + 1 ) ) ) -> R e. Ring )
63 elmapi 
 |-  ( b e. ( B ^m ( 0 ... s ) ) -> b : ( 0 ... s ) --> B )
64 63 adantl 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> b : ( 0 ... s ) --> B )
65 64 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> b : ( 0 ... s ) --> B )
66 65 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. ( 1 ... ( s + 1 ) ) ) -> b : ( 0 ... s ) --> B )
67 nnz 
 |-  ( k e. NN -> k e. ZZ )
68 peano2nn 
 |-  ( s e. NN -> ( s + 1 ) e. NN )
69 68 nnzd 
 |-  ( s e. NN -> ( s + 1 ) e. ZZ )
70 elfzm1b 
 |-  ( ( k e. ZZ /\ ( s + 1 ) e. ZZ ) -> ( k e. ( 1 ... ( s + 1 ) ) <-> ( k - 1 ) e. ( 0 ... ( ( s + 1 ) - 1 ) ) ) )
71 67 69 70 syl2an 
 |-  ( ( k e. NN /\ s e. NN ) -> ( k e. ( 1 ... ( s + 1 ) ) <-> ( k - 1 ) e. ( 0 ... ( ( s + 1 ) - 1 ) ) ) )
72 nncn 
 |-  ( s e. NN -> s e. CC )
73 pncan1 
 |-  ( s e. CC -> ( ( s + 1 ) - 1 ) = s )
74 72 73 syl 
 |-  ( s e. NN -> ( ( s + 1 ) - 1 ) = s )
75 74 adantl 
 |-  ( ( k e. NN /\ s e. NN ) -> ( ( s + 1 ) - 1 ) = s )
76 75 oveq2d 
 |-  ( ( k e. NN /\ s e. NN ) -> ( 0 ... ( ( s + 1 ) - 1 ) ) = ( 0 ... s ) )
77 76 eleq2d 
 |-  ( ( k e. NN /\ s e. NN ) -> ( ( k - 1 ) e. ( 0 ... ( ( s + 1 ) - 1 ) ) <-> ( k - 1 ) e. ( 0 ... s ) ) )
78 77 biimpd 
 |-  ( ( k e. NN /\ s e. NN ) -> ( ( k - 1 ) e. ( 0 ... ( ( s + 1 ) - 1 ) ) -> ( k - 1 ) e. ( 0 ... s ) ) )
79 71 78 sylbid 
 |-  ( ( k e. NN /\ s e. NN ) -> ( k e. ( 1 ... ( s + 1 ) ) -> ( k - 1 ) e. ( 0 ... s ) ) )
80 79 expcom 
 |-  ( s e. NN -> ( k e. NN -> ( k e. ( 1 ... ( s + 1 ) ) -> ( k - 1 ) e. ( 0 ... s ) ) ) )
81 80 com13 
 |-  ( k e. ( 1 ... ( s + 1 ) ) -> ( k e. NN -> ( s e. NN -> ( k - 1 ) e. ( 0 ... s ) ) ) )
82 49 81 mpd 
 |-  ( k e. ( 1 ... ( s + 1 ) ) -> ( s e. NN -> ( k - 1 ) e. ( 0 ... s ) ) )
83 82 com12 
 |-  ( s e. NN -> ( k e. ( 1 ... ( s + 1 ) ) -> ( k - 1 ) e. ( 0 ... s ) ) )
84 83 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( k e. ( 1 ... ( s + 1 ) ) -> ( k - 1 ) e. ( 0 ... s ) ) )
85 84 imp 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. ( 1 ... ( s + 1 ) ) ) -> ( k - 1 ) e. ( 0 ... s ) )
86 66 85 ffvelrnd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. ( 1 ... ( s + 1 ) ) ) -> ( b ` ( k - 1 ) ) e. B )
87 8 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` ( k - 1 ) ) e. B ) -> ( T ` ( b ` ( k - 1 ) ) ) e. ( Base ` Y ) )
88 59 62 86 87 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. ( 1 ... ( s + 1 ) ) ) -> ( T ` ( b ` ( k - 1 ) ) ) e. ( Base ` Y ) )
89 26 5 ringcl 
 |-  ( ( Y e. Ring /\ ( k .^ ( T ` M ) ) e. ( Base ` Y ) /\ ( T ` ( b ` ( k - 1 ) ) ) e. ( Base ` Y ) ) -> ( ( k .^ ( T ` M ) ) .X. ( T ` ( b ` ( k - 1 ) ) ) ) e. ( Base ` Y ) )
90 39 57 88 89 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ k e. ( 1 ... ( s + 1 ) ) ) -> ( ( k .^ ( T ` M ) ) .X. ( T ` ( b ` ( k - 1 ) ) ) ) e. ( Base ` Y ) )
91 90 ralrimiva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> A. k e. ( 1 ... ( s + 1 ) ) ( ( k .^ ( T ` M ) ) .X. ( T ` ( b ` ( k - 1 ) ) ) ) e. ( Base ` Y ) )
92 oveq1 
 |-  ( k = i -> ( k .^ ( T ` M ) ) = ( i .^ ( T ` M ) ) )
93 fvoveq1 
 |-  ( k = i -> ( b ` ( k - 1 ) ) = ( b ` ( i - 1 ) ) )
94 93 fveq2d 
 |-  ( k = i -> ( T ` ( b ` ( k - 1 ) ) ) = ( T ` ( b ` ( i - 1 ) ) ) )
95 92 94 oveq12d 
 |-  ( k = i -> ( ( k .^ ( T ` M ) ) .X. ( T ` ( b ` ( k - 1 ) ) ) ) = ( ( i .^ ( T ` M ) ) .X. ( T ` ( b ` ( i - 1 ) ) ) ) )
96 oveq1 
 |-  ( k = ( i + 1 ) -> ( k .^ ( T ` M ) ) = ( ( i + 1 ) .^ ( T ` M ) ) )
97 fvoveq1 
 |-  ( k = ( i + 1 ) -> ( b ` ( k - 1 ) ) = ( b ` ( ( i + 1 ) - 1 ) ) )
98 97 fveq2d 
 |-  ( k = ( i + 1 ) -> ( T ` ( b ` ( k - 1 ) ) ) = ( T ` ( b ` ( ( i + 1 ) - 1 ) ) ) )
99 96 98 oveq12d 
 |-  ( k = ( i + 1 ) -> ( ( k .^ ( T ` M ) ) .X. ( T ` ( b ` ( k - 1 ) ) ) ) = ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` ( ( i + 1 ) - 1 ) ) ) ) )
100 oveq1 
 |-  ( k = 1 -> ( k .^ ( T ` M ) ) = ( 1 .^ ( T ` M ) ) )
101 fvoveq1 
 |-  ( k = 1 -> ( b ` ( k - 1 ) ) = ( b ` ( 1 - 1 ) ) )
102 101 fveq2d 
 |-  ( k = 1 -> ( T ` ( b ` ( k - 1 ) ) ) = ( T ` ( b ` ( 1 - 1 ) ) ) )
103 100 102 oveq12d 
 |-  ( k = 1 -> ( ( k .^ ( T ` M ) ) .X. ( T ` ( b ` ( k - 1 ) ) ) ) = ( ( 1 .^ ( T ` M ) ) .X. ( T ` ( b ` ( 1 - 1 ) ) ) ) )
104 oveq1 
 |-  ( k = ( s + 1 ) -> ( k .^ ( T ` M ) ) = ( ( s + 1 ) .^ ( T ` M ) ) )
105 fvoveq1 
 |-  ( k = ( s + 1 ) -> ( b ` ( k - 1 ) ) = ( b ` ( ( s + 1 ) - 1 ) ) )
106 105 fveq2d 
 |-  ( k = ( s + 1 ) -> ( T ` ( b ` ( k - 1 ) ) ) = ( T ` ( b ` ( ( s + 1 ) - 1 ) ) ) )
107 104 106 oveq12d 
 |-  ( k = ( s + 1 ) -> ( ( k .^ ( T ` M ) ) .X. ( T ` ( b ` ( k - 1 ) ) ) ) = ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` ( ( s + 1 ) - 1 ) ) ) ) )
108 26 34 6 37 91 95 99 103 107 telgsumfz 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ ( T ` M ) ) .X. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` ( ( i + 1 ) - 1 ) ) ) ) ) ) ) = ( ( ( 1 .^ ( T ` M ) ) .X. ( T ` ( b ` ( 1 - 1 ) ) ) ) .- ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` ( ( s + 1 ) - 1 ) ) ) ) ) )
109 25 108 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ ( T ` M ) ) .X. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` i ) ) ) ) ) ) = ( ( ( 1 .^ ( T ` M ) ) .X. ( T ` ( b ` ( 1 - 1 ) ) ) ) .- ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` ( ( s + 1 ) - 1 ) ) ) ) ) )
110 109 oveq1d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( Y gsum ( i e. ( 1 ... s ) |-> ( ( ( i .^ ( T ` M ) ) .X. ( T ` ( b ` ( i - 1 ) ) ) ) .- ( ( ( i + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` i ) ) ) ) ) ) ( +g ` Y ) ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) = ( ( ( ( 1 .^ ( T ` M ) ) .X. ( T ` ( b ` ( 1 - 1 ) ) ) ) .- ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` ( ( s + 1 ) - 1 ) ) ) ) ) ( +g ` Y ) ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
111 55 10 mulg1 
 |-  ( ( T ` M ) e. ( Base ` Y ) -> ( 1 .^ ( T ` M ) ) = ( T ` M ) )
112 52 111 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( 1 .^ ( T ` M ) ) = ( T ` M ) )
113 112 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 1 .^ ( T ` M ) ) = ( T ` M ) )
114 1cnd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> 1 e. CC )
115 114 subidd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( 1 - 1 ) = 0 )
116 115 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( b ` ( 1 - 1 ) ) = ( b ` 0 ) )
117 116 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` ( b ` ( 1 - 1 ) ) ) = ( T ` ( b ` 0 ) ) )
118 113 117 oveq12d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( 1 .^ ( T ` M ) ) .X. ( T ` ( b ` ( 1 - 1 ) ) ) ) = ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) )
119 72 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> s e. CC )
120 119 114 pncand 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( s + 1 ) - 1 ) = s )
121 120 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( b ` ( ( s + 1 ) - 1 ) ) = ( b ` s ) )
122 121 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` ( b ` ( ( s + 1 ) - 1 ) ) ) = ( T ` ( b ` s ) ) )
123 122 oveq2d 
 |-  ( ( ( 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 + 1 ) - 1 ) ) ) ) = ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) )
124 118 123 oveq12d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( 1 .^ ( T ` M ) ) .X. ( T ` ( b ` ( 1 - 1 ) ) ) ) .- ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` ( ( s + 1 ) - 1 ) ) ) ) ) = ( ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) .- ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) ) )
125 124 oveq1d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( 1 .^ ( T ` M ) ) .X. ( T ` ( b ` ( 1 - 1 ) ) ) ) .- ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` ( ( s + 1 ) - 1 ) ) ) ) ) ( +g ` Y ) ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) = ( ( ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) .- ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) ) ( +g ` Y ) ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) )
126 ringgrp 
 |-  ( Y e. Ring -> Y e. Grp )
127 31 126 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Grp )
128 127 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Grp )
129 nnnn0 
 |-  ( s e. NN -> s e. NN0 )
130 0elfz 
 |-  ( s e. NN0 -> 0 e. ( 0 ... s ) )
131 129 130 syl 
 |-  ( s e. NN -> 0 e. ( 0 ... s ) )
132 131 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> 0 e. ( 0 ... s ) )
133 65 132 ffvelrnd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( b ` 0 ) e. B )
134 8 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` 0 ) e. B ) -> ( T ` ( b ` 0 ) ) e. ( Base ` Y ) )
135 58 61 133 134 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 ) )
136 26 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 ) )
137 38 53 135 136 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 ) )
138 45 47 syl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( mulGrp ` Y ) e. Mgm )
139 simprl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> s e. NN )
140 139 peano2nnd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( s + 1 ) e. NN )
141 55 10 mulgnncl 
 |-  ( ( ( mulGrp ` Y ) e. Mgm /\ ( s + 1 ) e. NN /\ ( T ` M ) e. ( Base ` Y ) ) -> ( ( s + 1 ) .^ ( T ` M ) ) e. ( Base ` Y ) )
142 138 140 53 141 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( s + 1 ) .^ ( T ` M ) ) e. ( Base ` Y ) )
143 nn0fz0 
 |-  ( s e. NN0 <-> s e. ( 0 ... s ) )
144 129 143 sylib 
 |-  ( s e. NN -> s e. ( 0 ... s ) )
145 144 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> s e. ( 0 ... s ) )
146 65 145 ffvelrnd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( b ` s ) e. B )
147 8 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` s ) e. B ) -> ( T ` ( b ` s ) ) e. ( Base ` Y ) )
148 58 61 146 147 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` ( b ` s ) ) e. ( Base ` Y ) )
149 26 5 ringcl 
 |-  ( ( Y e. Ring /\ ( ( s + 1 ) .^ ( T ` M ) ) e. ( Base ` Y ) /\ ( T ` ( b ` s ) ) e. ( Base ` Y ) ) -> ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) e. ( Base ` Y ) )
150 38 142 148 149 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) e. ( Base ` Y ) )
151 26 11 6 7 grpnpncan0 
 |-  ( ( Y e. Grp /\ ( ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) e. ( Base ` Y ) /\ ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) e. ( Base ` Y ) ) ) -> ( ( ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) .- ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) ) ( +g ` Y ) ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) = .0. )
152 128 137 150 151 syl12anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) .- ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) ) ( +g ` Y ) ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) = .0. )
153 125 152 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( ( 1 .^ ( T ` M ) ) .X. ( T ` ( b ` ( 1 - 1 ) ) ) ) .- ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` ( ( s + 1 ) - 1 ) ) ) ) ) ( +g ` Y ) ( ( ( ( s + 1 ) .^ ( T ` M ) ) .X. ( T ` ( b ` s ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) ) = .0. )
154 12 110 153 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( i e. NN0 |-> ( ( i .^ ( T ` M ) ) .X. ( G ` i ) ) ) ) = .0. )