Theorem pmatcollpwscmat

Description: Write a scalar matrix over polynomials (over a commutative ring) as a sum of the product of variable powers and constant scalar matrices with scalar entries. (Contributed by AV, 2-Nov-2019) (Revised by AV, 4-Dec-2019)

	Ref	Expression
Hypotheses	pmatcollpwscmat.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	pmatcollpwscmat.c	$$⊢C=N\mathrm{Mat}P$$
	pmatcollpwscmat.b	$$⊢B={\mathrm{Base}}_C$$
	pmatcollpwscmat.m1	$$⊢\underset{\dot{}}{\ast }={\cdot }_C$$
	pmatcollpwscmat.e1	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
	pmatcollpwscmat.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	pmatcollpwscmat.t	$$⊢T=N\mathrm{matToPolyMat}R$$
	pmatcollpwscmat.a	$$⊢A=N\mathrm{Mat}R$$
	pmatcollpwscmat.d	$$⊢D={\mathrm{Base}}_A$$
	pmatcollpwscmat.u	$$⊢U=\mathrm{algSc}\left(P\right)$$
	pmatcollpwscmat.k	$$⊢K={\mathrm{Base}}_R$$
	pmatcollpwscmat.e2	$$⊢E={\mathrm{Base}}_P$$
	pmatcollpwscmat.s	$$⊢S=\mathrm{algSc}\left(P\right)$$
	pmatcollpwscmat.1	$$⊢\underset{\dot{}}{1}=1_C$$
	pmatcollpwscmat.m2	$$⊢M=Q\underset{\dot{}}{\ast }\underset{\dot{}}{1}$$
Assertion	pmatcollpwscmat	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge Q\in E\right)\to M=\underset{n\in {\mathbb{N}}_0}{{\sum }_C}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }\left(U\left({\mathrm{coe}}_1\left(Q\right)\left(n\right)\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		pmatcollpwscmat.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		pmatcollpwscmat.c	$$⊢C=N\mathrm{Mat}P$$
3		pmatcollpwscmat.b	$$⊢B={\mathrm{Base}}_C$$
4		pmatcollpwscmat.m1	$$⊢\underset{\dot{}}{\ast }={\cdot }_C$$
5		pmatcollpwscmat.e1	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
6		pmatcollpwscmat.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
7		pmatcollpwscmat.t	$$⊢T=N\mathrm{matToPolyMat}R$$
8		pmatcollpwscmat.a	$$⊢A=N\mathrm{Mat}R$$
9		pmatcollpwscmat.d	$$⊢D={\mathrm{Base}}_A$$
10		pmatcollpwscmat.u	$$⊢U=\mathrm{algSc}\left(P\right)$$
11		pmatcollpwscmat.k	$$⊢K={\mathrm{Base}}_R$$
12		pmatcollpwscmat.e2	$$⊢E={\mathrm{Base}}_P$$
13		pmatcollpwscmat.s	$$⊢S=\mathrm{algSc}\left(P\right)$$
14		pmatcollpwscmat.1	$$⊢\underset{\dot{}}{1}=1_C$$
15		pmatcollpwscmat.m2	$$⊢M=Q\underset{\dot{}}{\ast }\underset{\dot{}}{1}$$
16		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
17	1 2 3 12 4 14	1pmatscmul	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge Q\in E\right)\to Q\underset{\dot{}}{\ast }\underset{\dot{}}{1}\in B$$
18	15 17	eqeltrid	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge Q\in E\right)\to M\in B$$
19	16 18	syl3an2	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge Q\in E\right)\to M\in B$$
20	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)$$
21	19 20	syld3an3	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge Q\in E\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)$$
22	16	anim2i	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\right)\to \left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)$$
23	22	3adant3	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge Q\in E\right)\to \left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)$$
24		simp3	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge Q\in E\right)\to Q\in E$$
25	24	anim1ci	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge Q\in E\right)\wedge n\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0\wedge Q\in E\right)$$
26	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	pmatcollpwscmatlem2	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\wedge \left(n\in {\mathbb{N}}_0\wedge Q\in E\right)\right)\to T\left(M\mathrm{decompPMat}n\right)=U\left({\mathrm{coe}}_1\left(Q\right)\left(n\right)\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}$$
27	23 25 26	syl2an2r	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge Q\in E\right)\wedge n\in {\mathbb{N}}_0\right)\to T\left(M\mathrm{decompPMat}n\right)=U\left({\mathrm{coe}}_1\left(Q\right)\left(n\right)\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}$$
28	27	oveq2d	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge Q\in E\right)\wedge n\in {\mathbb{N}}_0\right)\to \left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(M\mathrm{decompPMat}n\right)=\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }\left(U\left({\mathrm{coe}}_1\left(Q\right)\left(n\right)\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)$$
29	28	mpteq2dva	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge Q\in E\right)\to \left(n\in {\mathbb{N}}_0⟼\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }T\left(M\mathrm{decompPMat}n\right)\right)=\left(n\in {\mathbb{N}}_0⟼\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }\left(U\left({\mathrm{coe}}_1\left(Q\right)\left(n\right)\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)\right)$$
30	29	oveq2d	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge Q\in E\right)\to \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)=\underset{n\in {\mathbb{N}}_0}{{\sum }_C}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }\left(U\left({\mathrm{coe}}_1\left(Q\right)\left(n\right)\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)\right)$$
31	21 30	eqtrd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge Q\in E\right)\to M=\underset{n\in {\mathbb{N}}_0}{{\sum }_C}\left(\left(n\underset{\dot{}}{\times }X\right)\underset{\dot{}}{\ast }\left(U\left({\mathrm{coe}}_1\left(Q\right)\left(n\right)\right)\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)\right)$$