Theorem cpmadumatpolylem1

Description: Lemma 1 for cpmadumatpoly . (Contributed by AV, 20-Nov-2019) (Revised by AV, 15-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$$
Assertion	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)$$

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		simp1	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to N\in \mathrm{Fin}$$
23		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
24	23	3ad2ant2	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to R\in \mathrm{Ring}$$
25	22 24	jca	$$⊢\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{Ring}\right)$$
26	25	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{Ring}\right)$$
27	1 2 10 21	cpm2mf	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to U:S⟶B$$
28	26 27	syl	$$⊢\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:S⟶B$$
29	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$$
30	23 29	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$$
31	30	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$$
32		fco	$$⊢\left(U:S⟶B\wedge G:{\mathbb{N}}_0⟶S\right)\to \left(U\circ G\right):{\mathbb{N}}_0⟶B$$
33	28 31 32	syl2anc	$$⊢\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(U\circ G\right):{\mathbb{N}}_0⟶B$$
34	2	fvexi	$$⊢B\in \mathrm{V}$$
35		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
36	34 35	pm3.2i	$$⊢\left(B\in \mathrm{V}\wedge {\mathbb{N}}_0\in \mathrm{V}\right)$$
37		elmapg	$$⊢\left(B\in \mathrm{V}\wedge {\mathbb{N}}_0\in \mathrm{V}\right)\to \left(U\circ G\in \left(B^{{\mathbb{N}}_0}\right)\leftrightarrow \left(U\circ G\right):{\mathbb{N}}_0⟶B\right)$$
38	36 37	mp1i	$$⊢\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(U\circ G\in \left(B^{{\mathbb{N}}_0}\right)\leftrightarrow \left(U\circ G\right):{\mathbb{N}}_0⟶B\right)$$
39	33 38	mpbird	$$⊢\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)$$