Metamath Proof Explorer

Theorem cayleyhamiltonALT

Description: Alternate proof of cayleyhamilton , the Cayley-Hamilton theorem. This proof does not use cayleyhamilton0 directly, but has the same structure as the proof of cayleyhamilton0 . In contrast to the proof of cayleyhamilton0 , only the definitions required to formulate the theorem itself are used, causing the definitions used in the lemmas being expanded, which makes the proof longer and more difficult to read. (Contributed by AV, 25-Nov-2019) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses cayleyhamilton.a 
|- A = ( N Mat R )
cayleyhamilton.b 
|- B = ( Base ` A )
cayleyhamilton.0 
|- .0. = ( 0g ` A )
cayleyhamilton.c 
|- C = ( N CharPlyMat R )
cayleyhamilton.k 
|- K = ( coe1 ` ( C ` M ) )
cayleyhamilton.m 
|- .* = ( .s ` A )
cayleyhamilton.e 
|- .^ = ( .g ` ( mulGrp ` A ) )
Assertion cayleyhamiltonALT 
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) = .0. )

Proof

Step Hyp Ref Expression
1 cayleyhamilton.a 
 |-  A = ( N Mat R )
2 cayleyhamilton.b 
 |-  B = ( Base ` A )
3 cayleyhamilton.0 
 |-  .0. = ( 0g ` A )
4 cayleyhamilton.c 
 |-  C = ( N CharPlyMat R )
5 cayleyhamilton.k 
 |-  K = ( coe1 ` ( C ` M ) )
6 cayleyhamilton.m 
 |-  .* = ( .s ` A )
7 cayleyhamilton.e 
 |-  .^ = ( .g ` ( mulGrp ` A ) )
8 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
9 eqid 
 |-  ( N Mat ( Poly1 ` R ) ) = ( N Mat ( Poly1 ` R ) )
10 eqid 
 |-  ( .r ` ( N Mat ( Poly1 ` R ) ) ) = ( .r ` ( N Mat ( Poly1 ` R ) ) )
11 eqid 
 |-  ( -g ` ( N Mat ( Poly1 ` R ) ) ) = ( -g ` ( N Mat ( Poly1 ` R ) ) )
12 eqid 
 |-  ( 0g ` ( N Mat ( Poly1 ` R ) ) ) = ( 0g ` ( N Mat ( Poly1 ` R ) ) )
13 eqid 
 |-  ( N matToPolyMat R ) = ( N matToPolyMat R )
14 eqid 
 |-  ( C ` M ) = ( C ` M )
15 eqeq1 
 |-  ( l = n -> ( l = 0 <-> n = 0 ) )
16 eqeq1 
 |-  ( l = n -> ( l = ( s + 1 ) <-> n = ( s + 1 ) ) )
17 breq2 
 |-  ( l = n -> ( ( s + 1 ) < l <-> ( s + 1 ) < n ) )
18 oveq1 
 |-  ( l = n -> ( l - 1 ) = ( n - 1 ) )
19 18 fveq2d 
 |-  ( l = n -> ( b ` ( l - 1 ) ) = ( b ` ( n - 1 ) ) )
20 19 fveq2d 
 |-  ( l = n -> ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) = ( ( N matToPolyMat R ) ` ( b ` ( n - 1 ) ) ) )
21 fveq2 
 |-  ( l = n -> ( b ` l ) = ( b ` n ) )
22 21 fveq2d 
 |-  ( l = n -> ( ( N matToPolyMat R ) ` ( b ` l ) ) = ( ( N matToPolyMat R ) ` ( b ` n ) ) )
23 22 oveq2d 
 |-  ( l = n -> ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) = ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` n ) ) ) )
24 20 23 oveq12d 
 |-  ( l = n -> ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) = ( ( ( N matToPolyMat R ) ` ( b ` ( n - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` n ) ) ) ) )
25 17 24 ifbieq2d 
 |-  ( l = n -> if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) = if ( ( s + 1 ) < n , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( n - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` n ) ) ) ) ) )
26 16 25 ifbieq2d 
 |-  ( l = n -> if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) = if ( n = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < n , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( n - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` n ) ) ) ) ) ) )
27 15 26 ifbieq2d 
 |-  ( l = n -> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) = if ( n = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < n , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( n - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` n ) ) ) ) ) ) ) )
28 27 cbvmptv 
 |-  ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) = ( n e. NN0 |-> if ( n = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < n , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( n - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` n ) ) ) ) ) ) ) )
29 eqid 
 |-  ( Base ` ( N Mat ( Poly1 ` R ) ) ) = ( Base ` ( N Mat ( Poly1 ` R ) ) )
30 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
31 eqid 
 |-  ( N cPolyMatToMat R ) = ( N cPolyMatToMat R )
