Theorem cpmadumatpoly

Description: The product of the characteristic matrix of a given matrix and its adjunct represented as a polynomial over matrices. (Contributed by AV, 20-Nov-2019) (Revised by AV, 7-Dec-2019)

	Ref	Expression
Hypotheses	cpmadumatpoly.a	$$⊢A=N\mathrm{Mat}R$$
	cpmadumatpoly.b	$$⊢B={\mathrm{Base}}_A$$
	cpmadumatpoly.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	cpmadumatpoly.y	$$⊢Y=N\mathrm{Mat}P$$
	cpmadumatpoly.t	$$⊢T=N\mathrm{matToPolyMat}R$$
	cpmadumatpoly.r	$$⊢\underset{\dot{}}{\times }={\cdot }_Y$$
	cpmadumatpoly.m0	$$⊢\underset{\dot{}}{-}={-}_Y$$
	cpmadumatpoly.0	$$⊢\underset{\dot{}}{0}=0_Y$$
	cpmadumatpoly.g	$$⊢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)$$
	cpmadumatpoly.s	$$⊢S=N\mathrm{ConstPolyMat}R$$
	cpmadumatpoly.m1	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
	cpmadumatpoly.1	$$⊢\underset{\dot{}}{1}=1_Y$$
	cpmadumatpoly.z	$$⊢Z={\mathrm{var}}_1\left(R\right)$$
	cpmadumatpoly.d	$$⊢D=\left(Z\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(M\right)$$
	cpmadumatpoly.j	$$⊢J=N\mathrm{maAdju}P$$
	cpmadumatpoly.w	$$⊢W={\mathrm{Base}}_Y$$
	cpmadumatpoly.q	$$⊢Q={\mathrm{Poly}}_1\left(A\right)$$
	cpmadumatpoly.x	$$⊢X={\mathrm{var}}_1\left(A\right)$$
	cpmadumatpoly.m2	$$⊢\underset{\dot{}}{\ast }={\cdot }_Q$$
	cpmadumatpoly.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_Q}$$
	cpmadumatpoly.u	$$⊢U=N\mathrm{cPolyMatToMat}R$$
	cpmadumatpoly.i	$$⊢I=N\mathrm{pMatToMatPoly}R$$
