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 = {Poly}_{1} (R)$
	chmaidscmat.e	$⊢ E = {Base}_{P}$
	chmaidscmat.y	$⊢ Y = N Mat P$
	chmaidscmat.k	$⊢ K = {Base}_{Y}$
	chmaidscmat.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
	chmaidscmat.1	$⊢ \underset{˙}{1} = 1_{Y}$
	chmaidscmat.d	$⊢ S = N ScMat P$
Assertion	chmaidscmat	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to C (M) \underset{˙}{\cdot} \underset{˙}{1} \in 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 = {Poly}_{1} (R)$
5		chmaidscmat.e	$⊢ E = {Base}_{P}$
6		chmaidscmat.y	$⊢ Y = N Mat P$
7		chmaidscmat.k	$⊢ K = {Base}_{Y}$
8		chmaidscmat.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
9		chmaidscmat.1	$⊢ \underset{˙}{1} = 1_{Y}$
10		chmaidscmat.d	$⊢ S = N ScMat P$
11		crngring	$⊢ R \in CRing \to R \in Ring$
12	4	ply1ring	$⊢ R \in Ring \to P \in Ring$
13	11 12	syl	$⊢ R \in CRing \to P \in Ring$
14	13	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land P \in Ring)$
15	14	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land P \in Ring)$
16	3 1 2 4 5	chpmatply1	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to C (M) \in E$
17	4 6	pmatring	$⊢ (N \in Fin \land R \in Ring) \to Y \in Ring$
18	11 17	sylan2	$⊢ (N \in Fin \land R \in CRing) \to Y \in Ring$
19	7 9	ringidcl	$⊢ Y \in Ring \to \underset{˙}{1} \in K$
20	18 19	syl	$⊢ (N \in Fin \land R \in CRing) \to \underset{˙}{1} \in K$
21	20	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \underset{˙}{1} \in K$
22	5 6 7 8	matvscl	$⊢ ((N \in Fin \land P \in Ring) \land (C (M) \in E \land \underset{˙}{1} \in K)) \to C (M) \underset{˙}{\cdot} \underset{˙}{1} \in K$
23	15 16 21 22	syl12anc	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to C (M) \underset{˙}{\cdot} \underset{˙}{1} \in K$
24		risset	$⊢ C (M) \in E \leftrightarrow \exists c \in E c = C (M)$
25		oveq1	$⊢ C (M) = c \to C (M) \underset{˙}{\cdot} \underset{˙}{1} = c \underset{˙}{\cdot} \underset{˙}{1}$
26	25	eqcoms	$⊢ c = C (M) \to C (M) \underset{˙}{\cdot} \underset{˙}{1} = c \underset{˙}{\cdot} \underset{˙}{1}$
27	26	a1i	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land c \in E) \to (c = C (M) \to C (M) \underset{˙}{\cdot} \underset{˙}{1} = c \underset{˙}{\cdot} \underset{˙}{1})$
28	27	reximdva	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (\exists c \in E c = C (M) \to \exists c \in E C (M) \underset{˙}{\cdot} \underset{˙}{1} = c \underset{˙}{\cdot} \underset{˙}{1})$
29	28	com12	$⊢ \exists c \in E c = C (M) \to ((N \in Fin \land R \in CRing \land M \in B) \to \exists c \in E C (M) \underset{˙}{\cdot} \underset{˙}{1} = c \underset{˙}{\cdot} \underset{˙}{1})$
30	24 29	sylbi	$⊢ C (M) \in E \to ((N \in Fin \land R \in CRing \land M \in B) \to \exists c \in E C (M) \underset{˙}{\cdot} \underset{˙}{1} = c \underset{˙}{\cdot} \underset{˙}{1})$
31	16 30	mpcom	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \exists c \in E C (M) \underset{˙}{\cdot} \underset{˙}{1} = c \underset{˙}{\cdot} \underset{˙}{1}$
32	5 6 7 9 8 10	scmatel	$⊢ (N \in Fin \land P \in Ring) \to (C (M) \underset{˙}{\cdot} \underset{˙}{1} \in S \leftrightarrow (C (M) \underset{˙}{\cdot} \underset{˙}{1} \in K \land \exists c \in E C (M) \underset{˙}{\cdot} \underset{˙}{1} = c \underset{˙}{\cdot} \underset{˙}{1}))$
33	15 32	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (C (M) \underset{˙}{\cdot} \underset{˙}{1} \in S \leftrightarrow (C (M) \underset{˙}{\cdot} \underset{˙}{1} \in K \land \exists c \in E C (M) \underset{˙}{\cdot} \underset{˙}{1} = c \underset{˙}{\cdot} \underset{˙}{1}))$
34	23 31 33	mpbir2and	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to C (M) \underset{˙}{\cdot} \underset{˙}{1} \in S$

Metamath Proof Explorer

Theorem chmaidscmat

Proof