Theorem cpmadugsum

Description: The product of the characteristic matrix of a given matrix and its adjunct represented as an infinite sum. (Contributed by AV, 10-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)$$
Assertion	cpmadugsum	$$⊢\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)I\underset{\dot{}}{\times }J\left(I\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	1 2 3 4 5 6 7 8 9 10 11 12 13 14	cpmadugsumfi	$$⊢\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)I\underset{\dot{}}{\times }J\left(I\right)=\left(\underset{i=1}{\overset{s}{{\sum }_Y}},\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}\left(T\left(b\left(i-1\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(i\right)\right)\right)\right)\right)\right)\underset{\dot{}}{+}\left(\left(\left(\left(s+1\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}T\left(b\left(s\right)\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(0\right)\right)\right)\right)$$
18		simpr	$$⊢\left(\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left(s\in \mathbb{N}\wedge b\in \left(B^{\left(0\dots s\right)}\right)\right)\right)\wedge I\underset{\dot{}}{\times }J\left(I\right)=\left(\underset{i=1}{\overset{s}{{\sum }_Y}},\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}\left(T\left(b\left(i-1\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(i\right)\right)\right)\right)\right)\right)\underset{\dot{}}{+}\left(\left(\left(\left(s+1\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}T\left(b\left(s\right)\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(0\right)\right)\right)\right)\right)\to I\underset{\dot{}}{\times }J\left(I\right)=\left(\underset{i=1}{\overset{s}{{\sum }_Y}},\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}\left(T\left(b\left(i-1\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(i\right)\right)\right)\right)\right)\right)\underset{\dot{}}{+}\left(\left(\left(\left(s+1\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}T\left(b\left(s\right)\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(0\right)\right)\right)\right)$$
19	1 2 3 4 9 12 15 5 16 6 8 7 11	chfacfscmulgsum	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left(s\in \mathbb{N}\wedge b\in \left(B^{\left(0\dots s\right)}\right)\right)\right)\to \underset{i\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}G\left(i\right)\right)=\left(\underset{i=1}{\overset{s}{{\sum }_Y}},\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}\left(T\left(b\left(i-1\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(i\right)\right)\right)\right)\right)\right)\underset{\dot{}}{+}\left(\left(\left(\left(s+1\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}T\left(b\left(s\right)\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(0\right)\right)\right)\right)$$
20	19	eqcomd	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left(s\in \mathbb{N}\wedge b\in \left(B^{\left(0\dots s\right)}\right)\right)\right)\to \left(\underset{i=1}{\overset{s}{{\sum }_Y}},\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}\left(T\left(b\left(i-1\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(i\right)\right)\right)\right)\right)\right)\underset{\dot{}}{+}\left(\left(\left(\left(s+1\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}T\left(b\left(s\right)\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(0\right)\right)\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)$$
21	20	adantr	$$⊢\left(\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left(s\in \mathbb{N}\wedge b\in \left(B^{\left(0\dots s\right)}\right)\right)\right)\wedge I\underset{\dot{}}{\times }J\left(I\right)=\left(\underset{i=1}{\overset{s}{{\sum }_Y}},\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}\left(T\left(b\left(i-1\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(i\right)\right)\right)\right)\right)\right)\underset{\dot{}}{+}\left(\left(\left(\left(s+1\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}T\left(b\left(s\right)\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(0\right)\right)\right)\right)\right)\to \left(\underset{i=1}{\overset{s}{{\sum }_Y}},\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}\left(T\left(b\left(i-1\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(i\right)\right)\right)\right)\right)\right)\underset{\dot{}}{+}\left(\left(\left(\left(s+1\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}T\left(b\left(s\right)\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(0\right)\right)\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)$$
22	18 21	eqtrd	$$⊢\left(\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left(s\in \mathbb{N}\wedge b\in \left(B^{\left(0\dots s\right)}\right)\right)\right)\wedge I\underset{\dot{}}{\times }J\left(I\right)=\left(\underset{i=1}{\overset{s}{{\sum }_Y}},\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}\left(T\left(b\left(i-1\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(i\right)\right)\right)\right)\right)\right)\underset{\dot{}}{+}\left(\left(\left(\left(s+1\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}T\left(b\left(s\right)\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(0\right)\right)\right)\right)\right)\to I\underset{\dot{}}{\times }J\left(I\right)=\underset{i\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}G\left(i\right)\right)$$
23	22	ex	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left(s\in \mathbb{N}\wedge b\in \left(B^{\left(0\dots s\right)}\right)\right)\right)\to \left(I\underset{\dot{}}{\times }J\left(I\right)=\left(\underset{i=1}{\overset{s}{{\sum }_Y}},\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}\left(T\left(b\left(i-1\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(i\right)\right)\right)\right)\right)\right)\underset{\dot{}}{+}\left(\left(\left(\left(s+1\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}T\left(b\left(s\right)\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(0\right)\right)\right)\right)\to I\underset{\dot{}}{\times }J\left(I\right)=\underset{i\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}G\left(i\right)\right)\right)$$
24	23	reximdvva	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \left(\exists s\in \mathbb{N}\exists b\in \left(B^{\left(0\dots s\right)}\right)I\underset{\dot{}}{\times }J\left(I\right)=\left(\underset{i=1}{\overset{s}{{\sum }_Y}},\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}\left(T\left(b\left(i-1\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(i\right)\right)\right)\right)\right)\right)\underset{\dot{}}{+}\left(\left(\left(\left(s+1\right)\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}T\left(b\left(s\right)\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(0\right)\right)\right)\right)\to \exists s\in \mathbb{N}\exists b\in \left(B^{\left(0\dots s\right)}\right)I\underset{\dot{}}{\times }J\left(I\right)=\underset{i\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}G\left(i\right)\right)\right)$$
25	17 24	mpd	$$⊢\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)I\underset{\dot{}}{\times }J\left(I\right)=\underset{i\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(i\underset{\dot{}}{\times }X\right)\underset{\dot{}}{·}G\left(i\right)\right)$$