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 
|- A = ( N Mat R )
chmaidscmat.b 
|- B = ( Base ` A )
chmaidscmat.c 
|- C = ( N CharPlyMat R )
chmaidscmat.p 
|- P = ( Poly1 ` R )
chmaidscmat.e 
|- E = ( Base ` P )
chmaidscmat.y 
|- Y = ( N Mat P )
chmaidscmat.k 
|- K = ( Base ` Y )
chmaidscmat.m 
|- .x. = ( .s ` Y )
chmaidscmat.1 
|- .1. = ( 1r ` Y )
chmaidscmat.d 
|- S = ( N ScMat P )
Assertion chmaidscmat 
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( C ` M ) .x. .1. ) e. S )

Proof

Step Hyp Ref Expression
1 chmaidscmat.a 
 |-  A = ( N Mat R )
2 chmaidscmat.b 
 |-  B = ( Base ` A )
3 chmaidscmat.c 
 |-  C = ( N CharPlyMat R )
4 chmaidscmat.p 
 |-  P = ( Poly1 ` R )
5 chmaidscmat.e 
 |-  E = ( Base ` P )
6 chmaidscmat.y 
 |-  Y = ( N Mat P )
7 chmaidscmat.k 
 |-  K = ( Base ` Y )
8 chmaidscmat.m 
 |-  .x. = ( .s ` Y )
9 chmaidscmat.1 
 |-  .1. = ( 1r ` Y )
10 chmaidscmat.d 
 |-  S = ( N ScMat P )
11 crngring 
 |-  ( R e. CRing -> R e. Ring )
12 4 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
13 11 12 syl 
 |-  ( R e. CRing -> P e. Ring )
14 13 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ P e. Ring ) )
15 14 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ P e. Ring ) )
16 3 1 2 4 5 chpmatply1 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( C ` M ) e. E )
17 4 6 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Y e. Ring )
18 11 17 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. Ring )
19 7 9 ringidcl 
 |-  ( Y e. Ring -> .1. e. K )
20 18 19 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> .1. e. K )
21 20 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> .1. e. K )
22 5 6 7 8 matvscl 
 |-  ( ( ( N e. Fin /\ P e. Ring ) /\ ( ( C ` M ) e. E /\ .1. e. K ) ) -> ( ( C ` M ) .x. .1. ) e. K )
23 15 16 21 22 syl12anc 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( C ` M ) .x. .1. ) e. K )
24 risset 
 |-  ( ( C ` M ) e. E <-> E. c e. E c = ( C ` M ) )
25 oveq1 
 |-  ( ( C ` M ) = c -> ( ( C ` M ) .x. .1. ) = ( c .x. .1. ) )
26 25 eqcoms 
 |-  ( c = ( C ` M ) -> ( ( C ` M ) .x. .1. ) = ( c .x. .1. ) )
27 26 a1i 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ c e. E ) -> ( c = ( C ` M ) -> ( ( C ` M ) .x. .1. ) = ( c .x. .1. ) ) )
28 27 reximdva 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( E. c e. E c = ( C ` M ) -> E. c e. E ( ( C ` M ) .x. .1. ) = ( c .x. .1. ) ) )
29 28 com12 
 |-  ( E. c e. E c = ( C ` M ) -> ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. c e. E ( ( C ` M ) .x. .1. ) = ( c .x. .1. ) ) )
30 24 29 sylbi 
 |-  ( ( C ` M ) e. E -> ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. c e. E ( ( C ` M ) .x. .1. ) = ( c .x. .1. ) ) )
31 16 30 mpcom 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. c e. E ( ( C ` M ) .x. .1. ) = ( c .x. .1. ) )
32 5 6 7 9 8 10 scmatel 
 |-  ( ( N e. Fin /\ P e. Ring ) -> ( ( ( C ` M ) .x. .1. ) e. S <-> ( ( ( C ` M ) .x. .1. ) e. K /\ E. c e. E ( ( C ` M ) .x. .1. ) = ( c .x. .1. ) ) ) )
33 15 32 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( ( C ` M ) .x. .1. ) e. S <-> ( ( ( C ` M ) .x. .1. ) e. K /\ E. c e. E ( ( C ` M ) .x. .1. ) = ( c .x. .1. ) ) ) )
34 23 31 33 mpbir2and 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( C ` M ) .x. .1. ) e. S )