Description: The characteristic polynomial of a (nonempty!) scalar matrix, expressed with its diagonal element. (Contributed by AV, 21-Aug-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | chp0mat.c | |- C = ( N CharPlyMat R ) |
|
| chp0mat.p | |- P = ( Poly1 ` R ) |
||
| chp0mat.a | |- A = ( N Mat R ) |
||
| chp0mat.x | |- X = ( var1 ` R ) |
||
| chp0mat.g | |- G = ( mulGrp ` P ) |
||
| chp0mat.m | |- .^ = ( .g ` G ) |
||
| chpscmat.d | |- D = { m e. ( Base ` A ) | E. c e. ( Base ` R ) A. i e. N A. j e. N ( i m j ) = if ( i = j , c , ( 0g ` R ) ) } |
||
| chpscmat.s | |- S = ( algSc ` P ) |
||
| chpscmat.m | |- .- = ( -g ` P ) |
||
| Assertion | chpscmat0 | |- ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = ( I M I ) ) ) -> ( C ` M ) = ( ( # ` N ) .^ ( X .- ( S ` ( I M I ) ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | chp0mat.c | |- C = ( N CharPlyMat R ) |
|
| 2 | chp0mat.p | |- P = ( Poly1 ` R ) |
|
| 3 | chp0mat.a | |- A = ( N Mat R ) |
|
| 4 | chp0mat.x | |- X = ( var1 ` R ) |
|
| 5 | chp0mat.g | |- G = ( mulGrp ` P ) |
|
| 6 | chp0mat.m | |- .^ = ( .g ` G ) |
|
| 7 | chpscmat.d | |- D = { m e. ( Base ` A ) | E. c e. ( Base ` R ) A. i e. N A. j e. N ( i m j ) = if ( i = j , c , ( 0g ` R ) ) } |
|
| 8 | chpscmat.s | |- S = ( algSc ` P ) |
|
| 9 | chpscmat.m | |- .- = ( -g ` P ) |
|
| 10 | 1 2 3 4 5 6 7 8 9 | chpscmat | |- ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = ( I M I ) ) ) -> ( C ` M ) = ( ( # ` N ) .^ ( X .- ( S ` ( I M I ) ) ) ) ) |