cpmidgsumm2pm

Description: Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as group sum with a matrix to polynomial matrix transformation. (Contributed by AV, 13-Nov-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$
Assertion	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))$

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	1 2 3 4 5 6 7 8 9 10 11 12	cpmidgsum	$⊢ (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} (U ({coe}_{1} (K) (n)) \underset{˙}{\cdot} \underset{˙}{1}))$
17		3simpa	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land R \in CRing)$
18	17	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to (N \in Fin \land R \in CRing)$
19		eqid	$⊢ {Base}_{P} = {Base}_{P}$
20	10 1 2 3 19	chpmatply1	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to C (M) \in {Base}_{P}$
21	11 20	eqeltrid	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to K \in {Base}_{P}$
22		eqid	$⊢ {coe}_{1} (K) = {coe}_{1} (K)$
23		eqid	$⊢ {Base}_{R} = {Base}_{R}$
24	22 19 3 23	coe1fvalcl	$⊢ (K \in {Base}_{P} \land n \in ℕ_{0}) \to {coe}_{1} (K) (n) \in {Base}_{R}$
25	21 24	sylan	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to {coe}_{1} (K) (n) \in {Base}_{R}$
26		crngring	$⊢ R \in CRing \to R \in Ring$
27	26	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land R \in Ring)$
28	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
29	2 13	ringidcl	$⊢ A \in Ring \to O \in B$
30	27 28 29	3syl	$⊢ (N \in Fin \land R \in CRing) \to O \in B$
31	30	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to O \in B$
32	31	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to O \in B$
33		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
34	15 1 2 3 4 33 23 9 14 7	mat2pmatlin	$⊢ ((N \in Fin \land R \in CRing) \land ({coe}_{1} (K) (n) \in {Base}_{R} \land O \in B)) \to T ({coe}_{1} (K) (n) \underset{˙}{*} O) = U ({coe}_{1} (K) (n)) \underset{˙}{\cdot} T (O)$
35	18 25 32 34	syl12anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to T ({coe}_{1} (K) (n) \underset{˙}{*} O) = U ({coe}_{1} (K) (n)) \underset{˙}{\cdot} T (O)$
36	15 1 2 3 4 33	mat2pmatrhm	$⊢ (N \in Fin \land R \in CRing) \to T \in (A RingHom Y)$
37	13 8	rhm1	$⊢ T \in (A RingHom Y) \to T (O) = \underset{˙}{1}$
38	17 36 37	3syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to T (O) = \underset{˙}{1}$
39	38	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to T (O) = \underset{˙}{1}$
40	39	oveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to U ({coe}_{1} (K) (n)) \underset{˙}{\cdot} T (O) = U ({coe}_{1} (K) (n)) \underset{˙}{\cdot} \underset{˙}{1}$
41	35 40	eqtr2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to U ({coe}_{1} (K) (n)) \underset{˙}{\cdot} \underset{˙}{1} = T ({coe}_{1} (K) (n) \underset{˙}{*} O)$
42	41	oveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to (n \underset{˙}{\times} X) \underset{˙}{\cdot} (U ({coe}_{1} (K) (n)) \underset{˙}{\cdot} \underset{˙}{1}) = (n \underset{˙}{\times} X) \underset{˙}{\cdot} T ({coe}_{1} (K) (n) \underset{˙}{*} O)$
43	42	mpteq2dva	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (n \in ℕ_{0} ⟼ (n \underset{˙}{\times} X) \underset{˙}{\cdot} (U ({coe}_{1} (K) (n)) \underset{˙}{\cdot} \underset{˙}{1})) = (n \in ℕ_{0} ⟼ (n \underset{˙}{\times} X) \underset{˙}{\cdot} T ({coe}_{1} (K) (n) \underset{˙}{*} O))$
44	43	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} (U ({coe}_{1} (K) (n)) \underset{˙}{\cdot} \underset{˙}{1})) = \underset{n \in ℕ_{0}}{\sum_{Y}} ((n \underset{˙}{\times} X) \underset{˙}{\cdot} T ({coe}_{1} (K) (n) \underset{˙}{*} O))$
45	16 44	eqtrd	$⊢ (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))$

Metamath Proof Explorer

Theorem cpmidgsumm2pm

Proof