cpmidpmat

Description: Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as polynomial over the ring of matrices. (Contributed by AV, 14-Nov-2019) (Revised by AV, 7-Dec-2019)

	Ref	Expression
Hypotheses	cpmidgsum.a	$⊢ A = N Mat R$
	cpmidgsum.b	$⊢ B = {Base}_{A}$
	cpmidgsum.p	$⊢ P = {Poly}_{1} (R)$
	cpmidgsum.y	$⊢ Y = N Mat P$
	cpmidgsum.x	$⊢ X = {var}_{1} (R)$
	cpmidgsum.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	cpmidgsum.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
	cpmidgsum.1	$⊢ \underset{˙}{1} = 1_{Y}$
	cpmidgsum.u	$⊢ U = algSc (P)$
	cpmidgsum.c	$⊢ C = N CharPlyMat R$
	cpmidgsum.k	$⊢ K = C (M)$
	cpmidgsum.h	$⊢ H = K \underset{˙}{\cdot} \underset{˙}{1}$
	cpmidgsumm2pm.o	$⊢ O = 1_{A}$
	cpmidgsumm2pm.m	$⊢ \underset{˙}{*} = \cdot_{A}$
	cpmidgsumm2pm.t	$⊢ T = N matToPolyMat R$
	cpmidgsum.w	$⊢ W = {Base}_{Y}$
	cpmidpmat.p	$⊢ Q = {Poly}_{1} (A)$
	cpmidpmat.z	$⊢ Z = {var}_{1} (A)$
	cpmidpmat.m	$⊢ \underset{˙}{∙} = \cdot_{Q}$
	cpmidpmat.e	$⊢ E = \cdot_{{mulGrp}_{Q}}$
	cpmidpmat.i	$⊢ I = N pMatToMatPoly R$
Assertion	cpmidpmat	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to I (H) = \underset{n \in ℕ_{0}}{\sum_{Q}} (({coe}_{1} (K) (n) \underset{˙}{*} O) \underset{˙}{∙} (n E Z))$

Proof

