Theorem chcoeffeq

Description: The coefficients of the characteristic polynomial multiplied with the identity matrix represented by (transformed) ring elements obtained from the adjunct of the characteristic matrix. (Contributed by AV, 21-Nov-2019) (Proof shortened by AV, 8-Dec-2019) (Revised by AV, 15-Dec-2019)

	Ref	Expression
Hypotheses	chcoeffeq.a	$$⊢A=N\mathrm{Mat}R$$
	chcoeffeq.b	$$⊢B={\mathrm{Base}}_A$$
	chcoeffeq.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	chcoeffeq.y	$$⊢Y=N\mathrm{Mat}P$$
	chcoeffeq.r	$$⊢\underset{\dot{}}{\times }={\cdot }_Y$$
	chcoeffeq.s	$$⊢\underset{\dot{}}{-}={-}_Y$$
	chcoeffeq.0	$$⊢\underset{\dot{}}{0}=0_Y$$
	chcoeffeq.t	$$⊢T=N\mathrm{matToPolyMat}R$$
	chcoeffeq.c	$$⊢C=N\mathrm{CharPlyMat}R$$
	chcoeffeq.k	$$⊢K=C\left(M\right)$$
	chcoeffeq.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)$$
	chcoeffeq.w	$$⊢W={\mathrm{Base}}_Y$$
	chcoeffeq.1	$$⊢\underset{\dot{}}{1}=1_A$$
	chcoeffeq.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_A$$
	chcoeffeq.u	$$⊢U=N\mathrm{cPolyMatToMat}R$$
