chpscmat

Description: The characteristic polynomial of a (nonempty!) scalar matrix. (Contributed by AV, 21-Aug-2019)

	Ref	Expression
Hypotheses	chp0mat.c	$⊢ C = N CharPlyMat R$
	chp0mat.p	$⊢ P = {Poly}_{1} (R)$
	chp0mat.a	$⊢ A = N Mat R$
	chp0mat.x	$⊢ X = {var}_{1} (R)$
	chp0mat.g	$⊢ G = {mulGrp}_{P}$
	chp0mat.m	$⊢ \underset{˙}{\times} = \cdot_{G}$
	chpscmat.d	$⊢ D = \{m \in {Base}_{A} \| \exists c \in {Base}_{R} \forall i \in N \forall j \in N i m j = if (i = j, c, 0_{R})\}$
	chpscmat.s	$⊢ S = algSc (P)$
	chpscmat.m	$⊢ \underset{˙}{-} = -_{P}$
Assertion	chpscmat	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land I \in N \land \forall n \in N n M n = E)) \to C (M) = \|N\| \underset{˙}{\times} (X \underset{˙}{-} S (E))$

Proof

Step	Hyp	Ref	Expression
1		chp0mat.c	$⊢ C = N CharPlyMat R$
2		chp0mat.p	$⊢ P = {Poly}_{1} (R)$
3		chp0mat.a	$⊢ A = N Mat R$
4		chp0mat.x	$⊢ X = {var}_{1} (R)$
5		chp0mat.g	$⊢ G = {mulGrp}_{P}$
6		chp0mat.m	$⊢ \underset{˙}{\times} = \cdot_{G}$
7		chpscmat.d	$⊢ D = \{m \in {Base}_{A} \| \exists c \in {Base}_{R} \forall i \in N \forall j \in N i m j = if (i = j, c, 0_{R})\}$
8		chpscmat.s	$⊢ S = algSc (P)$
9		chpscmat.m	$⊢ \underset{˙}{-} = -_{P}$
10		simpll	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land I \in N \land \forall n \in N n M n = E)) \to N \in Fin$
11		simplr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land I \in N \land \forall n \in N n M n = E)) \to R \in CRing$
12		elrabi	$⊢ M \in \{m \in {Base}_{A} \| \exists c \in {Base}_{R} \forall i \in N \forall j \in N i m j = if (i = j, c, 0_{R})\} \to M \in {Base}_{A}$
13	12 7	eleq2s	$⊢ M \in D \to M \in {Base}_{A}$
14	13	3ad2ant1	$⊢ (M \in D \land I \in N \land \forall n \in N n M n = E) \to M \in {Base}_{A}$
15	14	adantl	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land I \in N \land \forall n \in N n M n = E)) \to M \in {Base}_{A}$
16		oveq	$⊢ m = M \to i m j = i M j$
17	16	eqeq1d	$⊢ m = M \to (i m j = if (i = j, c, 0_{R}) \leftrightarrow i M j = if (i = j, c, 0_{R}))$
18	17	2ralbidv	$⊢ m = M \to (\forall i \in N \forall j \in N i m j = if (i = j, c, 0_{R}) \leftrightarrow \forall i \in N \forall j \in N i M j = if (i = j, c, 0_{R}))$
19	18	rexbidv	$⊢ m = M \to (\exists c \in {Base}_{R} \forall i \in N \forall j \in N i m j = if (i = j, c, 0_{R}) \leftrightarrow \exists c \in {Base}_{R} \forall i \in N \forall j \in N i M j = if (i = j, c, 0_{R}))$
20	19	elrab	$⊢ M \in \{m \in {Base}_{A} \| \exists c \in {Base}_{R} \forall i \in N \forall j \in N i m j = if (i = j, c, 0_{R})\} \leftrightarrow (M \in {Base}_{A} \land \exists c \in {Base}_{R} \forall i \in N \forall j \in N i M j = if (i = j, c, 0_{R}))$
21		ifnefalse	$⊢ i \neq j \to if (i = j, c, 0_{R}) = 0_{R}$
22	21	eqeq2d	$⊢ i \neq j \to (i M j = if (i = j, c, 0_{R}) \leftrightarrow i M j = 0_{R})$
23	22	biimpcd	$⊢ i M j = if (i = j, c, 0_{R}) \to (i \neq j \to i M j = 0_{R})$
24	23	a1i	$⊢ ((((M \in {Base}_{A} \land c \in {Base}_{R}) \land (N \in Fin \land R \in CRing)) \land i \in N) \land j \in N) \to (i M j = if (i = j, c, 0_{R}) \to (i \neq j \to i M j = 0_{R}))$
25	24	ralimdva	$⊢ (((M \in {Base}_{A} \land c \in {Base}_{R}) \land (N \in Fin \land R \in CRing)) \land i \in N) \to (\forall j \in N i M j = if (i = j, c, 0_{R}) \to \forall j \in N (i \neq j \to i M j = 0_{R}))$
26	25	ralimdva	$⊢ ((M \in {Base}_{A} \land c \in {Base}_{R}) \land (N \in Fin \land R \in CRing)) \to (\forall i \in N \forall j \in N i M j = if (i = j, c, 0_{R}) \to \forall i \in N \forall j \in N (i \neq j \to i M j = 0_{R}))$
27	26	ex	$⊢ (M \in {Base}_{A} \land c \in {Base}_{R}) \to ((N \in Fin \land R \in CRing) \to (\forall i \in N \forall j \in N i M j = if (i = j, c, 0_{R}) \to \forall i \in N \forall j \in N (i \neq j \to i M j = 0_{R})))$
28	27	com23	$⊢ (M \in {Base}_{A} \land c \in {Base}_{R}) \to (\forall i \in N \forall j \in N i M j = if (i = j, c, 0_{R}) \to ((N \in Fin \land R \in CRing) \to \forall i \in N \forall j \in N (i \neq j \to i M j = 0_{R})))$
29	28	rexlimdva	$⊢ M \in {Base}_{A} \to (\exists c \in {Base}_{R} \forall i \in N \forall j \in N i M j = if (i = j, c, 0_{R}) \to ((N \in Fin \land R \in CRing) \to \forall i \in N \forall j \in N (i \neq j \to i M j = 0_{R})))$
30	29	imp	$⊢ (M \in {Base}_{A} \land \exists c \in {Base}_{R} \forall i \in N \forall j \in N i M j = if (i = j, c, 0_{R})) \to ((N \in Fin \land R \in CRing) \to \forall i \in N \forall j \in N (i \neq j \to i M j = 0_{R}))$
31	20 30	sylbi	$⊢ M \in \{m \in {Base}_{A} \| \exists c \in {Base}_{R} \forall i \in N \forall j \in N i m j = if (i = j, c, 0_{R})\} \to ((N \in Fin \land R \in CRing) \to \forall i \in N \forall j \in N (i \neq j \to i M j = 0_{R}))$
32	31 7	eleq2s	$⊢ M \in D \to ((N \in Fin \land R \in CRing) \to \forall i \in N \forall j \in N (i \neq j \to i M j = 0_{R}))$
33	32	3ad2ant1	$⊢ (M \in D \land I \in N \land \forall n \in N n M n = E) \to ((N \in Fin \land R \in CRing) \to \forall i \in N \forall j \in N (i \neq j \to i M j = 0_{R}))$
34	33	impcom	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land I \in N \land \forall n \in N n M n = E)) \to \forall i \in N \forall j \in N (i \neq j \to i M j = 0_{R})$
35		eqid	$⊢ {Base}_{A} = {Base}_{A}$
36		eqid	$⊢ 0_{R} = 0_{R}$
37	1 2 3 8 35 4 36 5 9	chpdmat	$⊢ ((N \in Fin \land R \in CRing \land M \in {Base}_{A}) \land \forall i \in N \forall j \in N (i \neq j \to i M j = 0_{R})) \to C (M) = \underset{k \in N}{\sum_{G}} (X \underset{˙}{-} S (k M k))$
38	10 11 15 34 37	syl31anc	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land I \in N \land \forall n \in N n M n = E)) \to C (M) = \underset{k \in N}{\sum_{G}} (X \underset{˙}{-} S (k M k))$
39		id	$⊢ n = k \to n = k$
40	39 39	oveq12d	$⊢ n = k \to n M n = k M k$
41	40	eqeq1d	$⊢ n = k \to (n M n = E \leftrightarrow k M k = E)$
42	41	rspccv	$⊢ \forall n \in N n M n = E \to (k \in N \to k M k = E)$
43	42	3ad2ant3	$⊢ (M \in D \land I \in N \land \forall n \in N n M n = E) \to (k \in N \to k M k = E)$
44	43	adantl	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land I \in N \land \forall n \in N n M n = E)) \to (k \in N \to k M k = E)$
45	44	imp	$⊢ (((N \in Fin \land R \in CRing) \land (M \in D \land I \in N \land \forall n \in N n M n = E)) \land k \in N) \to k M k = E$
46	45	fveq2d	$⊢ (((N \in Fin \land R \in CRing) \land (M \in D \land I \in N \land \forall n \in N n M n = E)) \land k \in N) \to S (k M k) = S (E)$
47	46	oveq2d	$⊢ (((N \in Fin \land R \in CRing) \land (M \in D \land I \in N \land \forall n \in N n M n = E)) \land k \in N) \to X \underset{˙}{-} S (k M k) = X \underset{˙}{-} S (E)$
48	47	mpteq2dva	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land I \in N \land \forall n \in N n M n = E)) \to (k \in N ⟼ X \underset{˙}{-} S (k M k)) = (k \in N ⟼ X \underset{˙}{-} S (E))$
49	48	oveq2d	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land I \in N \land \forall n \in N n M n = E)) \to \underset{k \in N}{\sum_{G}} (X \underset{˙}{-} S (k M k)) = \underset{k \in N}{\sum_{G}} (X \underset{˙}{-} S (E))$
50	2	ply1crng	$⊢ R \in CRing \to P \in CRing$
51	5	crngmgp	$⊢ P \in CRing \to G \in CMnd$
52		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
53	50 51 52	3syl	$⊢ R \in CRing \to G \in Mnd$
54	53	ad2antlr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land I \in N \land \forall n \in N n M n = E)) \to G \in Mnd$
55		crngring	$⊢ R \in CRing \to R \in Ring$
56	2	ply1ring	$⊢ R \in Ring \to P \in Ring$
57	55 56	syl	$⊢ R \in CRing \to P \in Ring$
58		ringgrp	$⊢ P \in Ring \to P \in Grp$
59	57 58	syl	$⊢ R \in CRing \to P \in Grp$
60	59	ad2antlr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land I \in N \land \forall n \in N n M n = E)) \to P \in Grp$
61		eqid	$⊢ {Base}_{P} = {Base}_{P}$
62	4 2 61	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
63	55 62	syl	$⊢ R \in CRing \to X \in {Base}_{P}$
64	63	ad2antlr	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land I \in N \land \forall n \in N n M n = E)) \to X \in {Base}_{P}$
65		simpr	$⊢ ((M \in D \land (N \in Fin \land R \in CRing)) \land I \in N) \to I \in N$
66		eqid	$⊢ Scalar (P) = Scalar (P)$
67	57	ad2antll	$⊢ (M \in D \land (N \in Fin \land R \in CRing)) \to P \in Ring$
68	67	adantr	$⊢ ((M \in D \land (N \in Fin \land R \in CRing)) \land I \in N) \to P \in Ring$
69	2	ply1lmod	$⊢ R \in Ring \to P \in LMod$
70	55 69	syl	$⊢ R \in CRing \to P \in LMod$
71	70	ad2antll	$⊢ (M \in D \land (N \in Fin \land R \in CRing)) \to P \in LMod$
72	71	adantr	$⊢ ((M \in D \land (N \in Fin \land R \in CRing)) \land I \in N) \to P \in LMod$
73		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
74	8 66 68 72 73 61	asclf	$⊢ ((M \in D \land (N \in Fin \land R \in CRing)) \land I \in N) \to S : {Base}_{Scalar (P)} ⟶ {Base}_{P}$
75	13	adantr	$⊢ (M \in D \land (N \in Fin \land R \in CRing)) \to M \in {Base}_{A}$
76	75	adantr	$⊢ ((M \in D \land (N \in Fin \land R \in CRing)) \land I \in N) \to M \in {Base}_{A}$
77		eqid	$⊢ {Base}_{R} = {Base}_{R}$
78	3 77	matecl	$⊢ (I \in N \land I \in N \land M \in {Base}_{A}) \to I M I \in {Base}_{R}$
79	65 65 76 78	syl3anc	$⊢ ((M \in D \land (N \in Fin \land R \in CRing)) \land I \in N) \to I M I \in {Base}_{R}$
80	2	ply1sca	$⊢ R \in CRing \to R = Scalar (P)$
81	80	ad2antll	$⊢ (M \in D \land (N \in Fin \land R \in CRing)) \to R = Scalar (P)$
82	81	adantr	$⊢ ((M \in D \land (N \in Fin \land R \in CRing)) \land I \in N) \to R = Scalar (P)$
83	82	eqcomd	$⊢ ((M \in D \land (N \in Fin \land R \in CRing)) \land I \in N) \to Scalar (P) = R$
84	83	fveq2d	$⊢ ((M \in D \land (N \in Fin \land R \in CRing)) \land I \in N) \to {Base}_{Scalar (P)} = {Base}_{R}$
85	79 84	eleqtrrd	$⊢ ((M \in D \land (N \in Fin \land R \in CRing)) \land I \in N) \to I M I \in {Base}_{Scalar (P)}$
86	74 85	ffvelrnd	$⊢ ((M \in D \land (N \in Fin \land R \in CRing)) \land I \in N) \to S (I M I) \in {Base}_{P}$
87		fveq2	$⊢ E = I M I \to S (E) = S (I M I)$
88	87	eqcoms	$⊢ I M I = E \to S (E) = S (I M I)$
89	88	eleq1d	$⊢ I M I = E \to (S (E) \in {Base}_{P} \leftrightarrow S (I M I) \in {Base}_{P})$
90	86 89	syl5ibrcom	$⊢ ((M \in D \land (N \in Fin \land R \in CRing)) \land I \in N) \to (I M I = E \to S (E) \in {Base}_{P})$
91	90	adantr	$⊢ (((M \in D \land (N \in Fin \land R \in CRing)) \land I \in N) \land n = I) \to (I M I = E \to S (E) \in {Base}_{P})$
92		id	$⊢ n = I \to n = I$
93	92 92	oveq12d	$⊢ n = I \to n M n = I M I$
94	93	eqeq1d	$⊢ n = I \to (n M n = E \leftrightarrow I M I = E)$
95	94	imbi1d	$⊢ n = I \to ((n M n = E \to S (E) \in {Base}_{P}) \leftrightarrow (I M I = E \to S (E) \in {Base}_{P}))$
96	95	adantl	$⊢ (((M \in D \land (N \in Fin \land R \in CRing)) \land I \in N) \land n = I) \to ((n M n = E \to S (E) \in {Base}_{P}) \leftrightarrow (I M I = E \to S (E) \in {Base}_{P}))$
97	91 96	mpbird	$⊢ (((M \in D \land (N \in Fin \land R \in CRing)) \land I \in N) \land n = I) \to (n M n = E \to S (E) \in {Base}_{P})$
98	65 97	rspcimdv	$⊢ ((M \in D \land (N \in Fin \land R \in CRing)) \land I \in N) \to (\forall n \in N n M n = E \to S (E) \in {Base}_{P})$
99	98	ex	$⊢ (M \in D \land (N \in Fin \land R \in CRing)) \to (I \in N \to (\forall n \in N n M n = E \to S (E) \in {Base}_{P}))$
100	99	com23	$⊢ (M \in D \land (N \in Fin \land R \in CRing)) \to (\forall n \in N n M n = E \to (I \in N \to S (E) \in {Base}_{P}))$
101	100	ex	$⊢ M \in D \to ((N \in Fin \land R \in CRing) \to (\forall n \in N n M n = E \to (I \in N \to S (E) \in {Base}_{P})))$
102	101	com24	$⊢ M \in D \to (I \in N \to (\forall n \in N n M n = E \to ((N \in Fin \land R \in CRing) \to S (E) \in {Base}_{P})))$
103	102	3imp	$⊢ (M \in D \land I \in N \land \forall n \in N n M n = E) \to ((N \in Fin \land R \in CRing) \to S (E) \in {Base}_{P})$
104	103	impcom	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land I \in N \land \forall n \in N n M n = E)) \to S (E) \in {Base}_{P}$
105	61 9	grpsubcl	$⊢ (P \in Grp \land X \in {Base}_{P} \land S (E) \in {Base}_{P}) \to X \underset{˙}{-} S (E) \in {Base}_{P}$
106	60 64 104 105	syl3anc	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land I \in N \land \forall n \in N n M n = E)) \to X \underset{˙}{-} S (E) \in {Base}_{P}$
107	5 61	mgpbas	$⊢ {Base}_{P} = {Base}_{G}$
108	106 107	eleqtrdi	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land I \in N \land \forall n \in N n M n = E)) \to X \underset{˙}{-} S (E) \in {Base}_{G}$
109		eqid	$⊢ {Base}_{G} = {Base}_{G}$
110	109 6	gsumconst	$⊢ (G \in Mnd \land N \in Fin \land X \underset{˙}{-} S (E) \in {Base}_{G}) \to \underset{k \in N}{\sum_{G}} (X \underset{˙}{-} S (E)) = \|N\| \underset{˙}{\times} (X \underset{˙}{-} S (E))$
111	54 10 108 110	syl3anc	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land I \in N \land \forall n \in N n M n = E)) \to \underset{k \in N}{\sum_{G}} (X \underset{˙}{-} S (E)) = \|N\| \underset{˙}{\times} (X \underset{˙}{-} S (E))$
112	38 49 111	3eqtrd	$⊢ ((N \in Fin \land R \in CRing) \land (M \in D \land I \in N \land \forall n \in N n M n = E)) \to C (M) = \|N\| \underset{˙}{\times} (X \underset{˙}{-} S (E))$

Metamath Proof Explorer

Theorem chpscmat

Proof