chpmat1d

Description: The characteristic polynomial of a matrix with dimension 1. (Contributed by AV, 7-Aug-2019)

	Ref	Expression
Hypotheses	chpmat1d.c	$⊢ C = N CharPlyMat R$
	chpmat1d.p	$⊢ P = {Poly}_{1} (R)$
	chpmat1d.a	$⊢ A = N Mat R$
	chpmat1d.b	$⊢ B = {Base}_{A}$
	chpmat1d.x	$⊢ X = {var}_{1} (R)$
	chpmat1d.z	$⊢ \underset{˙}{-} = -_{P}$
	chpmat1d.s	$⊢ S = algSc (P)$
Assertion	chpmat1d	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to C (M) = X \underset{˙}{-} S (I M I)$

Proof

Step	Hyp	Ref	Expression
1		chpmat1d.c	$⊢ C = N CharPlyMat R$
2		chpmat1d.p	$⊢ P = {Poly}_{1} (R)$
3		chpmat1d.a	$⊢ A = N Mat R$
4		chpmat1d.b	$⊢ B = {Base}_{A}$
5		chpmat1d.x	$⊢ X = {var}_{1} (R)$
6		chpmat1d.z	$⊢ \underset{˙}{-} = -_{P}$
7		chpmat1d.s	$⊢ S = algSc (P)$
8		snfi	$⊢ \{I\} \in Fin$
9		eleq1	$⊢ N = \{I\} \to (N \in Fin \leftrightarrow \{I\} \in Fin)$
10	8 9	mpbiri	$⊢ N = \{I\} \to N \in Fin$
11	10	adantr	$⊢ (N = \{I\} \land I \in V) \to N \in Fin$
12	11	3ad2ant2	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to N \in Fin$
13		simp1	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to R \in CRing$
14		simp3	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to M \in B$
15		eqid	$⊢ N Mat P = N Mat P$
16		eqid	$⊢ N maDet P = N maDet P$
17		eqid	$⊢ -_{(N Mat P)} = -_{(N Mat P)}$
18		eqid	$⊢ {var}_{1} (R) = {var}_{1} (R)$
19		eqid	$⊢ \cdot_{(N Mat P)} = \cdot_{(N Mat P)}$
20		eqid	$⊢ N matToPolyMat R = N matToPolyMat R$
21		eqid	$⊢ 1_{(N Mat P)} = 1_{(N Mat P)}$
22	1 3 4 2 15 16 17 18 19 20 21	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))$
23	12 13 14 22	syl3anc	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \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))$
24	2	ply1crng	$⊢ R \in CRing \to P \in CRing$
25	24	3ad2ant1	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to P \in CRing$
26		simp2	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to (N = \{I\} \land I \in V)$
27		crngring	$⊢ R \in CRing \to R \in Ring$
28	2	ply1ring	$⊢ R \in Ring \to P \in Ring$
29	27 28	syl	$⊢ R \in CRing \to P \in Ring$
30	29	3ad2ant1	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to P \in Ring$
31	15	matring	$⊢ (N \in Fin \land P \in Ring) \to N Mat P \in Ring$
32	12 30 31	syl2anc	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to N Mat P \in Ring$
33		ringgrp	$⊢ N Mat P \in Ring \to N Mat P \in Grp$
34	32 33	syl	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to N Mat P \in Grp$
35	15	matlmod	$⊢ (N \in Fin \land P \in Ring) \to N Mat P \in LMod$
36	12 30 35	syl2anc	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to N Mat P \in LMod$
37	27	3ad2ant1	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to R \in Ring$
38		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
39		eqid	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{{Poly}_{1} (R)}$
40	18 38 39	vr1cl	$⊢ R \in Ring \to {var}_{1} (R) \in {Base}_{{Poly}_{1} (R)}$
41	37 40	syl	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to {var}_{1} (R) \in {Base}_{{Poly}_{1} (R)}$
42	38	ply1crng	$⊢ R \in CRing \to {Poly}_{1} (R) \in CRing$
43	42	3ad2ant1	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to {Poly}_{1} (R) \in CRing$
44	2	oveq2i	$⊢ N Mat P = N Mat {Poly}_{1} (R)$
45	44	matsca2	$⊢ (N \in Fin \land {Poly}_{1} (R) \in CRing) \to {Poly}_{1} (R) = Scalar (N Mat P)$
46	12 43 45	syl2anc	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to {Poly}_{1} (R) = Scalar (N Mat P)$
47	46	eqcomd	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to Scalar (N Mat P) = {Poly}_{1} (R)$
48	47	fveq2d	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to {Base}_{Scalar (N Mat P)} = {Base}_{{Poly}_{1} (R)}$
49	41 48	eleqtrrd	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to {var}_{1} (R) \in {Base}_{Scalar (N Mat P)}$
50		eqid	$⊢ {Base}_{(N Mat P)} = {Base}_{(N Mat P)}$
51	50 21	ringidcl	$⊢ N Mat P \in Ring \to 1_{(N Mat P)} \in {Base}_{(N Mat P)}$
52	32 51	syl	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to 1_{(N Mat P)} \in {Base}_{(N Mat P)}$
53		eqid	$⊢ Scalar (N Mat P) = Scalar (N Mat P)$
54		eqid	$⊢ {Base}_{Scalar (N Mat P)} = {Base}_{Scalar (N Mat P)}$
55	50 53 19 54	lmodvscl	$⊢ (N Mat P \in LMod \land {var}_{1} (R) \in {Base}_{Scalar (N Mat P)} \land 1_{(N Mat P)} \in {Base}_{(N Mat P)}) \to {var}_{1} (R) \cdot_{(N Mat P)} 1_{(N Mat P)} \in {Base}_{(N Mat P)}$
56	36 49 52 55	syl3anc	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to {var}_{1} (R) \cdot_{(N Mat P)} 1_{(N Mat P)} \in {Base}_{(N Mat P)}$
57	20 3 4 2 15	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to (N matToPolyMat R) (M) \in {Base}_{(N Mat P)}$
58	12 37 14 57	syl3anc	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to (N matToPolyMat R) (M) \in {Base}_{(N Mat P)}$
59	50 17	grpsubcl	$⊢ (N Mat P \in Grp \land {var}_{1} (R) \cdot_{(N Mat P)} 1_{(N Mat P)} \in {Base}_{(N Mat P)} \land (N matToPolyMat R) (M) \in {Base}_{(N Mat P)}) \to ({var}_{1} (R) \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M) \in {Base}_{(N Mat P)}$
60	34 56 58 59	syl3anc	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \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)}$
61	16 15 50	m1detdiag	$⊢ (P \in CRing \land (N = \{I\} \land I \in V) \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)) = I (({var}_{1} (R) \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) I$
62	25 26 60 61	syl3anc	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \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)) = I (({var}_{1} (R) \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) I$
63	5	eqcomi	$⊢ {var}_{1} (R) = X$
64	63	a1i	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to {var}_{1} (R) = X$
65	64	oveq1d	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to {var}_{1} (R) \cdot_{(N Mat P)} 1_{(N Mat P)} = X \cdot_{(N Mat P)} 1_{(N Mat P)}$
66	65	oveq1d	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to ({var}_{1} (R) \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M) = (X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)$
67	66	oveqd	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to I (({var}_{1} (R) \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) I = I ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) I$
68	1 2 3 4 5 6 7 15 20	chpmat1dlem	$⊢ (R \in Ring \land (N = \{I\} \land I \in V) \land M \in B) \to I ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) I = X \underset{˙}{-} S (I M I)$
69	27 68	syl3an1	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to I ((X \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) I = X \underset{˙}{-} S (I M I)$
70	67 69	eqtrd	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to I (({var}_{1} (R) \cdot_{(N Mat P)} 1_{(N Mat P)}) -_{(N Mat P)} (N matToPolyMat R) (M)) I = X \underset{˙}{-} S (I M I)$
71	62 70	eqtrd	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \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)) = X \underset{˙}{-} S (I M I)$
72	23 71	eqtrd	$⊢ (R \in CRing \land (N = \{I\} \land I \in V) \land M \in B) \to C (M) = X \underset{˙}{-} S (I M I)$

Metamath Proof Explorer

Theorem chpmat1d

Proof