Assertion	chcoeffeq	$$⊢\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)\forall n\in {\mathbb{N}}_{0}U\left(G\left(n\right)\right)={\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		chcoeffeq.a	$$⊢A=N\mathrm{Mat}R$$
2		chcoeffeq.b	$$⊢B={\mathrm{Base}}_A$$
3		chcoeffeq.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
4		chcoeffeq.y	$$⊢Y=N\mathrm{Mat}P$$
5		chcoeffeq.r	$$⊢\underset{\dot{}}{\times }={\cdot }_Y$$
6		chcoeffeq.s	$$⊢\underset{\dot{}}{-}={-}_Y$$
7		chcoeffeq.0	$$⊢\underset{\dot{}}{0}=0_Y$$
8		chcoeffeq.t	$$⊢T=N\mathrm{matToPolyMat}R$$
9		chcoeffeq.c	$$⊢C=N\mathrm{CharPlyMat}R$$
10		chcoeffeq.k	$$⊢K=C\left(M\right)$$
11		chcoeffeq.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)$$
12		chcoeffeq.w	$$⊢W={\mathrm{Base}}_Y$$
13		chcoeffeq.1	$$⊢\underset{\dot{}}{1}=1_A$$
14		chcoeffeq.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_A$$
15		chcoeffeq.u	$$⊢U=N\mathrm{cPolyMatToMat}R$$
16		eqid	$$⊢N\mathrm{ConstPolyMat}R=N\mathrm{ConstPolyMat}R$$
17		eqid	$$⊢{\cdot }_Y={\cdot }_Y$$
18		eqid	$$⊢1_Y=1_Y$$
19		eqid	$$⊢{\mathrm{var}}_1\left(R\right)={\mathrm{var}}_1\left(R\right)$$
20		eqid	$$⊢\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)=\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)$$
21		eqid	$$⊢N\mathrm{maAdju}P=N\mathrm{maAdju}P$$
22		eqid	$$⊢{\mathrm{Poly}}_1\left(A\right)={\mathrm{Poly}}_1\left(A\right)$$
23		eqid	$$⊢{\mathrm{var}}_1\left(A\right)={\mathrm{var}}_1\left(A\right)$$
24		eqid	$$⊢{\cdot }_{{\mathrm{Poly}}_1\left(A\right)}={\cdot }_{{\mathrm{Poly}}_1\left(A\right)}$$
25		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}$$
26		eqid	$$⊢N\mathrm{pMatToMatPoly}R=N\mathrm{pMatToMatPoly}R$$
27	1 2 3 4 8 5 6 7 11 16 17 18 19 20 21 12 22 23 24 25 15 26	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)\left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)$$
28		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_P}={\cdot }_{{\mathrm{mulGrp}}_P}$$
29		eqid	$$⊢\mathrm{algSc}\left(P\right)=\mathrm{algSc}\left(P\right)$$
30		eqid	$$⊢K{\cdot }_Y{1}_Y=K{\cdot }_Y{1}_Y$$
31	1 2 3 4 19 28 17 18 29 9 10 30 13 14 8 12 22 23 24 25 26	cpmidpmat	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \left(N\mathrm{pMatToMatPoly}R\right)\left(K{\cdot }_Y{1}_Y\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(\left({\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)$$
32		eqid	$$⊢N\mathrm{CharPlyMat}R=N\mathrm{CharPlyMat}R$$
33	1 2 32 3 4 19 8 6 17 18 20 21 5	cpmadurid	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)=\left(N\mathrm{CharPlyMat}R\right)\left(M\right){\cdot }_Y{1}_Y$$
34	9	fveq1i	$$⊢C\left(M\right)=\left(N\mathrm{CharPlyMat}R\right)\left(M\right)$$
35	10 34	eqtri	$$⊢K=\left(N\mathrm{CharPlyMat}R\right)\left(M\right)$$
36	35	a1i	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to K=\left(N\mathrm{CharPlyMat}R\right)\left(M\right)$$
37	36	eqcomd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \left(N\mathrm{CharPlyMat}R\right)\left(M\right)=K$$
38	37	oveq1d	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \left(N\mathrm{CharPlyMat}R\right)\left(M\right){\cdot }_Y{1}_Y=K{\cdot }_Y{1}_Y$$
39	33 38	eqtrd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)=K{\cdot }_Y{1}_Y$$
40		fveq2	$$⊢\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)=K{\cdot }_Y{1}_Y\to \left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\left(N\mathrm{pMatToMatPoly}R\right)\left(K{\cdot }_Y{1}_Y\right)$$
41		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 \left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\right)\to \left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)$$
42	41	adantr	$$⊢\left(\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 \left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\right)\wedge \left(N\mathrm{pMatToMatPoly}R\right)\left(K{\cdot }_Y{1}_Y\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(\left({\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\right)\to \left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)$$
43		simpr	$$⊢\left(\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 \left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\right)\wedge \left(N\mathrm{pMatToMatPoly}R\right)\left(K{\cdot }_Y{1}_Y\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(\left({\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\right)\to \left(N\mathrm{pMatToMatPoly}R\right)\left(K{\cdot }_Y{1}_Y\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(\left({\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)$$
44	42 43	eqeq12d	$$⊢\left(\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 \left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\right)\wedge \left(N\mathrm{pMatToMatPoly}R\right)\left(K{\cdot }_Y{1}_Y\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(\left({\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\right)\to \left(\left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\left(N\mathrm{pMatToMatPoly}R\right)\left(K{\cdot }_Y{1}_Y\right)\leftrightarrow \underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(\left({\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\right)$$
45	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	chcoeffeqlem	$$⊢\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{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(\left({\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\to \forall n\in {\mathbb{N}}_{0}U\left(G\left(n\right)\right)={\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)$$
46	45	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 \left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\right)\to \left(\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(\left({\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\to \forall n\in {\mathbb{N}}_{0}U\left(G\left(n\right)\right)={\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)$$
47	46	adantr	$$⊢\left(\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 \left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\right)\wedge \left(N\mathrm{pMatToMatPoly}R\right)\left(K{\cdot }_Y{1}_Y\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(\left({\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\right)\to \left(\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(\left({\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\to \forall n\in {\mathbb{N}}_{0}U\left(G\left(n\right)\right)={\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)$$
48	44 47	sylbid	$$⊢\left(\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 \left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\right)\wedge \left(N\mathrm{pMatToMatPoly}R\right)\left(K{\cdot }_Y{1}_Y\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(\left({\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\right)\to \left(\left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\left(N\mathrm{pMatToMatPoly}R\right)\left(K{\cdot }_Y{1}_Y\right)\to \forall n\in {\mathbb{N}}_{0}U\left(G\left(n\right)\right)={\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)$$
49	48	exp31	$$⊢\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(\left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\to \left(\left(N\mathrm{pMatToMatPoly}R\right)\left(K{\cdot }_Y{1}_Y\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(\left({\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\to \left(\left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\left(N\mathrm{pMatToMatPoly}R\right)\left(K{\cdot }_Y{1}_Y\right)\to \forall n\in {\mathbb{N}}_{0}U\left(G\left(n\right)\right)={\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)\right)\right)$$
50	49	com24	$$⊢\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(\left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\left(N\mathrm{pMatToMatPoly}R\right)\left(K{\cdot }_Y{1}_Y\right)\to \left(\left(N\mathrm{pMatToMatPoly}R\right)\left(K{\cdot }_Y{1}_Y\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(\left({\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\to \left(\left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\to \forall n\in {\mathbb{N}}_{0}U\left(G\left(n\right)\right)={\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)\right)\right)$$
51	40 50	syl5	$$⊢\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(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)=K{\cdot }_Y{1}_Y\to \left(\left(N\mathrm{pMatToMatPoly}R\right)\left(K{\cdot }_Y{1}_Y\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(\left({\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\to \left(\left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\to \forall n\in {\mathbb{N}}_{0}U\left(G\left(n\right)\right)={\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)\right)\right)$$
52	51	ex	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \left(\left(s\in \mathbb{N}\wedge b\in \left(B^{\left(0\dots s\right)}\right)\right)\to \left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)=K{\cdot }_Y{1}_Y\to \left(\left(N\mathrm{pMatToMatPoly}R\right)\left(K{\cdot }_Y{1}_Y\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(\left({\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\to \left(\left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\to \forall n\in {\mathbb{N}}_{0}U\left(G\left(n\right)\right)={\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)\right)\right)\right)$$
53	52	com24	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \left(\left(N\mathrm{pMatToMatPoly}R\right)\left(K{\cdot }_Y{1}_Y\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(\left({\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\to \left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)=K{\cdot }_Y{1}_Y\to \left(\left(s\in \mathbb{N}\wedge b\in \left(B^{\left(0\dots s\right)}\right)\right)\to \left(\left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\to \forall n\in {\mathbb{N}}_{0}U\left(G\left(n\right)\right)={\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)\right)\right)\right)$$
54	31 39 53	mp2d	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \left(\left(s\in \mathbb{N}\wedge b\in \left(B^{\left(0\dots s\right)}\right)\right)\to \left(\left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\to \forall n\in {\mathbb{N}}_{0}U\left(G\left(n\right)\right)={\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)\right)$$
55	54	impl	$$⊢\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(\left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\to \forall n\in {\mathbb{N}}_{0}U\left(G\left(n\right)\right)={\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)$$
56	55	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)\left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\to \exists b\in \left(B^{\left(0\dots s\right)}\right)\forall n\in {\mathbb{N}}_{0}U\left(G\left(n\right)\right)={\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)$$
57	56	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)\left(N\mathrm{pMatToMatPoly}R\right)\left(\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\underset{\dot{}}{\times }\left(N\mathrm{maAdju}P\right)\left(\left({\mathrm{var}}_1\left(R\right){\cdot }_Y{1}_Y\right)\underset{\dot{}}{-}T\left(M\right)\right)\right)=\underset{n\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(A\right)}}\left(U\left(G\left(n\right)\right){\cdot }_{{\mathrm{Poly}}_1\left(A\right)}\left(n{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(A\right)}}{\mathrm{var}}_1\left(A\right)\right)\right)\to \exists s\in \mathbb{N}\exists b\in \left(B^{\left(0\dots s\right)}\right)\forall n\in {\mathbb{N}}_{0}U\left(G\left(n\right)\right)={\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)$$
58	27 57	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)\forall n\in {\mathbb{N}}_{0}U\left(G\left(n\right)\right)={\mathrm{coe}}_1\left(K\right)\left(n\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}$$