Theorem pm2mpfval

Description: A polynomial matrix transformed into a polynomial over matrices. (Contributed by AV, 4-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$$
Assertion	pm2mpfval	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\wedge M\in B\right)\to T\left(M\right)=\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)$$

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	1 2 3 4 5 6 7 8 9	pm2mpval	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\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)$$
11	10	3adant3	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\wedge M\in B\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)$$
12		oveq1	$$⊢m=M\to m\mathrm{decompPMat}k=M\mathrm{decompPMat}k$$
13	12	oveq1d	$$⊢m=M\to \left(m\mathrm{decompPMat}k\right)\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)=\left(M\mathrm{decompPMat}k\right)\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)$$
14	13	mpteq2dv	$$⊢m=M\to \left(k\in {\mathbb{N}}_0⟼\left(m\mathrm{decompPMat}k\right)\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)=\left(k\in {\mathbb{N}}_0⟼\left(M\mathrm{decompPMat}k\right)\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)$$
15	14	oveq2d	$$⊢m=M\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)=\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)$$
16	15	adantl	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in V\wedge M\in B\right)\wedge m=M\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)=\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)$$
17		simp3	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\wedge M\in B\right)\to M\in B$$
18		ovexd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\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}$$
19	11 16 17 18	fvmptd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\wedge M\in B\right)\to T\left(M\right)=\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)$$