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 ) ∈ 𝑆 )