Theorem cpmidgsum

Description: Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as group sum. (Contributed by AV, 7-Nov-2019)

	Ref	Expression
Hypotheses	cpmidgsum.a	$$⊢A=N\mathrm{Mat}R$$
	cpmidgsum.b	$$⊢B={\mathrm{Base}}_A$$
	cpmidgsum.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	cpmidgsum.y	$$⊢Y=N\mathrm{Mat}P$$
	cpmidgsum.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	cpmidgsum.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
	cpmidgsum.m	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
	cpmidgsum.1	$$⊢\underset{\dot{}}{1}=1_Y$$
	cpmidgsum.u	$$⊢U=\mathrm{algSc}\left(P\right)$$
	cpmidgsum.c	$$⊢C=N\mathrm{CharPlyMat}R$$
	cpmidgsum.k	$$⊢K=C\left(M\right)$$
	cpmidgsum.h	$$⊢H=K\underset{\dot{}}{·}\underset{\dot{}}{1}$$
Assertion	cpmidgsum	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to H=\underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}\left(U\left({\mathrm{coe}}_1\left(K\right)\left(n\right)\right)\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cpmidgsum.a	$$⊢A=N\mathrm{Mat}R$$
2		cpmidgsum.b	$$⊢B={\mathrm{Base}}_A$$
3		cpmidgsum.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
4		cpmidgsum.y	$$⊢Y=N\mathrm{Mat}P$$
5		cpmidgsum.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
6		cpmidgsum.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
7		cpmidgsum.m	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
8		cpmidgsum.1	$$⊢\underset{\dot{}}{1}=1_Y$$
9		cpmidgsum.u	$$⊢U=\mathrm{algSc}\left(P\right)$$
10		cpmidgsum.c	$$⊢C=N\mathrm{CharPlyMat}R$$
11		cpmidgsum.k	$$⊢K=C\left(M\right)$$
12		cpmidgsum.h	$$⊢H=K\underset{\dot{}}{·}\underset{\dot{}}{1}$$
13		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
14	10 1 2 3 13	chpmatply1	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to C\left(M\right)\in {\mathrm{Base}}_P$$
15	11 14	eqeltrid	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to K\in {\mathrm{Base}}_P$$
16		eqid	$$⊢{\mathrm{Base}}_Y={\mathrm{Base}}_Y$$
17		eqid	$$⊢N\mathrm{matToPolyMat}R=N\mathrm{matToPolyMat}R$$
18		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
19	3 4 16 7 6 5 17 1 2 9 18 13 9 8 12	pmatcollpwscmat	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge K\in {\mathrm{Base}}_P\right)\to H=\underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}\left(U\left({\mathrm{coe}}_1\left(K\right)\left(n\right)\right)\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\right)$$
20	15 19	syld3an3	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to H=\underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}\left(U\left({\mathrm{coe}}_1\left(K\right)\left(n\right)\right)\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\right)$$