Assertion	cpmadumatpoly	$$⊢\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\left(D\underset{\dot{}}{\times }J\left(D\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Q}\left(U\left(G\left(n\right)\right)\underset{\dot{}}{\ast }\left(n\underset{\dot{}}{\times }X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cpmadumatpoly.a	$$⊢A=N\mathrm{Mat}R$$
2		cpmadumatpoly.b	$$⊢B={\mathrm{Base}}_A$$
3		cpmadumatpoly.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
4		cpmadumatpoly.y	$$⊢Y=N\mathrm{Mat}P$$
5		cpmadumatpoly.t	$$⊢T=N\mathrm{matToPolyMat}R$$
6		cpmadumatpoly.r	$$⊢\underset{\dot{}}{\times }={\cdot }_Y$$
7		cpmadumatpoly.m0	$$⊢\underset{\dot{}}{-}={-}_Y$$
8		cpmadumatpoly.0	$$⊢\underset{\dot{}}{0}=0_Y$$
9		cpmadumatpoly.g	$$⊢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)$$
10		cpmadumatpoly.s	$$⊢S=N\mathrm{ConstPolyMat}R$$
11		cpmadumatpoly.m1	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
12		cpmadumatpoly.1	$$⊢\underset{\dot{}}{1}=1_Y$$
13		cpmadumatpoly.z	$$⊢Z={\mathrm{var}}_1\left(R\right)$$
14		cpmadumatpoly.d	$$⊢D=\left(Z\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{-}T\left(M\right)$$
15		cpmadumatpoly.j	$$⊢J=N\mathrm{maAdju}P$$
16		cpmadumatpoly.w	$$⊢W={\mathrm{Base}}_Y$$
17		cpmadumatpoly.q	$$⊢Q={\mathrm{Poly}}_1\left(A\right)$$
18		cpmadumatpoly.x	$$⊢X={\mathrm{var}}_1\left(A\right)$$
19		cpmadumatpoly.m2	$$⊢\underset{\dot{}}{\ast }={\cdot }_Q$$
20		cpmadumatpoly.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_Q}$$
21		cpmadumatpoly.u	$$⊢U=N\mathrm{cPolyMatToMat}R$$
22		cpmadumatpoly.i	$$⊢I=N\mathrm{pMatToMatPoly}R$$
23		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_P}={\cdot }_{{\mathrm{mulGrp}}_P}$$
24		eqid	$$⊢{+}_Y={+}_Y$$
25		eqeq1	$$⊢n=z\to \left(n=0\leftrightarrow z=0\right)$$
26		eqeq1	$$⊢n=z\to \left(n=s+1\leftrightarrow z=s+1\right)$$
27		breq2	$$⊢n=z\to \left(s+1<n\leftrightarrow s+1<z\right)$$
28		fvoveq1	$$⊢n=z\to b\left(n-1\right)=b\left(z-1\right)$$
29	28	fveq2d	$$⊢n=z\to T\left(b\left(n-1\right)\right)=T\left(b\left(z-1\right)\right)$$
30		2fveq3	$$⊢n=z\to T\left(b\left(n\right)\right)=T\left(b\left(z\right)\right)$$
31	30	oveq2d	$$⊢n=z\to T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(n\right)\right)=T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(z\right)\right)$$
32	29 31	oveq12d	$$⊢n=z\to 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)=T\left(b\left(z-1\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(z\right)\right)\right)$$
33	27 32	ifbieq2d	$$⊢n=z\to 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)=if\left(s+1<z,\underset{\dot{}}{0},T\left(b\left(z-1\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(z\right)\right)\right)\right)$$
34	26 33	ifbieq2d	$$⊢n=z\to 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)=if\left(z=s+1,T\left(b\left(s\right)\right),if\left(s+1<z,\underset{\dot{}}{0},T\left(b\left(z-1\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(z\right)\right)\right)\right)\right)$$
35	25 34	ifbieq2d	$$⊢n=z\to 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)=if\left(z=0,\underset{\dot{}}{0}\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(0\right)\right)\right),if\left(z=s+1,T\left(b\left(s\right)\right),if\left(s+1<z,\underset{\dot{}}{0},T\left(b\left(z-1\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(z\right)\right)\right)\right)\right)\right)$$
36	35	cbvmptv	$$⊢\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)=\left(z\in {\mathbb{N}}_0⟼if\left(z=0,\underset{\dot{}}{0}\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(0\right)\right)\right),if\left(z=s+1,T\left(b\left(s\right)\right),if\left(s+1<z,\underset{\dot{}}{0},T\left(b\left(z-1\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(z\right)\right)\right)\right)\right)\right)\right)$$
37	9 36	eqtri	$$⊢G=\left(z\in {\mathbb{N}}_0⟼if\left(z=0,\underset{\dot{}}{0}\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(0\right)\right)\right),if\left(z=s+1,T\left(b\left(s\right)\right),if\left(s+1<z,\underset{\dot{}}{0},T\left(b\left(z-1\right)\right)\underset{\dot{}}{-}\left(T\left(M\right)\underset{\dot{}}{\times }T\left(b\left(z\right)\right)\right)\right)\right)\right)\right)$$
38	1 2 3 4 5 13 23 11 6 12 24 7 14 15 8 37	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)D\underset{\dot{}}{\times }J\left(D\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}G\left(n\right)\right)$$
39		simp1	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to N\in \mathrm{Fin}$$
40	39	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 n\in {\mathbb{N}}_0\right)\to N\in \mathrm{Fin}$$
41		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
42	41	3ad2ant2	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to R\in \mathrm{Ring}$$
43	42	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 n\in {\mathbb{N}}_0\right)\to R\in \mathrm{Ring}$$
44	1 2 3 4 6 7 8 5 9 10	chfacfisfcpmat	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\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 G:{\mathbb{N}}_0⟶S$$
45	41 44	syl3anl2	$$⊢\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 G:{\mathbb{N}}_0⟶S$$
46	45	anassrs	$$⊢\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)\to G:{\mathbb{N}}_0⟶S$$
47	46	ffvelrnda	$$⊢\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 n\in {\mathbb{N}}_0\right)\to G\left(n\right)\in S$$
48	10 21 5	m2cpminvid2	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge G\left(n\right)\in S\right)\to T\left(U\left(G\left(n\right)\right)\right)=G\left(n\right)$$
49	40 43 47 48	syl3anc	$$⊢\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 n\in {\mathbb{N}}_0\right)\to T\left(U\left(G\left(n\right)\right)\right)=G\left(n\right)$$
50	49	eqcomd	$$⊢\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 n\in {\mathbb{N}}_0\right)\to G\left(n\right)=T\left(U\left(G\left(n\right)\right)\right)$$
51	50	oveq2d	$$⊢\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 n\in {\mathbb{N}}_0\right)\to \left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}G\left(n\right)=\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}T\left(U\left(G\left(n\right)\right)\right)$$
52	51	mpteq2dva	$$⊢\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)\to \left(n\in {\mathbb{N}}_0⟼\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}G\left(n\right)\right)=\left(n\in {\mathbb{N}}_0⟼\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}T\left(U\left(G\left(n\right)\right)\right)\right)$$
53	52	oveq2d	$$⊢\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)\to \underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}G\left(n\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}T\left(U\left(G\left(n\right)\right)\right)\right)$$
54	53	eqeq2d	$$⊢\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)\to \left(D\underset{\dot{}}{\times }J\left(D\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}G\left(n\right)\right)\leftrightarrow D\underset{\dot{}}{\times }J\left(D\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}T\left(U\left(G\left(n\right)\right)\right)\right)\right)$$
55		fveq2	$$⊢D\underset{\dot{}}{\times }J\left(D\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}T\left(U\left(G\left(n\right)\right)\right)\right)\to I\left(D\underset{\dot{}}{\times }J\left(D\right)\right)=I\left(\underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}T\left(U\left(G\left(n\right)\right)\right)\right)\right)$$
56		3simpa	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\right)$$
57	56	ad2antrr	$$⊢\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)\to \left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\right)$$
58	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21	cpmadumatpolylem1	$$⊢\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)\to U\circ G\in \left(B^{{\mathbb{N}}_0}\right)$$
59	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21	cpmadumatpolylem2	$$⊢\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)\to {finSupp}_{0_A}\left(\left(U\circ G\right)\right)$$
60	3 4 16 19 20 18 1 2 17 22 23 13 11 5	pm2mp	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\right)\wedge \left(U\circ G\in \left(B^{{\mathbb{N}}_0}\right)\wedge {finSupp}_{0_A}\left(\left(U\circ G\right)\right)\right)\right)\to I\left(\underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}T\left(\left(U\circ G\right)\left(n\right)\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Q}\left(\left(U\circ G\right)\left(n\right)\underset{\dot{}}{\ast }\left(n\underset{\dot{}}{\times }X\right)\right)$$
61	57 58 59 60	syl12anc	$$⊢\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)\to I\left(\underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}T\left(\left(U\circ G\right)\left(n\right)\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Q}\left(\left(U\circ G\right)\left(n\right)\underset{\dot{}}{\ast }\left(n\underset{\dot{}}{\times }X\right)\right)$$
62		fvco3	$$⊢\left(G:{\mathbb{N}}_0⟶S\wedge n\in {\mathbb{N}}_0\right)\to \left(U\circ G\right)\left(n\right)=U\left(G\left(n\right)\right)$$
63	62	eqcomd	$$⊢\left(G:{\mathbb{N}}_0⟶S\wedge n\in {\mathbb{N}}_0\right)\to U\left(G\left(n\right)\right)=\left(U\circ G\right)\left(n\right)$$
64	46 63	sylan	$$⊢\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 n\in {\mathbb{N}}_0\right)\to U\left(G\left(n\right)\right)=\left(U\circ G\right)\left(n\right)$$
65	64	fveq2d	$$⊢\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 n\in {\mathbb{N}}_0\right)\to T\left(U\left(G\left(n\right)\right)\right)=T\left(\left(U\circ G\right)\left(n\right)\right)$$
66	65	oveq2d	$$⊢\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 n\in {\mathbb{N}}_0\right)\to \left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}T\left(U\left(G\left(n\right)\right)\right)=\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}T\left(\left(U\circ G\right)\left(n\right)\right)$$
67	66	mpteq2dva	$$⊢\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)\to \left(n\in {\mathbb{N}}_0⟼\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}T\left(U\left(G\left(n\right)\right)\right)\right)=\left(n\in {\mathbb{N}}_0⟼\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}T\left(\left(U\circ G\right)\left(n\right)\right)\right)$$
68	67	oveq2d	$$⊢\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)\to \underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}T\left(U\left(G\left(n\right)\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}T\left(\left(U\circ G\right)\left(n\right)\right)\right)$$
69	68	fveq2d	$$⊢\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)\to I\left(\underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}T\left(U\left(G\left(n\right)\right)\right)\right)\right)=I\left(\underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}T\left(\left(U\circ G\right)\left(n\right)\right)\right)\right)$$
70	64	oveq1d	$$⊢\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 n\in {\mathbb{N}}_0\right)\to U\left(G\left(n\right)\right)\underset{\dot{}}{\ast }\left(n\underset{\dot{}}{\times }X\right)=\left(U\circ G\right)\left(n\right)\underset{\dot{}}{\ast }\left(n\underset{\dot{}}{\times }X\right)$$
71	70	mpteq2dva	$$⊢\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)\to \left(n\in {\mathbb{N}}_0⟼U\left(G\left(n\right)\right)\underset{\dot{}}{\ast }\left(n\underset{\dot{}}{\times }X\right)\right)=\left(n\in {\mathbb{N}}_0⟼\left(U\circ G\right)\left(n\right)\underset{\dot{}}{\ast }\left(n\underset{\dot{}}{\times }X\right)\right)$$
72	71	oveq2d	$$⊢\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)\to \underset{n\in {\mathbb{N}}_0}{{\sum }_Q}\left(U\left(G\left(n\right)\right)\underset{\dot{}}{\ast }\left(n\underset{\dot{}}{\times }X\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Q}\left(\left(U\circ G\right)\left(n\right)\underset{\dot{}}{\ast }\left(n\underset{\dot{}}{\times }X\right)\right)$$
73	61 69 72	3eqtr4d	$$⊢\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)\to I\left(\underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}T\left(U\left(G\left(n\right)\right)\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Q}\left(U\left(G\left(n\right)\right)\underset{\dot{}}{\ast }\left(n\underset{\dot{}}{\times }X\right)\right)$$
74	55 73	sylan9eqr	$$⊢\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 D\underset{\dot{}}{\times }J\left(D\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}T\left(U\left(G\left(n\right)\right)\right)\right)\right)\to I\left(D\underset{\dot{}}{\times }J\left(D\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Q}\left(U\left(G\left(n\right)\right)\underset{\dot{}}{\ast }\left(n\underset{\dot{}}{\times }X\right)\right)$$
75	74	ex	$$⊢\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)\to \left(D\underset{\dot{}}{\times }J\left(D\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}T\left(U\left(G\left(n\right)\right)\right)\right)\to I\left(D\underset{\dot{}}{\times }J\left(D\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Q}\left(U\left(G\left(n\right)\right)\underset{\dot{}}{\ast }\left(n\underset{\dot{}}{\times }X\right)\right)\right)$$
76	54 75	sylbid	$$⊢\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)\to \left(D\underset{\dot{}}{\times }J\left(D\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}G\left(n\right)\right)\to I\left(D\underset{\dot{}}{\times }J\left(D\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Q}\left(U\left(G\left(n\right)\right)\underset{\dot{}}{\ast }\left(n\underset{\dot{}}{\times }X\right)\right)\right)$$
77	76	reximdva	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\wedge s\in \mathbb{N}\right)\to \left(\exists b\in \left(B^{\left(0\dots s\right)}\right)D\underset{\dot{}}{\times }J\left(D\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}G\left(n\right)\right)\to \exists b\in \left(B^{\left(0\dots s\right)}\right)I\left(D\underset{\dot{}}{\times }J\left(D\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Q}\left(U\left(G\left(n\right)\right)\underset{\dot{}}{\ast }\left(n\underset{\dot{}}{\times }X\right)\right)\right)$$
78	77	reximdva	$$⊢\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)D\underset{\dot{}}{\times }J\left(D\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Y}\left(\left(n{\cdot }_{{\mathrm{mulGrp}}_P}Z\right)\underset{\dot{}}{·}G\left(n\right)\right)\to \exists s\in \mathbb{N}\exists b\in \left(B^{\left(0\dots s\right)}\right)I\left(D\underset{\dot{}}{\times }J\left(D\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Q}\left(U\left(G\left(n\right)\right)\underset{\dot{}}{\ast }\left(n\underset{\dot{}}{\times }X\right)\right)\right)$$
79	38 78	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\left(D\underset{\dot{}}{\times }J\left(D\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_Q}\left(U\left(G\left(n\right)\right)\underset{\dot{}}{\ast }\left(n\underset{\dot{}}{\times }X\right)\right)$$