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	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
	chp0mat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	chp0mat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	chp0mat.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	chp0mat.g	⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
	chp0mat.m	⊢ ↑ = ( .g ‘ 𝐺 )
	chpscmat.d	⊢ 𝐷 = { 𝑚 ∈ ( Base ‘ 𝐴 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g ‘ 𝑅 ) ) }
	chpscmat.s	⊢ 𝑆 = ( algSc ‘ 𝑃 )
	chpscmat.m	⊢ − = ( -g ‘ 𝑃 )
Assertion	chpscmat0	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐼 𝑀 𝐼 ) ) ) → ( 𝐶 ‘ 𝑀 ) = ( ( ♯ ‘ 𝑁 ) ↑ ( 𝑋 − ( 𝑆 ‘ ( 𝐼 𝑀 𝐼 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		chp0mat.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
2		chp0mat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		chp0mat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4		chp0mat.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
5		chp0mat.g	⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
6		chp0mat.m	⊢ ↑ = ( .g ‘ 𝐺 )
7		chpscmat.d	⊢ 𝐷 = { 𝑚 ∈ ( Base ‘ 𝐴 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g ‘ 𝑅 ) ) }
8		chpscmat.s	⊢ 𝑆 = ( algSc ‘ 𝑃 )
9		chpscmat.m	⊢ − = ( -g ‘ 𝑃 )
10	1 2 3 4 5 6 7 8 9	chpscmat	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 𝑛 ) = ( 𝐼 𝑀 𝐼 ) ) ) → ( 𝐶 ‘ 𝑀 ) = ( ( ♯ ‘ 𝑁 ) ↑ ( 𝑋 − ( 𝑆 ‘ ( 𝐼 𝑀 𝐼 ) ) ) ) )