Metamath Proof Explorer

Theorem cpmidpmat

Description: Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as polynomial over the ring of matrices. (Contributed by AV, 14-Nov-2019) (Revised by AV, 7-Dec-2019)

Ref Expression
Hypotheses cpmidgsum.a 
|- A = ( N Mat R )
cpmidgsum.b 
|- B = ( Base ` A )
cpmidgsum.p 
|- P = ( Poly1 ` R )
cpmidgsum.y 
|- Y = ( N Mat P )
cpmidgsum.x 
|- X = ( var1 ` R )
cpmidgsum.e 
|- .^ = ( .g ` ( mulGrp ` P ) )
cpmidgsum.m 
|- .x. = ( .s ` Y )
cpmidgsum.1 
|- .1. = ( 1r ` Y )
cpmidgsum.u 
|- U = ( algSc ` P )
cpmidgsum.c 
|- C = ( N CharPlyMat R )
cpmidgsum.k 
|- K = ( C ` M )
cpmidgsum.h 
|- H = ( K .x. .1. )
cpmidgsumm2pm.o 
|- O = ( 1r ` A )
cpmidgsumm2pm.m 
|- .* = ( .s ` A )
cpmidgsumm2pm.t 
|- T = ( N matToPolyMat R )
cpmidgsum.w 
|- W = ( Base ` Y )
cpmidpmat.p 
|- Q = ( Poly1 ` A )
cpmidpmat.z 
|- Z = ( var1 ` A )
cpmidpmat.m 
|- .xb = ( .s ` Q )
cpmidpmat.e 
|- E = ( .g ` ( mulGrp ` Q ) )
cpmidpmat.i 
|- I = ( N pMatToMatPoly R )
Assertion cpmidpmat 
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( I ` H ) = ( Q gsum ( n e. NN0 |-> ( ( ( ( coe1 ` K ) ` n ) .* O ) .xb ( n E Z ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cpmidgsum.a 
 |-  A = ( N Mat R )
2 cpmidgsum.b 
 |-  B = ( Base ` A )
3 cpmidgsum.p 
 |-  P = ( Poly1 ` R )
4 cpmidgsum.y 
 |-  Y = ( N Mat P )
5 cpmidgsum.x 
 |-  X = ( var1 ` R )
6 cpmidgsum.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
7 cpmidgsum.m 
 |-  .x. = ( .s ` Y )
8 cpmidgsum.1 
 |-  .1. = ( 1r ` Y )
9 cpmidgsum.u 
 |-  U = ( algSc ` P )
10 cpmidgsum.c 
 |-  C = ( N CharPlyMat R )
11 cpmidgsum.k 
 |-  K = ( C ` M )
12 cpmidgsum.h 
 |-  H = ( K .x. .1. )
13 cpmidgsumm2pm.o 
 |-  O = ( 1r ` A )
14 cpmidgsumm2pm.m 
 |-  .* = ( .s ` A )
15 cpmidgsumm2pm.t 
 |-  T = ( N matToPolyMat R )
16 cpmidgsum.w 
 |-  W = ( Base ` Y )
17 cpmidpmat.p 
 |-  Q = ( Poly1 ` A )
18 cpmidpmat.z 
 |-  Z = ( var1 ` A )
19 cpmidpmat.m 
 |-  .xb = ( .s ` Q )
20 cpmidpmat.e 
 |-  E = ( .g ` ( mulGrp ` Q ) )
21 cpmidpmat.i 
 |-  I = ( N pMatToMatPoly R )
22 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 cpmidgsumm2pm 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> H = ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( ( coe1 ` K ) ` n ) .* O ) ) ) ) ) )
23 22 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( I ` H ) = ( I ` ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( ( coe1 ` K ) ` n ) .* O ) ) ) ) ) ) )
24 eqid 
 |-  ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) = ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) )
25 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 24 cpmidpmatlem1 
 |-  ( n e. NN0 -> ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) = ( ( ( coe1 ` K ) ` n ) .* O ) )
26 25 eqcomd 
 |-  ( n e. NN0 -> ( ( ( coe1 ` K ) ` n ) .* O ) = ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) )
27 26 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( ( ( coe1 ` K ) ` n ) .* O ) = ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) )
28 27 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( T ` ( ( ( coe1 ` K ) ` n ) .* O ) ) = ( T ` ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) ) )
29 28 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( ( n .^ X ) .x. ( T ` ( ( ( coe1 ` K ) ` n ) .* O ) ) ) = ( ( n .^ X ) .x. ( T ` ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) ) ) )
30 29 mpteq2dva 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( ( coe1 ` K ) ` n ) .* O ) ) ) ) = ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) ) ) ) )
31 30 oveq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( ( coe1 ` K ) ` n ) .* O ) ) ) ) ) = ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) ) ) ) ) )
32 31 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( I ` ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( ( coe1 ` K ) ` n ) .* O ) ) ) ) ) ) = ( I ` ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) ) ) ) ) ) )
33 3simpa 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ R e. CRing ) )
34 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 24 cpmidpmatlem2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) e. ( B ^m NN0 ) )
35 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 24 cpmidpmatlem3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) finSupp ( 0g ` A ) )
36 fveq2 
 |-  ( k = x -> ( ( coe1 ` K ) ` k ) = ( ( coe1 ` K ) ` x ) )
37 36 oveq1d 
 |-  ( k = x -> ( ( ( coe1 ` K ) ` k ) .* O ) = ( ( ( coe1 ` K ) ` x ) .* O ) )
38 37 cbvmptv 
 |-  ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) = ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) )
39 38 eleq1i 
 |-  ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) e. ( B ^m NN0 ) <-> ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) ) e. ( B ^m NN0 ) )
