Theorem pmatcollpw3

Description: Write a polynomial matrix (over a commutative ring) as a sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 27-Oct-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	pmatcollpw3	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \exists f\in \left(D^{{\mathbb{N}}_0}\right)M=\underset{n\in {\mathbb{N}}_0}{{\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	pmatcollpw	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to M=\underset{n\in {\mathbb{N}}_0}{{\sum }_C}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(M\mathrm{decompPMat}n\right)\right)$$
11		ssid	$$⊢{\mathbb{N}}_0\subseteq {\mathbb{N}}_0$$
12		0nn0	$$⊢0\in {\mathbb{N}}_0$$
13	12	ne0ii	$$⊢{\mathbb{N}}_0\ne \varnothing$$
14	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({\mathbb{N}}_0\subseteq {\mathbb{N}}_0\wedge {\mathbb{N}}_0\ne \varnothing \right)\right)\to \left(M=\underset{n\in {\mathbb{N}}_0}{{\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^{{\mathbb{N}}_0}\right)M=\underset{n\in {\mathbb{N}}_0}{{\sum }_C}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(f\left(n\right)\right)\right)\right)$$
15	11 13 14	mpanr12	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \left(M=\underset{n\in {\mathbb{N}}_0}{{\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^{{\mathbb{N}}_0}\right)M=\underset{n\in {\mathbb{N}}_0}{{\sum }_C}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(f\left(n\right)\right)\right)\right)$$
16	10 15	mpd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \exists f\in \left(D^{{\mathbb{N}}_0}\right)M=\underset{n\in {\mathbb{N}}_0}{{\sum }_C}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(f\left(n\right)\right)\right)$$