chpmatply1

Description: The characteristic polynomial of a (square) matrix over a commutative ring is a polynomial, see also the following remark in Lang, p. 561: "[the characteristic polynomial] is an element of k[t". (Contributed by AV, 2-Aug-2019) (Proof shortened by AV, 29-Nov-2019)

	Ref	Expression
Hypotheses	chpmatply1.c	$⊢ C = N CharPlyMat R$
	chpmatply1.a	$⊢ A = N Mat R$
	chpmatply1.b	$⊢ B = {Base}_{A}$
	chpmatply1.p	$⊢ P = {Poly}_{1} (R)$
	chpmatply1.e	$⊢ E = {Base}_{P}$
Assertion	chpmatply1	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to C (M) \in E$

Proof

Step	Hyp	Ref	Expression
1		chpmatply1.c	$⊢ C = N CharPlyMat R$
2		chpmatply1.a	$⊢ A = N Mat R$
3		chpmatply1.b	$⊢ B = {Base}_{A}$
4		chpmatply1.p	$⊢ P = {Poly}_{1} (R)$
5		chpmatply1.e	$⊢ E = {Base}_{P}$
6		eqid	$⊢ N Mat P = N Mat P$
7		eqid	$⊢ N maDet P = N maDet P$
8		eqid	$⊢ -_{(N Mat P)} = -_{(N Mat P)}$
9		eqid	$⊢ {var}_{1} (R) = {var}_{1} (R)$
10		eqid	$⊢ \cdot_{(N Mat P)} = \cdot_{(N Mat P)}$
11		eqid	$⊢ N matToPolyMat R = N matToPolyMat R$
12		eqid	$⊢ 1_{(N Mat P)} = 1_{(N Mat P)}$
13	1 2 3 4 6 7 8 9 10 11 12	chpmatval	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to C (M) = (N maDet P) (({var}_{1} (R) \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M))$
14	4	ply1crng	$⊢ R \in CRing \to P \in CRing$
15	14	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P \in CRing$
16		crngring	$⊢ R \in CRing \to R \in Ring$
17		eqid	$⊢ ({var}_{1} (R) \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M) = ({var}_{1} (R) \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)$
18	2 3 4 6 9 11 8 10 12 17	chmatcl	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to ({var}_{1} (R) \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M) \in {Base}_{(N Mat P)}$
19	16 18	syl3an2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to ({var}_{1} (R) \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M) \in {Base}_{(N Mat P)}$
20		eqid	$⊢ {Base}_{(N Mat P)} = {Base}_{(N Mat P)}$
21	7 6 20 5	mdetcl	$⊢ (P \in CRing \land ({var}_{1} (R) \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M) \in {Base}_{(N Mat P)}) \to (N maDet P) (({var}_{1} (R) \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) \in E$
22	15 19 21	syl2anc	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N maDet P) (({var}_{1} (R) \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) \in E$
23	13 22	eqeltrd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to C (M) \in E$

Metamath Proof Explorer

Theorem chpmatply1

Proof