32 eqid 
 |-  ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) = ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) )
33 1 2 8 9 10 11 12 13 4 14 28 29 30 6 31 7 32 cayhamlem4 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) ) = ( ( N cPolyMatToMat R ) ` ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) ) )
34 eqid 
 |-  ( N ConstPolyMat R ) = ( N ConstPolyMat R )
35 31 34 cpm2mfval 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N cPolyMatToMat R ) = ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) )
36 35 eqcomd 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) = ( N cPolyMatToMat R ) )
37 36 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) = ( N cPolyMatToMat R ) )
38 37 fveq1d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) ) = ( ( N cPolyMatToMat R ) ` ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) ) )
39 38 eqeq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) ) = ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) ) <-> ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) ) = ( ( N cPolyMatToMat R ) ` ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) ) ) )
40 39 2rexbidv 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) ) = ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) ) <-> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) ) = ( ( N cPolyMatToMat R ) ` ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) ) ) )
41 33 40 mpbird 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) ) = ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) ) )
42 5 eqcomi 
 |-  ( coe1 ` ( C ` M ) ) = K
43 42 a1i 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) -> ( coe1 ` ( C ` M ) ) = K )
44 43 fveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) -> ( ( coe1 ` ( C ` M ) ) ` n ) = ( K ` n ) )
45 44 oveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) -> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) = ( ( K ` n ) .* ( n .^ M ) ) )
46 45 mpteq2dva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) = ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) )
47 46 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) ) = ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) )
48 47 eqeq1d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) ) = ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) ) <-> ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) = ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) ) ) )
49 48 biimpa 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) ) = ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) ) ) -> ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) = ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) ) )
50 oveq1 
 |-  ( n = j -> ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) = ( j ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) )
51 fveq2 
 |-  ( n = j -> ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) = ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` j ) )
52 50 51 oveq12d 
 |-  ( n = j -> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) = ( ( j ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` j ) ) )
53 52 cbvmptv 
 |-  ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) = ( j e. NN0 |-> ( ( j ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` j ) ) )
54 53 oveq2i 
 |-  ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) = ( ( N Mat ( Poly1 ` R ) ) gsum ( j e. NN0 |-> ( ( j ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` j ) ) ) )
55 54 a1i 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) = ( ( N Mat ( Poly1 ` R ) ) gsum ( j e. NN0 |-> ( ( j ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` j ) ) ) ) )
56 1 2 8 9 10 11 12 13 28 32 cayhamlem1 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( N Mat ( Poly1 ` R ) ) gsum ( j e. NN0 |-> ( ( j ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` j ) ) ) ) = ( 0g ` ( N Mat ( Poly1 ` R ) ) ) )
57 55 56 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) = ( 0g ` ( N Mat ( Poly1 ` R ) ) ) )
58 fveq2 
 |-  ( ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) = ( 0g ` ( N Mat ( Poly1 ` R ) ) ) -> ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) ) = ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ) )
59 crngring 
 |-  ( R e. CRing -> R e. Ring )
60 59 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
61 60 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ R e. Ring ) )
62 31 34 cpm2mfval 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( N cPolyMatToMat R ) = ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) )
63 62 eqcomd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) = ( N cPolyMatToMat R ) )
64 63 fveq1d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ) = ( ( N cPolyMatToMat R ) ` ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ) )
65 eqid 
 |-  ( 0g ` A ) = ( 0g ` A )
66 1 31 8 9 65 12 m2cpminv0 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( N cPolyMatToMat R ) ` ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ) = ( 0g ` A ) )
67 64 66 eqtrd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ) = ( 0g ` A ) )
68 61 67 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ) = ( 0g ` A ) )
69 68 3 eqtr4di 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ) = .0. )
70 69 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ) = .0. )
71 58 70 sylan9eqr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) = ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ) -> ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) ) = .0. )
72 57 71 mpdan 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) ) = .0. )
73 72 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) ) = ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) ) ) -> ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) ) = .0. )
74 49 73 eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) ) = ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) ) ) -> ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) = .0. )
75 74 ex 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) ) = ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) ) -> ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) = .0. ) )
76 75 rexlimdvva 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) ) = ( ( m e. ( N ConstPolyMat R ) |-> ( x e. N , y e. N |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ` ( ( N Mat ( Poly1 ` R ) ) gsum ( n e. NN0 |-> ( ( n ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) ( ( N matToPolyMat R ) ` M ) ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` 0 ) ) ) ) , if ( l = ( s + 1 ) , ( ( N matToPolyMat R ) ` ( b ` s ) ) , if ( ( s + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( b ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( b ` l ) ) ) ) ) ) ) ) ` n ) ) ) ) ) -> ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) = .0. ) )
77 41 76 mpd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) = .0. )