Theorem pmatcollpw3fi

Description: Write a polynomial matrix (over a commutative ring) as a finite sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 4-Nov-2019) (Revised by AV, 4-Dec-2019) (Proof shortened by AV, 8-Dec-2019)

	Ref	Expression
Hypotheses	pmatcollpw.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	pmatcollpw.c	$$⊢C=N\mathrm{Mat}P$$
	pmatcollpw.b	$$⊢B={\mathrm{Base}}_C$$
	pmatcollpw.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_C$$
	pmatcollpw.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
	pmatcollpw.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	pmatcollpw.t	$$⊢T=N\mathrm{matToPolyMat}R$$
	pmatcollpw3.a	$$⊢A=N\mathrm{Mat}R$$
	pmatcollpw3.d	$$⊢D={\mathrm{Base}}_A$$
Assertion	pmatcollpw3fi	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \exists s\in {\mathbb{N}}_0\exists f\in \left(D^{\left(0\dots s\right)}\right)M=\underset{n=0}{\overset{s}{{\sum }_C}}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(f\left(n\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		pmatcollpw.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		pmatcollpw.c	$$⊢C=N\mathrm{Mat}P$$
3		pmatcollpw.b	$$⊢B={\mathrm{Base}}_C$$
4		pmatcollpw.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_C$$
5		pmatcollpw.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
6		pmatcollpw.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
7		pmatcollpw.t	$$⊢T=N\mathrm{matToPolyMat}R$$
8		pmatcollpw3.a	$$⊢A=N\mathrm{Mat}R$$
9		pmatcollpw3.d	$$⊢D={\mathrm{Base}}_A$$
10	1 2 3 4 5 6 7	pmatcollpwfi	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \exists s\in {\mathbb{N}}_{0}M=\underset{n=0}{\overset{s}{{\sum }_C}}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(M\mathrm{decompPMat}n\right)\right)$$
11		elnn0uz	$$⊢s\in {\mathbb{N}}_0\leftrightarrow s\in {\mathbb{Z}}_{\ge 0}$$
12		fzn0	$$⊢\left(0\dots s\right)\ne \varnothing \leftrightarrow s\in {\mathbb{Z}}_{\ge 0}$$
13	11 12	sylbb2	$$⊢s\in {\mathbb{N}}_0\to \left(0\dots s\right)\ne \varnothing$$
14		fz0ssnn0	$$⊢\left(0\dots s\right)\subseteq {\mathbb{N}}_0$$
15	13 14	jctil	$$⊢s\in {\mathbb{N}}_0\to \left(\left(0\dots s\right)\subseteq {\mathbb{N}}_0\wedge \left(0\dots s\right)\ne \varnothing \right)$$
16	1 2 3 4 5 6 7 8 9	pmatcollpw3lem	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\wedge \left(\left(0\dots s\right)\subseteq {\mathbb{N}}_0\wedge \left(0\dots s\right)\ne \varnothing \right)\right)\to \left(M=\underset{n=0}{\overset{s}{{\sum }_C}}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(M\mathrm{decompPMat}n\right)\right)\to \exists f\in \left(D^{\left(0\dots s\right)}\right)M=\underset{n=0}{\overset{s}{{\sum }_C}}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(f\left(n\right)\right)\right)\right)$$
17	15 16	sylan2	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\wedge s\in {\mathbb{N}}_0\right)\to \left(M=\underset{n=0}{\overset{s}{{\sum }_C}}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(M\mathrm{decompPMat}n\right)\right)\to \exists f\in \left(D^{\left(0\dots s\right)}\right)M=\underset{n=0}{\overset{s}{{\sum }_C}}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(f\left(n\right)\right)\right)\right)$$
18	17	reximdva	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \left(\exists s\in {\mathbb{N}}_{0}M=\underset{n=0}{\overset{s}{{\sum }_C}}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(M\mathrm{decompPMat}n\right)\right)\to \exists s\in {\mathbb{N}}_0\exists f\in \left(D^{\left(0\dots s\right)}\right)M=\underset{n=0}{\overset{s}{{\sum }_C}}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(f\left(n\right)\right)\right)\right)$$
19	10 18	mpd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \exists s\in {\mathbb{N}}_0\exists f\in \left(D^{\left(0\dots s\right)}\right)M=\underset{n=0}{\overset{s}{{\sum }_C}}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(f\left(n\right)\right)\right)$$