Metamath Proof Explorer


Theorem cpmidg2sum

Description: Equality of two sums representing the identity matrix multiplied with the characteristic polynomial of a matrix. (Contributed by AV, 11-Nov-2019)

Ref Expression
Hypotheses cpmadugsum.a โŠข ๐ด = ( ๐‘ Mat ๐‘… )
cpmadugsum.b โŠข ๐ต = ( Base โ€˜ ๐ด )
cpmadugsum.p โŠข ๐‘ƒ = ( Poly1 โ€˜ ๐‘… )
cpmadugsum.y โŠข ๐‘Œ = ( ๐‘ Mat ๐‘ƒ )
cpmadugsum.t โŠข ๐‘‡ = ( ๐‘ matToPolyMat ๐‘… )
cpmadugsum.x โŠข ๐‘‹ = ( var1 โ€˜ ๐‘… )
cpmadugsum.e โŠข โ†‘ = ( .g โ€˜ ( mulGrp โ€˜ ๐‘ƒ ) )
cpmadugsum.m โŠข ยท = ( ยท๐‘  โ€˜ ๐‘Œ )
cpmadugsum.r โŠข ร— = ( .r โ€˜ ๐‘Œ )
cpmadugsum.1 โŠข 1 = ( 1r โ€˜ ๐‘Œ )
cpmadugsum.g โŠข + = ( +g โ€˜ ๐‘Œ )
cpmadugsum.s โŠข โˆ’ = ( -g โ€˜ ๐‘Œ )
cpmadugsum.i โŠข ๐ผ = ( ( ๐‘‹ ยท 1 ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) )
cpmadugsum.j โŠข ๐ฝ = ( ๐‘ maAdju ๐‘ƒ )
cpmadugsum.0 โŠข 0 = ( 0g โ€˜ ๐‘Œ )
cpmadugsum.g2 โŠข ๐บ = ( ๐‘› โˆˆ โ„•0 โ†ฆ if ( ๐‘› = 0 , ( 0 โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) , if ( ๐‘› = ( ๐‘  + 1 ) , ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) , if ( ( ๐‘  + 1 ) < ๐‘› , 0 , ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘› โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘› ) ) ) ) ) ) ) )
cpmidgsum2.c โŠข ๐ถ = ( ๐‘ CharPlyMat ๐‘… )
cpmidgsum2.k โŠข ๐พ = ( ๐ถ โ€˜ ๐‘€ )
cpmidg2sum.u โŠข ๐‘ˆ = ( algSc โ€˜ ๐‘ƒ )
Assertion cpmidg2sum ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ โˆƒ ๐‘  โˆˆ โ„• โˆƒ ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ โ„•0 โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ( ๐‘ˆ โ€˜ ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘– ) ) ยท 1 ) ) ) ) = ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ โ„•0 โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cpmadugsum.a โŠข ๐ด = ( ๐‘ Mat ๐‘… )
2 cpmadugsum.b โŠข ๐ต = ( Base โ€˜ ๐ด )
3 cpmadugsum.p โŠข ๐‘ƒ = ( Poly1 โ€˜ ๐‘… )
4 cpmadugsum.y โŠข ๐‘Œ = ( ๐‘ Mat ๐‘ƒ )
5 cpmadugsum.t โŠข ๐‘‡ = ( ๐‘ matToPolyMat ๐‘… )
6 cpmadugsum.x โŠข ๐‘‹ = ( var1 โ€˜ ๐‘… )
7 cpmadugsum.e โŠข โ†‘ = ( .g โ€˜ ( mulGrp โ€˜ ๐‘ƒ ) )
8 cpmadugsum.m โŠข ยท = ( ยท๐‘  โ€˜ ๐‘Œ )
9 cpmadugsum.r โŠข ร— = ( .r โ€˜ ๐‘Œ )
10 cpmadugsum.1 โŠข 1 = ( 1r โ€˜ ๐‘Œ )
11 cpmadugsum.g โŠข + = ( +g โ€˜ ๐‘Œ )
12 cpmadugsum.s โŠข โˆ’ = ( -g โ€˜ ๐‘Œ )
13 cpmadugsum.i โŠข ๐ผ = ( ( ๐‘‹ ยท 1 ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) )
14 cpmadugsum.j โŠข ๐ฝ = ( ๐‘ maAdju ๐‘ƒ )
15 cpmadugsum.0 โŠข 0 = ( 0g โ€˜ ๐‘Œ )
16 cpmadugsum.g2 โŠข ๐บ = ( ๐‘› โˆˆ โ„•0 โ†ฆ if ( ๐‘› = 0 , ( 0 โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) , if ( ๐‘› = ( ๐‘  + 1 ) , ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) , if ( ( ๐‘  + 1 ) < ๐‘› , 0 , ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘› โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘› ) ) ) ) ) ) ) )
17 cpmidgsum2.c โŠข ๐ถ = ( ๐‘ CharPlyMat ๐‘… )
18 cpmidgsum2.k โŠข ๐พ = ( ๐ถ โ€˜ ๐‘€ )
19 cpmidg2sum.u โŠข ๐‘ˆ = ( algSc โ€˜ ๐‘ƒ )
20 eqid โŠข ( ๐พ ยท 1 ) = ( ๐พ ยท 1 )
21 1 2 3 4 6 7 8 10 19 17 18 20 cpmidgsum โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ๐พ ยท 1 ) = ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ โ„•0 โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ( ๐‘ˆ โ€˜ ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘– ) ) ยท 1 ) ) ) ) )
22 21 eqcomd โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ โ„•0 โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ( ๐‘ˆ โ€˜ ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘– ) ) ยท 1 ) ) ) ) = ( ๐พ ยท 1 ) )
23 22 ad3antrrr โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘  โˆˆ โ„• ) โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โˆง ( ๐พ ยท 1 ) = ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ โ„•0 โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ โ„•0 โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ( ๐‘ˆ โ€˜ ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘– ) ) ยท 1 ) ) ) ) = ( ๐พ ยท 1 ) )
24 simpr โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘  โˆˆ โ„• ) โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โˆง ( ๐พ ยท 1 ) = ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ โ„•0 โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) ) โ†’ ( ๐พ ยท 1 ) = ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ โ„•0 โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) )
25 23 24 eqtrd โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘  โˆˆ โ„• ) โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โˆง ( ๐พ ยท 1 ) = ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ โ„•0 โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ โ„•0 โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ( ๐‘ˆ โ€˜ ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘– ) ) ยท 1 ) ) ) ) = ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ โ„•0 โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) )
26 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 20 cpmidgsum2 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ โˆƒ ๐‘  โˆˆ โ„• โˆƒ ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ( ๐พ ยท 1 ) = ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ โ„•0 โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) )
27 25 26 reximddv2 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ โˆƒ ๐‘  โˆˆ โ„• โˆƒ ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ โ„•0 โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ( ๐‘ˆ โ€˜ ( ( coe1 โ€˜ ๐พ ) โ€˜ ๐‘– ) ) ยท 1 ) ) ) ) = ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ โ„•0 โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) )