Metamath Proof Explorer


Theorem cpmidgsum

Description: Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as group sum. (Contributed by AV, 7-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 )
Assertion cpmidgsum ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ๐ป = ( ๐‘Œ ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) ยท ( ( ๐‘ˆ โ€˜ ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) ) ยท 1 ) ) ) ) )

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 eqid โŠข ( Base โ€˜ ๐‘ƒ ) = ( Base โ€˜ ๐‘ƒ )
14 10 1 2 3 13 chpmatply1 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ๐ถ โ€˜ ๐‘€ ) โˆˆ ( Base โ€˜ ๐‘ƒ ) )
15 11 14 eqeltrid โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ๐พ โˆˆ ( Base โ€˜ ๐‘ƒ ) )
16 eqid โŠข ( Base โ€˜ ๐‘Œ ) = ( Base โ€˜ ๐‘Œ )
17 eqid โŠข ( ๐‘ matToPolyMat ๐‘… ) = ( ๐‘ matToPolyMat ๐‘… )
18 eqid โŠข ( Base โ€˜ ๐‘… ) = ( Base โ€˜ ๐‘… )
19 3 4 16 7 6 5 17 1 2 9 18 13 9 8 12 pmatcollpwscmat โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐พ โˆˆ ( Base โ€˜ ๐‘ƒ ) ) โ†’ ๐ป = ( ๐‘Œ ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) ยท ( ( ๐‘ˆ โ€˜ ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) ) ยท 1 ) ) ) ) )
20 15 19 syld3an3 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ๐ป = ( ๐‘Œ ฮฃg ( ๐‘› โˆˆ โ„•0 โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) ยท ( ( ๐‘ˆ โ€˜ ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘› ) ) ยท 1 ) ) ) ) )