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 โŠข ๐ด = ( ๐‘ Mat ๐‘… )
cpmidgsum.b โŠข ๐ต = ( Base โ€˜ ๐ด )
cpmidgsum.p โŠข ๐‘ƒ = ( Poly1 โ€˜ ๐‘… )
cpmidgsum.y โŠข ๐‘Œ = ( ๐‘ Mat ๐‘ƒ )
cpmidgsum.x โŠข ๐‘‹ = ( var1 โ€˜ ๐‘… )
cpmidgsum.e โŠข โ†‘ = ( .g โ€˜ ( mulGrp โ€˜ ๐‘ƒ ) )
cpmidgsum.m โŠข ยท = ( ยท๐‘  โ€˜ ๐‘Œ )
cpmidgsum.1 โŠข 1 = ( 1r โ€˜ ๐‘Œ )
cpmidgsum.u โŠข ๐‘ˆ = ( algSc โ€˜ ๐‘ƒ )
cpmidgsum.c โŠข ๐ถ = ( ๐‘ CharPlyMat ๐‘… )
cpmidgsum.k โŠข ๐พ = ( ๐ถ โ€˜ ๐‘€ )
cpmidgsum.h โŠข ๐ป = ( ๐พ ยท 1 )
cpmidgsumm2pm.o โŠข ๐‘‚ = ( 1r โ€˜ ๐ด )
cpmidgsumm2pm.m โŠข โˆ— = ( ยท๐‘  โ€˜ ๐ด )
cpmidgsumm2pm.t โŠข ๐‘‡ = ( ๐‘ matToPolyMat ๐‘… )
Assertion cpmidgsumm2pm ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ๐ป = ( ๐‘Œ ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) ยท ( ๐‘‡ โ€˜ ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— ๐‘‚ ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cpmidgsum.a โŠข ๐ด = ( ๐‘ Mat ๐‘… )
2 cpmidgsum.b โŠข ๐ต = ( Base โ€˜ ๐ด )
3 cpmidgsum.p โŠข ๐‘ƒ = ( Poly1 โ€˜ ๐‘… )
4 cpmidgsum.y โŠข ๐‘Œ = ( ๐‘ Mat ๐‘ƒ )
5 cpmidgsum.x โŠข ๐‘‹ = ( var1 โ€˜ ๐‘… )
6 cpmidgsum.e โŠข โ†‘ = ( .g โ€˜ ( mulGrp โ€˜ ๐‘ƒ ) )
7 cpmidgsum.m โŠข ยท = ( ยท๐‘  โ€˜ ๐‘Œ )
8 cpmidgsum.1 โŠข 1 = ( 1r โ€˜ ๐‘Œ )
9 cpmidgsum.u โŠข ๐‘ˆ = ( algSc โ€˜ ๐‘ƒ )
10 cpmidgsum.c โŠข ๐ถ = ( ๐‘ CharPlyMat ๐‘… )
11 cpmidgsum.k โŠข ๐พ = ( ๐ถ โ€˜ ๐‘€ )
12 cpmidgsum.h โŠข ๐ป = ( ๐พ ยท 1 )
13 cpmidgsumm2pm.o โŠข ๐‘‚ = ( 1r โ€˜ ๐ด )
14 cpmidgsumm2pm.m โŠข โˆ— = ( ยท๐‘  โ€˜ ๐ด )
15 cpmidgsumm2pm.t โŠข ๐‘‡ = ( ๐‘ matToPolyMat ๐‘… )
16 1 2 3 4 5 6 7 8 9 10 11 12 cpmidgsum โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ๐ป = ( ๐‘Œ ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) ยท ( ( ๐‘ˆ โ€˜ ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) ) ยท 1 ) ) ) ) )
17 3simpa โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing ) )
18 17 adantr โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘› โˆˆ โ„•0 ) โ†’ ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing ) )
19 eqid โŠข ( Base โ€˜ ๐‘ƒ ) = ( Base โ€˜ ๐‘ƒ )
20 10 1 2 3 19 chpmatply1 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ๐ถ โ€˜ ๐‘€ ) โˆˆ ( Base โ€˜ ๐‘ƒ ) )
21 11 20 eqeltrid โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ๐พ โˆˆ ( Base โ€˜ ๐‘ƒ ) )
22 eqid โŠข ( coe1 โ€˜ ๐พ ) = ( coe1 โ€˜ ๐พ )
23 eqid โŠข ( Base โ€˜ ๐‘… ) = ( Base โ€˜ ๐‘… )
24 22 19 3 23 coe1fvalcl โŠข ( ( ๐พ โˆˆ ( Base โ€˜ ๐‘ƒ ) โˆง ๐‘› โˆˆ โ„•0 ) โ†’ ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆˆ ( Base โ€˜ ๐‘… ) )
25 21 24 sylan โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘› โˆˆ โ„•0 ) โ†’ ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆˆ ( Base โ€˜ ๐‘… ) )
26 crngring โŠข ( ๐‘… โˆˆ CRing โ†’ ๐‘… โˆˆ Ring )
27 26 anim2i โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing ) โ†’ ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring ) )
28 1 matring โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring ) โ†’ ๐ด โˆˆ Ring )
29 2 13 ringidcl โŠข ( ๐ด โˆˆ Ring โ†’ ๐‘‚ โˆˆ ๐ต )
30 27 28 29 3syl โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing ) โ†’ ๐‘‚ โˆˆ ๐ต )
31 30 3adant3 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ๐‘‚ โˆˆ ๐ต )
32 31 adantr โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘› โˆˆ โ„•0 ) โ†’ ๐‘‚ โˆˆ ๐ต )
33 eqid โŠข ( Base โ€˜ ๐‘Œ ) = ( Base โ€˜ ๐‘Œ )
34 15 1 2 3 4 33 23 9 14 7 mat2pmatlin โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing ) โˆง ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆˆ ( Base โ€˜ ๐‘… ) โˆง ๐‘‚ โˆˆ ๐ต ) ) โ†’ ( ๐‘‡ โ€˜ ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— ๐‘‚ ) ) = ( ( ๐‘ˆ โ€˜ ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) ) ยท ( ๐‘‡ โ€˜ ๐‘‚ ) ) )
35 18 25 32 34 syl12anc โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘› โˆˆ โ„•0 ) โ†’ ( ๐‘‡ โ€˜ ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— ๐‘‚ ) ) = ( ( ๐‘ˆ โ€˜ ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) ) ยท ( ๐‘‡ โ€˜ ๐‘‚ ) ) )
36 15 1 2 3 4 33 mat2pmatrhm โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing ) โ†’ ๐‘‡ โˆˆ ( ๐ด RingHom ๐‘Œ ) )
37 13 8 rhm1 โŠข ( ๐‘‡ โˆˆ ( ๐ด RingHom ๐‘Œ ) โ†’ ( ๐‘‡ โ€˜ ๐‘‚ ) = 1 )
38 17 36 37 3syl โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ๐‘‡ โ€˜ ๐‘‚ ) = 1 )
39 38 adantr โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘› โˆˆ โ„•0 ) โ†’ ( ๐‘‡ โ€˜ ๐‘‚ ) = 1 )
40 39 oveq2d โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘› โˆˆ โ„•0 ) โ†’ ( ( ๐‘ˆ โ€˜ ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) ) ยท ( ๐‘‡ โ€˜ ๐‘‚ ) ) = ( ( ๐‘ˆ โ€˜ ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) ) ยท 1 ) )
41 35 40 eqtr2d โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘› โˆˆ โ„•0 ) โ†’ ( ( ๐‘ˆ โ€˜ ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) ) ยท 1 ) = ( ๐‘‡ โ€˜ ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— ๐‘‚ ) ) )
42 41 oveq2d โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘› โˆˆ โ„•0 ) โ†’ ( ( ๐‘› โ†‘ ๐‘‹ ) ยท ( ( ๐‘ˆ โ€˜ ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) ) ยท 1 ) ) = ( ( ๐‘› โ†‘ ๐‘‹ ) ยท ( ๐‘‡ โ€˜ ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— ๐‘‚ ) ) ) )
43 42 mpteq2dva โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) ยท ( ( ๐‘ˆ โ€˜ ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) ) ยท 1 ) ) ) = ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) ยท ( ๐‘‡ โ€˜ ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— ๐‘‚ ) ) ) ) )
44 43 oveq2d โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) ยท ( ( ๐‘ˆ โ€˜ ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) ) ยท 1 ) ) ) ) = ( ๐‘Œ ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) ยท ( ๐‘‡ โ€˜ ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— ๐‘‚ ) ) ) ) ) )
45 16 44 eqtrd โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ๐ป = ( ๐‘Œ ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) ยท ( ๐‘‡ โ€˜ ( ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) โˆ— ๐‘‚ ) ) ) ) ) )