Metamath Proof Explorer

Theorem cpmidgsumm2pm

Description: Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as group sum with a matrix to polynomial matrix transformation. (Contributed by AV, 13-Nov-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 )
Assertion cpmidgsumm2pm 
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> H = ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( ( coe1 ` K ) ` n ) .* O ) ) ) ) ) )

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 1 2 3 4 5 6 7 8 9 10 11 12 cpmidgsum 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> H = ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( ( U ` ( ( coe1 ` K ) ` n ) ) .x. .1. ) ) ) ) )
17 3simpa 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ R e. CRing ) )
18 17 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( N e. Fin /\ R e. CRing ) )
19 eqid 
 |-  ( Base ` P ) = ( Base ` P )
20 10 1 2 3 19 chpmatply1 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( C ` M ) e. ( Base ` P ) )
21 11 20 eqeltrid 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> K e. ( Base ` P ) )
22 eqid 
 |-  ( coe1 ` K ) = ( coe1 ` K )
23 eqid 
 |-  ( Base ` R ) = ( Base ` R )
24 22 19 3 23 coe1fvalcl 
 |-  ( ( K e. ( Base ` P ) /\ n e. NN0 ) -> ( ( coe1 ` K ) ` n ) e. ( Base ` R ) )
25 21 24 sylan 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( ( coe1 ` K ) ` n ) e. ( Base ` R ) )
26 crngring 
 |-  ( R e. CRing -> R e. Ring )
27 26 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
28 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
29 2 13 ringidcl 
 |-  ( A e. Ring -> O e. B )
30 27 28 29 3syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> O e. B )
31 30 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> O e. B )
32 31 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> O e. B )
33 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
34 15 1 2 3 4 33 23 9 14 7 mat2pmatlin 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( ( ( coe1 ` K ) ` n ) e. ( Base ` R ) /\ O e. B ) ) -> ( T ` ( ( ( coe1 ` K ) ` n ) .* O ) ) = ( ( U ` ( ( coe1 ` K ) ` n ) ) .x. ( T ` O ) ) )
35 18 25 32 34 syl12anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( T ` ( ( ( coe1 ` K ) ` n ) .* O ) ) = ( ( U ` ( ( coe1 ` K ) ` n ) ) .x. ( T ` O ) ) )
36 15 1 2 3 4 33 mat2pmatrhm 
 |-  ( ( N e. Fin /\ R e. CRing ) -> T e. ( A RingHom Y ) )
37 13 8 rhm1 
 |-  ( T e. ( A RingHom Y ) -> ( T ` O ) = .1. )
38 17 36 37 3syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( T ` O ) = .1. )
39 38 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( T ` O ) = .1. )
40 39 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( ( U ` ( ( coe1 ` K ) ` n ) ) .x. ( T ` O ) ) = ( ( U ` ( ( coe1 ` K ) ` n ) ) .x. .1. ) )
41 35 40 eqtr2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( ( U ` ( ( coe1 ` K ) ` n ) ) .x. .1. ) = ( T ` ( ( ( coe1 ` K ) ` n ) .* O ) ) )
42 41 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( ( n .^ X ) .x. ( ( U ` ( ( coe1 ` K ) ` n ) ) .x. .1. ) ) = ( ( n .^ X ) .x. ( T ` ( ( ( coe1 ` K ) ` n ) .* O ) ) ) )
43 42 mpteq2dva 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( n e. NN0 |-> ( ( n .^ X ) .x. ( ( U ` ( ( coe1 ` K ) ` n ) ) .x. .1. ) ) ) = ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( ( coe1 ` K ) ` n ) .* O ) ) ) ) )
44 43 oveq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( ( U ` ( ( coe1 ` K ) ` n ) ) .x. .1. ) ) ) ) = ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( ( coe1 ` K ) ` n ) .* O ) ) ) ) ) )
45 16 44 eqtrd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> H = ( Y gsum ( n e. NN0 |-> ( ( n .^ X ) .x. ( T ` ( ( ( coe1 ` K ) ` n ) .* O ) ) ) ) ) )