Metamath Proof Explorer


Theorem chmaidscmat

Description: The characteristic polynomial of a matrix multiplied with the identity matrix is a scalar matrix. (Contributed by AV, 30-Oct-2019) (Revised by AV, 5-Jul-2022)

Ref Expression
Hypotheses chmaidscmat.a 𝐴 = ( 𝑁 Mat 𝑅 )
chmaidscmat.b 𝐵 = ( Base ‘ 𝐴 )
chmaidscmat.c 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
chmaidscmat.p 𝑃 = ( Poly1𝑅 )
chmaidscmat.e 𝐸 = ( Base ‘ 𝑃 )
chmaidscmat.y 𝑌 = ( 𝑁 Mat 𝑃 )
chmaidscmat.k 𝐾 = ( Base ‘ 𝑌 )
chmaidscmat.m · = ( ·𝑠𝑌 )
chmaidscmat.1 1 = ( 1r𝑌 )
chmaidscmat.d 𝑆 = ( 𝑁 ScMat 𝑃 )
Assertion chmaidscmat ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( ( 𝐶𝑀 ) · 1 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 chmaidscmat.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 chmaidscmat.b 𝐵 = ( Base ‘ 𝐴 )
3 chmaidscmat.c 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
4 chmaidscmat.p 𝑃 = ( Poly1𝑅 )
5 chmaidscmat.e 𝐸 = ( Base ‘ 𝑃 )
6 chmaidscmat.y 𝑌 = ( 𝑁 Mat 𝑃 )
7 chmaidscmat.k 𝐾 = ( Base ‘ 𝑌 )
8 chmaidscmat.m · = ( ·𝑠𝑌 )
9 chmaidscmat.1 1 = ( 1r𝑌 )
10 chmaidscmat.d 𝑆 = ( 𝑁 ScMat 𝑃 )
11 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
12 4 ply1ring ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
13 11 12 syl ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
14 13 anim2i ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) )
15 14 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) )
16 3 1 2 4 5 chpmatply1 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( 𝐶𝑀 ) ∈ 𝐸 )
17 4 6 pmatring ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ Ring )
18 11 17 sylan2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ Ring )
19 7 9 ringidcl ( 𝑌 ∈ Ring → 1𝐾 )
20 18 19 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 1𝐾 )
21 20 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 1𝐾 )
22 5 6 7 8 matvscl ( ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) ∧ ( ( 𝐶𝑀 ) ∈ 𝐸1𝐾 ) ) → ( ( 𝐶𝑀 ) · 1 ) ∈ 𝐾 )
23 15 16 21 22 syl12anc ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( ( 𝐶𝑀 ) · 1 ) ∈ 𝐾 )
24 risset ( ( 𝐶𝑀 ) ∈ 𝐸 ↔ ∃ 𝑐𝐸 𝑐 = ( 𝐶𝑀 ) )
25 oveq1 ( ( 𝐶𝑀 ) = 𝑐 → ( ( 𝐶𝑀 ) · 1 ) = ( 𝑐 · 1 ) )
26 25 eqcoms ( 𝑐 = ( 𝐶𝑀 ) → ( ( 𝐶𝑀 ) · 1 ) = ( 𝑐 · 1 ) )
27 26 a1i ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑐𝐸 ) → ( 𝑐 = ( 𝐶𝑀 ) → ( ( 𝐶𝑀 ) · 1 ) = ( 𝑐 · 1 ) ) )
28 27 reximdva ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( ∃ 𝑐𝐸 𝑐 = ( 𝐶𝑀 ) → ∃ 𝑐𝐸 ( ( 𝐶𝑀 ) · 1 ) = ( 𝑐 · 1 ) ) )
29 28 com12 ( ∃ 𝑐𝐸 𝑐 = ( 𝐶𝑀 ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ∃ 𝑐𝐸 ( ( 𝐶𝑀 ) · 1 ) = ( 𝑐 · 1 ) ) )
30 24 29 sylbi ( ( 𝐶𝑀 ) ∈ 𝐸 → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ∃ 𝑐𝐸 ( ( 𝐶𝑀 ) · 1 ) = ( 𝑐 · 1 ) ) )
31 16 30 mpcom ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ∃ 𝑐𝐸 ( ( 𝐶𝑀 ) · 1 ) = ( 𝑐 · 1 ) )
32 5 6 7 9 8 10 scmatel ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → ( ( ( 𝐶𝑀 ) · 1 ) ∈ 𝑆 ↔ ( ( ( 𝐶𝑀 ) · 1 ) ∈ 𝐾 ∧ ∃ 𝑐𝐸 ( ( 𝐶𝑀 ) · 1 ) = ( 𝑐 · 1 ) ) ) )
33 15 32 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( ( ( 𝐶𝑀 ) · 1 ) ∈ 𝑆 ↔ ( ( ( 𝐶𝑀 ) · 1 ) ∈ 𝐾 ∧ ∃ 𝑐𝐸 ( ( 𝐶𝑀 ) · 1 ) = ( 𝑐 · 1 ) ) ) )
34 23 31 33 mpbir2and ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( ( 𝐶𝑀 ) · 1 ) ∈ 𝑆 )