Theorem chpscmat0

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\mathrm{CharPlyMat}R$$
	chp0mat.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	chp0mat.a	$$⊢A=N\mathrm{Mat}R$$
	chp0mat.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	chp0mat.g	$$⊢G={\mathrm{mulGrp}}_P$$
	chp0mat.m	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
	chpscmat.d	$$⊢D=\left\{m\in {\mathrm{Base}}_A|\exists c\in {\mathrm{Base}}_R\forall i\in N\forall j\in Nimj=if\left(i=j,c,0_R\right)\right\}$$
	chpscmat.s	$$⊢S=\mathrm{algSc}\left(P\right)$$
	chpscmat.m	$$⊢\underset{\dot{}}{-}={-}_P$$
Assertion	chpscmat0	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\right)\wedge \left(M\in D\wedge I\in N\wedge \forall n\in NnMn=IMI\right)\right)\to C\left(M\right)=\left|N\right|\underset{\dot{}}{\times }\left(X\underset{\dot{}}{-}S\left(IMI\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		chp0mat.c	$$⊢C=N\mathrm{CharPlyMat}R$$
2		chp0mat.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		chp0mat.a	$$⊢A=N\mathrm{Mat}R$$
4		chp0mat.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
5		chp0mat.g	$$⊢G={\mathrm{mulGrp}}_P$$
6		chp0mat.m	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
7		chpscmat.d	$$⊢D=\left\{m\in {\mathrm{Base}}_A|\exists c\in {\mathrm{Base}}_R\forall i\in N\forall j\in Nimj=if\left(i=j,c,0_R\right)\right\}$$
8		chpscmat.s	$$⊢S=\mathrm{algSc}\left(P\right)$$
9		chpscmat.m	$$⊢\underset{\dot{}}{-}={-}_P$$
10	1 2 3 4 5 6 7 8 9	chpscmat	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\right)\wedge \left(M\in D\wedge I\in N\wedge \forall n\in NnMn=IMI\right)\right)\to C\left(M\right)=\left|N\right|\underset{\dot{}}{\times }\left(X\underset{\dot{}}{-}S\left(IMI\right)\right)$$