Step	Hyp	Ref	Expression
1		cpmidgsum.a	$⊢ A = N Mat R$
2		cpmidgsum.b	$⊢ B = {Base}_{A}$
3		cpmidgsum.p	$⊢ P = {Poly}_{1} (R)$
4		cpmidgsum.y	$⊢ Y = N Mat P$
5		cpmidgsum.x	$⊢ X = {var}_{1} (R)$
6		cpmidgsum.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
7		cpmidgsum.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
8		cpmidgsum.1	$⊢ \underset{˙}{1} = 1_{Y}$
9		cpmidgsum.u	$⊢ U = algSc (P)$
10		cpmidgsum.c	$⊢ C = N CharPlyMat R$
11		cpmidgsum.k	$⊢ K = C (M)$
12		cpmidgsum.h	$⊢ H = K \underset{˙}{\cdot} \underset{˙}{1}$
13		cpmidgsumm2pm.o	$⊢ O = 1_{A}$
14		cpmidgsumm2pm.m	$⊢ \underset{˙}{*} = \cdot_{A}$
15		cpmidgsumm2pm.t	$⊢ T = N matToPolyMat R$
16		cpmidgsum.w	$⊢ W = {Base}_{Y}$
17		cpmidpmat.p	$⊢ Q = {Poly}_{1} (A)$
18		cpmidpmat.z	$⊢ Z = {var}_{1} (A)$
19		cpmidpmat.m	$⊢ \underset{˙}{∙} = \cdot_{Q}$
20		cpmidpmat.e	$⊢ E = \cdot_{{mulGrp}_{Q}}$
21		cpmidpmat.i	$⊢ I = N pMatToMatPoly R$
22	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	cpmidgsumm2pm	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to H = \underset{n \in ℕ_{0}}{\sum_{Y}} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T ({coe}_{1} (K) (n) \underset{˙}{*} O))$
23	22	fveq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to I (H) = I (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T ({coe}_{1} (K) (n) \underset{˙}{*} O)))$
24		eqid	$⊢ (k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) = (k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O)$
25	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 24	cpmidpmatlem1	$⊢ n \in ℕ_{0} \to (k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n) = {coe}_{1} (K) (n) \underset{˙}{} O$
26	25	eqcomd	$⊢ n \in ℕ_{0} \to {coe}_{1} (K) (n) \underset{˙}{} O = (k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n)$
27	26	adantl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to {coe}_{1} (K) (n) \underset{˙}{} O = (k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n)$
28	27	fveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to T ({coe}_{1} (K) (n) \underset{˙}{} O) = T ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n))$
29	28	oveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to (n \underset{˙}{\times} X) \underset{˙}{\cdot} T ({coe}_{1} (K) (n) \underset{˙}{} O) = (n \underset{˙}{\times} X) \underset{˙}{\cdot} T ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n))$
30	29	mpteq2dva	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (n \in ℕ_{0} ⟼ (n \underset{˙}{\times} X) \underset{˙}{\cdot} T ({coe}_{1} (K) (n) \underset{˙}{} O)) = (n \in ℕ_{0} ⟼ (n \underset{˙}{\times} X) \underset{˙}{\cdot} T ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n)))$
31	30	oveq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \underset{n \in ℕ_{0}}{\sum_{Y}} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T ({coe}_{1} (K) (n) \underset{˙}{} O)) = \underset{n \in ℕ_{0}}{\sum_{Y}} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n)))$
32	31	fveq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to I (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T ({coe}_{1} (K) (n) \underset{˙}{} O))) = I (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n))))$
33		3simpa	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land R \in CRing)$
34	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 24	cpmidpmatlem2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{*} O) \in (B^{ℕ_{0}})$
35	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 24	cpmidpmatlem3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{*} O))$
36		fveq2	$⊢ k = x \to {coe}_{1} (K) (k) = {coe}_{1} (K) (x)$
37	36	oveq1d	$⊢ k = x \to {coe}_{1} (K) (k) \underset{˙}{} O = {coe}_{1} (K) (x) \underset{˙}{} O$
38	37	cbvmptv	$⊢ (k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) = (x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O)$
39	38	eleq1i	$⊢ (k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) \in (B^{ℕ_{0}}) \leftrightarrow (x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O) \in (B^{ℕ_{0}})$
40	38	breq1i	$⊢ {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O)) \leftrightarrow {finSupp}_{0_{A}} ((x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O))$
41	39 40	anbi12i	$⊢ ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) \in (B^{ℕ_{0}}) \land {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O))) \leftrightarrow ((x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O) \in (B^{ℕ_{0}}) \land {finSupp}_{0_{A}} ((x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O)))$
42	3 4 16 19 20 18 1 2 17 21 6 5 7 15	pm2mp	$⊢ ((N \in Fin \land R \in CRing) \land ((x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O) \in (B^{ℕ_{0}}) \land {finSupp}_{0_{A}} ((x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O)))) \to I (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T ((x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O) (n)))) = \underset{n \in ℕ_{0}}{\sum_{Q}} ((x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O) (n) \underset{˙}{∙} (n E Z))$
43	41 42	sylan2b	$⊢ ((N \in Fin \land R \in CRing) \land ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) \in (B^{ℕ_{0}}) \land {finSupp}_{0_{A}} ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O)))) \to I (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T ((x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O) (n)))) = \underset{n \in ℕ_{0}}{\sum_{Q}} ((x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O) (n) \underset{˙}{∙} (n E Z))$
44	33 34 35 43	syl12anc	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to I (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T ((x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O) (n)))) = \underset{n \in ℕ_{0}}{\sum_{Q}} ((x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O) (n) \underset{˙}{∙} (n E Z))$
45	38	fveq1i	$⊢ (k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n) = (x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O) (n)$
46	45	fveq2i	$⊢ T ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n)) = T ((x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O) (n))$
47	46	oveq2i	$⊢ (n \underset{˙}{\times} X) \underset{˙}{\cdot} T ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n)) = (n \underset{˙}{\times} X) \underset{˙}{\cdot} T ((x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O) (n))$
48	47	mpteq2i	$⊢ (n \in ℕ_{0} ⟼ (n \underset{˙}{\times} X) \underset{˙}{\cdot} T ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n))) = (n \in ℕ_{0} ⟼ (n \underset{˙}{\times} X) \underset{˙}{\cdot} T ((x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O) (n)))$
49	48	oveq2i	$⊢ \underset{n \in ℕ_{0}}{\sum_{Y}} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n))) = \underset{n \in ℕ_{0}}{\sum_{Y}} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T ((x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O) (n)))$
50	49	fveq2i	$⊢ I (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n)))) = I (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T ((x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O) (n))))$
51	45	oveq1i	$⊢ (k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n) \underset{˙}{∙} (n E Z) = (x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O) (n) \underset{˙}{∙} (n E Z)$
52	51	mpteq2i	$⊢ (n \in ℕ_{0} ⟼ (k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n) \underset{˙}{∙} (n E Z)) = (n \in ℕ_{0} ⟼ (x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O) (n) \underset{˙}{∙} (n E Z))$
53	52	oveq2i	$⊢ \underset{n \in ℕ_{0}}{\sum_{Q}} ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n) \underset{˙}{∙} (n E Z)) = \underset{n \in ℕ_{0}}{\sum_{Q}} ((x \in ℕ_{0} ⟼ {coe}_{1} (K) (x) \underset{˙}{} O) (n) \underset{˙}{∙} (n E Z))$
54	44 50 53	3eqtr4g	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to I (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n)))) = \underset{n \in ℕ_{0}}{\sum_{Q}} ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n) \underset{˙}{∙} (n E Z))$
55	32 54	eqtrd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to I (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T ({coe}_{1} (K) (n) \underset{˙}{} O))) = \underset{n \in ℕ_{0}}{\sum_{Q}} ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n) \underset{˙}{∙} (n E Z))$
56	25	adantl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n) = {coe}_{1} (K) (n) \underset{˙}{} O$
57	56	oveq1d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n) \underset{˙}{∙} (n E Z) = ({coe}_{1} (K) (n) \underset{˙}{} O) \underset{˙}{∙} (n E Z)$
58	57	mpteq2dva	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (n \in ℕ_{0} ⟼ (k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n) \underset{˙}{∙} (n E Z)) = (n \in ℕ_{0} ⟼ ({coe}_{1} (K) (n) \underset{˙}{} O) \underset{˙}{∙} (n E Z))$
59	58	oveq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \underset{n \in ℕ_{0}}{\sum_{Q}} ((k \in ℕ_{0} ⟼ {coe}_{1} (K) (k) \underset{˙}{} O) (n) \underset{˙}{∙} (n E Z)) = \underset{n \in ℕ_{0}}{\sum_{Q}} (({coe}_{1} (K) (n) \underset{˙}{} O) \underset{˙}{∙} (n E Z))$
60	23 55 59	3eqtrd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to I (H) = \underset{n \in ℕ_{0}}{\sum_{Q}} (({coe}_{1} (K) (n) \underset{˙}{*} O) \underset{˙}{∙} (n E Z))$

Metamath Proof Explorer

Theorem cpmidpmat

Proof