Theorem pmatcollpw3fi1

Description: Write a polynomial matrix (over a commutative ring) as a finite sum of (at least two) products of variable powers and constant matrices with scalar entries. (Contributed by AV, 6-Nov-2019) (Revised by AV, 4-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	pmatcollpw3fi1	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \exists s\in \mathbb{N}\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 8 9	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)$$
11		df-n0	$$⊢{\mathbb{N}}_0=\mathbb{N}\cup \left\{0\right\}$$
12	11	rexeqi	$$⊢\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)\leftrightarrow \exists s\in \left(\mathbb{N}\cup \left\{0\right\}\right)\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)$$
13		rexun	$$⊢\exists s\in \left(\mathbb{N}\cup \left\{0\right\}\right)\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)\leftrightarrow \left(\exists s\in \mathbb{N}\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)\vee \exists s\in \left\{0\right\}\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)$$
14	12 13	bitri	$$⊢\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)\leftrightarrow \left(\exists s\in \mathbb{N}\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)\vee \exists s\in \left\{0\right\}\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)$$
15		c0ex	$$⊢0\in \mathrm{V}$$
16		oveq2	$$⊢s=0\to \left(0\dots s\right)=\left(0\dots 0\right)$$
17		0z	$$⊢0\in \mathbb{Z}$$
18		fzsn	$$⊢0\in \mathbb{Z}\to \left(0\dots 0\right)=\left\{0\right\}$$
19	17 18	mp1i	$$⊢s=0\to \left(0\dots 0\right)=\left\{0\right\}$$
20	16 19	eqtrd	$$⊢s=0\to \left(0\dots s\right)=\left\{0\right\}$$
21	20	oveq2d	$$⊢s=0\to D^{\left(0\dots s\right)}=D^{\left\{0\right\}}$$
22	20	mpteq1d	$$⊢s=0\to \left(n\in \left(0\dots s\right)⟼\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(f\left(n\right)\right)\right)=\left(n\in \left\{0\right\}⟼\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(f\left(n\right)\right)\right)$$
23	22	oveq2d	$$⊢s=0\to \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)=\underset{n\in \left\{0\right\}}{{\sum }_C}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(f\left(n\right)\right)\right)$$
24	23	eqeq2d	$$⊢s=0\to \left(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)\leftrightarrow M=\underset{n\in \left\{0\right\}}{{\sum }_C}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(f\left(n\right)\right)\right)\right)$$
25	21 24	rexeqbidv	$$⊢s=0\to \left(\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)\leftrightarrow \exists f\in \left(D^{\left\{0\right\}}\right)M=\underset{n\in \left\{0\right\}}{{\sum }_C}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(f\left(n\right)\right)\right)\right)$$
26	15 25	rexsn	$$⊢\exists s\in \left\{0\right\}\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)\leftrightarrow \exists f\in \left(D^{\left\{0\right\}}\right)M=\underset{n\in \left\{0\right\}}{{\sum }_C}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(f\left(n\right)\right)\right)$$
27	1 2 3 4 5 6 7 8 9	pmatcollpw3fi1lem2	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \left(\exists f\in \left(D^{\left\{0\right\}}\right)M=\underset{n\in \left\{0\right\}}{{\sum }_C}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(f\left(n\right)\right)\right)\to \exists s\in \mathbb{N}\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)$$
28	27	com12	$$⊢\exists f\in \left(D^{\left\{0\right\}}\right)M=\underset{n\in \left\{0\right\}}{{\sum }_C}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(f\left(n\right)\right)\right)\to \left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \exists s\in \mathbb{N}\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)$$
29	26 28	sylbi	$$⊢\exists s\in \left\{0\right\}\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)\to \left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \exists s\in \mathbb{N}\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)$$
30	29	jao1i	$$⊢\left(\exists s\in \mathbb{N}\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)\vee \exists s\in \left\{0\right\}\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)\to \left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \exists s\in \mathbb{N}\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)$$
31	14 30	sylbi	$$⊢\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)\to \left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \exists s\in \mathbb{N}\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)$$
32	10 31	mpcom	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \exists s\in \mathbb{N}\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)$$