chpdmat

Description: The characteristic polynomial of a diagonal matrix. (Contributed by AV, 18-Aug-2019) (Proof shortened by AV, 21-Nov-2019)

	Ref	Expression
Hypotheses	chpdmat.c	$⊢ C = N CharPlyMat R$
	chpdmat.p	$⊢ P = {Poly}_{1} (R)$
	chpdmat.a	$⊢ A = N Mat R$
	chpdmat.s	$⊢ S = algSc (P)$
	chpdmat.b	$⊢ B = {Base}_{A}$
	chpdmat.x	$⊢ X = {var}_{1} (R)$
	chpdmat.0	$⊢ \underset{˙}{0} = 0_{R}$
	chpdmat.g	$⊢ G = {mulGrp}_{P}$
	chpdmat.m	$⊢ \underset{˙}{-} = -_{P}$
Assertion	chpdmat	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to C (M) = \underset{k \in N}{\sum_{G}} (X \underset{˙}{-} S (k M k))$

Proof

Step	Hyp	Ref	Expression
1		chpdmat.c	$⊢ C = N CharPlyMat R$
2		chpdmat.p	$⊢ P = {Poly}_{1} (R)$
3		chpdmat.a	$⊢ A = N Mat R$
4		chpdmat.s	$⊢ S = algSc (P)$
5		chpdmat.b	$⊢ B = {Base}_{A}$
6		chpdmat.x	$⊢ X = {var}_{1} (R)$
7		chpdmat.0	$⊢ \underset{˙}{0} = 0_{R}$
8		chpdmat.g	$⊢ G = {mulGrp}_{P}$
9		chpdmat.m	$⊢ \underset{˙}{-} = -_{P}$
10		eqid	$⊢ N Mat P = N Mat P$
11		eqid	$⊢ N maDet P = N maDet P$
12		eqid	$⊢ -_{(N Mat P)} = -_{(N Mat P)}$
13		eqid	$⊢ \cdot_{(N Mat P)} = \cdot_{(N Mat P)}$
14		eqid	$⊢ N matToPolyMat R = N matToPolyMat R$
15		eqid	$⊢ 1_{(N Mat P)} = 1_{(N Mat P)}$
16	1 3 5 2 10 11 12 6 13 14 15	chpmatval	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to C (M) = (N maDet P) ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M))$
17	16	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to C (M) = (N maDet P) ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M))$
18	2	ply1crng	$⊢ R \in CRing \to P \in CRing$
19	18	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P \in CRing$
20		simp1	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to N \in Fin$
21		crngring	$⊢ R \in CRing \to R \in Ring$
22	21	3anim2i	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land R \in Ring \land M \in B)$
23	1 2 3 4 5 6 7 8 9 10 15 13 12 14	chpdmatlem1	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M) \in {Base}_{(N Mat P)}$
24	22 23	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M) \in {Base}_{(N Mat P)}$
25	19 20 24	3jca	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (P \in CRing \land N \in Fin \land (X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M) \in {Base}_{(N Mat P)})$
26	25	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to (P \in CRing \land N \in Fin \land (X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M) \in {Base}_{(N Mat P)})$
27	22	anim1i	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land i \in N) \to ((N \in Fin \land R \in Ring \land M \in B) \land i \in N)$
28	27	anim1i	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land i \in N) \land j \in N) \to (((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N)$
29	1 2 3 4 5 6 7 8 9 10 15 13 12 14	chpdmatlem2	$⊢ (((((N \in Fin \land R \in Ring \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to i ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) j = 0_{P}$
30	28 29	sylanl1	$⊢ (((((N \in Fin \land R \in CRing \land M \in B) \land i \in N) \land j \in N) \land i \neq j) \land i M j = \underset{˙}{0}) \to i ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) j = 0_{P}$
31	30	exp31	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land i \in N) \land j \in N) \to (i \neq j \to (i M j = \underset{˙}{0} \to i ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) j = 0_{P}))$
32	31	a2d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land i \in N) \land j \in N) \to ((i \neq j \to i M j = \underset{˙}{0}) \to (i \neq j \to i ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) j = 0_{P}))$
33	32	ralimdva	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land i \in N) \to (\forall j \in N (i \neq j \to i M j = \underset{˙}{0}) \to \forall j \in N (i \neq j \to i ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) j = 0_{P}))$
34	33	ralimdva	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (\forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0}) \to \forall i \in N \forall j \in N (i \neq j \to i ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) j = 0_{P}))$
35	34	imp	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to \forall i \in N \forall j \in N (i \neq j \to i ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) j = 0_{P})$
36		eqid	$⊢ {Base}_{(N Mat P)} = {Base}_{(N Mat P)}$
37		eqid	$⊢ 0_{P} = 0_{P}$
38	11 10 36 8 37	mdetdiag	$⊢ (P \in CRing \land N \in Fin \land (X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M) \in {Base}_{(N Mat P)}) \to (\forall i \in N \forall j \in N (i \neq j \to i ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) j = 0_{P}) \to (N maDet P) ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) = \underset{k \in N}{\sum_{G}} (k ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) k))$
39	26 35 38	sylc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to (N maDet P) ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) = \underset{k \in N}{\sum_{G}} (k ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) k)$
40	1 2 3 4 5 6 7 8 9 10 15 13 12 14	chpdmatlem3	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land k \in N) \to k ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) k = X \underset{˙}{-} S (k M k)$
41	22 40	sylan	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land k \in N) \to k ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) k = X \underset{˙}{-} S (k M k)$
42	41	adantlr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land k \in N) \to k ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) k = X \underset{˙}{-} S (k M k)$
43	42	mpteq2dva	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to (k \in N ⟼ k ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) k) = (k \in N ⟼ X \underset{˙}{-} S (k M k))$
44	43	oveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to \underset{k \in N}{\sum_{G}} (k ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) k) = \underset{k \in N}{\sum_{G}} (X \underset{˙}{-} S (k M k))$
45	17 39 44	3eqtrd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to C (M) = \underset{k \in N}{\sum_{G}} (X \underset{˙}{-} S (k M k))$

Metamath Proof Explorer

Theorem chpdmat

Proof