Theorem cpmidg2sum

Description: Equality of two sums representing the identity matrix multiplied with the characteristic polynomial of a matrix. (Contributed by AV, 11-Nov-2019)

	Ref	Expression
Hypotheses	cpmadugsum.a	$$⊢A=N\mathrm{Mat}R$$
	cpmadugsum.b	$$⊢B={\mathrm{Base}}_A$$
	cpmadugsum.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	cpmadugsum.y	$$⊢Y=N\mathrm{Mat}P$$
	cpmadugsum.t	$$⊢T=N\mathrm{matToPolyMat}R$$
	cpmadugsum.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	cpmadugsum.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
	cpmadugsum.m	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
	cpmadugsum.r	$$⊢\underset{\dot{}}{\times }={\cdot }_Y$$
	cpmadugsum.1	$$⊢\underset{\dot{}}{1}=1_Y$$
	cpmadugsum.g	$$⊢\underset{\dot{}}{+}={+}_Y$$
	cpmadugsum.s	$$⊢\underset{\dot{}}{-}={-}_Y$$
	cpmadugsum.i	$$⊢I=\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(M\right)$$
	cpmadugsum.j	$$⊢J=N\mathrm{maAdju}P$$
	cpmadugsum.0	$$⊢\underset{\dot{}}{0}=0_Y$$
	cpmadugsum.g2	$$⊢G=\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\underset{\dot{}}{0}\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(0\right)\right)\right),if\left(n=s+1,T\left(b\left(s\right)\right),if\left(s+1<n,\underset{\dot{}}{0},T\left(b\left(n-1\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(n\right)\right)\right)\right)\right)\right)\right)$$
	cpmidgsum2.c	$$⊢C=N\mathrm{CharPlyMat}R$$
	cpmidgsum2.k	$$⊢K=C\left(M\right)$$
	cpmidg2sum.u	$$⊢U=\mathrm{algSc}\left(P\right)$$
Assertion	cpmidg2sum	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \exists s\in \mathbb{N}\exists b\in \left(B^{\left(0\dots s\right)}\right)\underset{i\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}\left(U\left({\mathrm{coe}}_1\left(K\right)\left(i\right)\right)\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\right)=\underset{i\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}G\left(i\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cpmadugsum.a	$$⊢A=N\mathrm{Mat}R$$
2		cpmadugsum.b	$$⊢B={\mathrm{Base}}_A$$
3		cpmadugsum.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
4		cpmadugsum.y	$$⊢Y=N\mathrm{Mat}P$$
5		cpmadugsum.t	$$⊢T=N\mathrm{matToPolyMat}R$$
6		cpmadugsum.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
7		cpmadugsum.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
8		cpmadugsum.m	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
9		cpmadugsum.r	$$⊢\underset{\dot{}}{\times }={\cdot }_Y$$
10		cpmadugsum.1	$$⊢\underset{\dot{}}{1}=1_Y$$
11		cpmadugsum.g	$$⊢\underset{\dot{}}{+}={+}_Y$$
12		cpmadugsum.s	$$⊢\underset{\dot{}}{-}={-}_Y$$
13		cpmadugsum.i	$$⊢I=\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(M\right)$$
14		cpmadugsum.j	$$⊢J=N\mathrm{maAdju}P$$
15		cpmadugsum.0	$$⊢\underset{\dot{}}{0}=0_Y$$
16		cpmadugsum.g2	$$⊢G=\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\underset{\dot{}}{0}\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(0\right)\right)\right),if\left(n=s+1,T\left(b\left(s\right)\right),if\left(s+1<n,\underset{\dot{}}{0},T\left(b\left(n-1\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(n\right)\right)\right)\right)\right)\right)\right)$$
17		cpmidgsum2.c	$$⊢C=N\mathrm{CharPlyMat}R$$
18		cpmidgsum2.k	$$⊢K=C\left(M\right)$$
19		cpmidg2sum.u	$$⊢U=\mathrm{algSc}\left(P\right)$$
20		eqid	$$⊢K\underset{\dot{}}{·}\underset{\dot{}}{1}=K\underset{\dot{}}{·}\underset{\dot{}}{1}$$
21	1 2 3 4 6 7 8 10 19 17 18 20	cpmidgsum	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to K\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{i\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}\left(U\left({\mathrm{coe}}_1\left(K\right)\left(i\right)\right)\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\right)$$
22	21	eqcomd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \underset{i\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}\left(U\left({\mathrm{coe}}_1\left(K\right)\left(i\right)\right)\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\right)=K\underset{\dot{}}{·}\underset{\dot{}}{1}$$
23	22	ad3antrrr	$$⊢\left(\left(\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\wedge s\in \mathbb{N}\right)\wedge b\in \left(B^{\left(0\dots s\right)}\right)\right)\wedge K\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{i\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}G\left(i\right)\right)\right)\to \underset{i\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}\left(U\left({\mathrm{coe}}_1\left(K\right)\left(i\right)\right)\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\right)=K\underset{\dot{}}{·}\underset{\dot{}}{1}$$
24		simpr	$$⊢\left(\left(\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\wedge s\in \mathbb{N}\right)\wedge b\in \left(B^{\left(0\dots s\right)}\right)\right)\wedge K\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{i\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}G\left(i\right)\right)\right)\to K\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{i\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}G\left(i\right)\right)$$
25	23 24	eqtrd	$$⊢\left(\left(\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\wedge s\in \mathbb{N}\right)\wedge b\in \left(B^{\left(0\dots s\right)}\right)\right)\wedge K\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{i\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}G\left(i\right)\right)\right)\to \underset{i\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}\left(U\left({\mathrm{coe}}_1\left(K\right)\left(i\right)\right)\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\right)=\underset{i\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}G\left(i\right)\right)$$
26	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 20	cpmidgsum2	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \exists s\in \mathbb{N}\exists b\in \left(B^{\left(0\dots s\right)}\right)K\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{i\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}G\left(i\right)\right)$$
27	25 26	reximddv2	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \exists s\in \mathbb{N}\exists b\in \left(B^{\left(0\dots s\right)}\right)\underset{i\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}\left(U\left({\mathrm{coe}}_1\left(K\right)\left(i\right)\right)\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\right)=\underset{i\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}G\left(i\right)\right)$$