40 38 breq1i 
 |-  ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) finSupp ( 0g ` A ) <-> ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) ) finSupp ( 0g ` A ) )
41 39 40 anbi12i 
 |-  ( ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) e. ( B ^m NN0 ) /\ ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) finSupp ( 0g ` A ) ) <-> ( ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) ) e. ( B ^m NN0 ) /\ ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) ) finSupp ( 0g ` A ) ) )
42 3 4 16 19 20 18 1 2 17 21 6 5 7 15 pm2mp 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) ) e. ( B ^m NN0 ) /\ ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) ) finSupp ( 0g ` A ) ) ) -> ( I ` ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) ) ` n ) ) ) ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) ) ` n ) .xb ( n E Z ) ) ) ) )
43 41 42 sylan2b 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) e. ( B ^m NN0 ) /\ ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) finSupp ( 0g ` A ) ) ) -> ( I ` ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) ) ` n ) ) ) ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) ) ` n ) .xb ( n E Z ) ) ) ) )
44 33 34 35 43 syl12anc 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( I ` ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) ) ` n ) ) ) ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) ) ` n ) .xb ( n E Z ) ) ) ) )
45 38 fveq1i 
 |-  ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) = ( ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) ) ` n )
46 45 fveq2i 
 |-  ( T ` ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) ) = ( T ` ( ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) ) ` n ) )
47 46 oveq2i 
 |-  ( ( n .^ X ) .x. ( T ` ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) ) ) = ( ( n .^ X ) .x. ( T ` ( ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) ) ` n ) ) )
48 47 mpteq2i 
 |-  ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) ) ) ) = ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) ) ` n ) ) ) )
49 48 oveq2i 
 |-  ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) ) ) ) ) = ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) ) ` n ) ) ) ) )
50 49 fveq2i 
 |-  ( I ` ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) ) ) ) ) ) = ( I ` ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) ) ` n ) ) ) ) ) )
51 45 oveq1i 
 |-  ( ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) .xb ( n E Z ) ) = ( ( ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) ) ` n ) .xb ( n E Z ) )
52 51 mpteq2i 
 |-  ( n e. NN0 |-> ( ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) .xb ( n E Z ) ) ) = ( n e. NN0 |-> ( ( ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) ) ` n ) .xb ( n E Z ) ) )
53 52 oveq2i 
 |-  ( Q gsum ( n e. NN0 |-> ( ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) .xb ( n E Z ) ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( ( x e. NN0 |-> ( ( ( coe1 ` K ) ` x ) .* O ) ) ` n ) .xb ( n E Z ) ) ) )
54 44 50 53 3eqtr4g 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( I ` ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) ) ) ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) .xb ( n E Z ) ) ) ) )
55 32 54 eqtrd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( I ` ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( ( coe1 ` K ) ` n ) .* O ) ) ) ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) .xb ( n E Z ) ) ) ) )
56 25 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) = ( ( ( coe1 ` K ) ` n ) .* O ) )
57 56 oveq1d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) .xb ( n E Z ) ) = ( ( ( ( coe1 ` K ) ` n ) .* O ) .xb ( n E Z ) ) )
58 57 mpteq2dva 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( n e. NN0 |-> ( ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) .xb ( n E Z ) ) ) = ( n e. NN0 |-> ( ( ( ( coe1 ` K ) ` n ) .* O ) .xb ( n E Z ) ) ) )
59 58 oveq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Q gsum ( n e. NN0 |-> ( ( ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) ` n ) .xb ( n E Z ) ) ) ) = ( Q gsum ( n e. NN0 |-> ( ( ( ( coe1 ` K ) ` n ) .* O ) .xb ( n E Z ) ) ) ) )
60 23 55 59 3eqtrd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( I ` H ) = ( Q gsum ( n e. NN0 |-> ( ( ( ( coe1 ` K ) ` n ) .* O ) .xb ( n E Z ) ) ) ) )