Theorem pm2mpf

Description: The transformation of polynomial matrices into polynomials over matrices is a function mapping polynomial matrices to polynomials over matrices. (Contributed by AV, 5-Oct-2019) (Revised by AV, 5-Dec-2019)

	Ref	Expression
Hypotheses	pm2mpval.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	pm2mpval.c	$$⊢C=N\mathrm{Mat}P$$
	pm2mpval.b	$$⊢B={\mathrm{Base}}_C$$
	pm2mpval.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_Q$$
	pm2mpval.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_Q}$$
	pm2mpval.x	$$⊢X={\mathrm{var}}_1\left(A\right)$$
	pm2mpval.a	$$⊢A=N\mathrm{Mat}R$$
	pm2mpval.q	$$⊢Q={\mathrm{Poly}}_1\left(A\right)$$
	pm2mpval.t	$$⊢T=N\mathrm{pMatToMatPoly}R$$
	pm2mpcl.l	$$⊢L={\mathrm{Base}}_Q$$
Assertion	pm2mpf	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T:B⟶L$$

Proof

Step	Hyp	Ref	Expression
1		pm2mpval.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		pm2mpval.c	$$⊢C=N\mathrm{Mat}P$$
3		pm2mpval.b	$$⊢B={\mathrm{Base}}_C$$
4		pm2mpval.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_Q$$
5		pm2mpval.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_Q}$$
6		pm2mpval.x	$$⊢X={\mathrm{var}}_1\left(A\right)$$
7		pm2mpval.a	$$⊢A=N\mathrm{Mat}R$$
8		pm2mpval.q	$$⊢Q={\mathrm{Poly}}_1\left(A\right)$$
9		pm2mpval.t	$$⊢T=N\mathrm{pMatToMatPoly}R$$
10		pm2mpcl.l	$$⊢L={\mathrm{Base}}_Q$$
11		ovexd	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\wedge m\in B\right)\to \underset{k\in {\mathbb{N}}_0}{{\sum }_Q}\left(\left(m\mathrm{decompPMat}k\right)\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\in \mathrm{V}$$
12	1 2 3 4 5 6 7 8 9	pm2mpval	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T=\left(m\in B⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_Q}\left(\left(m\mathrm{decompPMat}k\right)\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\right)$$
13	1 2 3 4 5 6 7 8 9 10	pm2mpcl	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge b\in B\right)\to T\left(b\right)\in L$$
14	13	3expa	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\wedge b\in B\right)\to T\left(b\right)\in L$$
15	11 12 14	fmpt2d	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T:B⟶L$$