Theorem pm2mpval

Description: Value of the transformation of a polynomial matrix into a polynomial over matrices. (Contributed 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	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)$$

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		df-pm2mp	$$⊢\mathrm{pMatToMatPoly}=\left(n\in \mathrm{Fin},r\in \mathrm{V}⟼\left(m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}{\mathrm{Poly}}_1\left(r\right)\right)}⟼⦋\left(n\mathrm{Mat}r\right)/a⦌⦋{\mathrm{Poly}}_1\left(a\right)/q⦌\left(\underset{k\in {\mathbb{N}}_0}{{\sum }_q},\left(\left(m\mathrm{decompPMat}k\right){\cdot }_q\left(k{\cdot }_{{\mathrm{mulGrp}}_q}{\mathrm{var}}_1\left(a\right)\right)\right)\right)\right)\right)$$
11	10	a1i	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to \mathrm{pMatToMatPoly}=\left(n\in \mathrm{Fin},r\in \mathrm{V}⟼\left(m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}{\mathrm{Poly}}_1\left(r\right)\right)}⟼⦋\left(n\mathrm{Mat}r\right)/a⦌⦋{\mathrm{Poly}}_1\left(a\right)/q⦌\left(\underset{k\in {\mathbb{N}}_0}{{\sum }_q},\left(\left(m\mathrm{decompPMat}k\right){\cdot }_q\left(k{\cdot }_{{\mathrm{mulGrp}}_q}{\mathrm{var}}_1\left(a\right)\right)\right)\right)\right)\right)$$
12		simpl	$$⊢\left(n=N\wedge r=R\right)\to n=N$$
13		fveq2	$$⊢r=R\to {\mathrm{Poly}}_1\left(r\right)={\mathrm{Poly}}_1\left(R\right)$$
14	13	adantl	$$⊢\left(n=N\wedge r=R\right)\to {\mathrm{Poly}}_1\left(r\right)={\mathrm{Poly}}_1\left(R\right)$$
15	12 14	oveq12d	$$⊢\left(n=N\wedge r=R\right)\to n\mathrm{Mat}{\mathrm{Poly}}_1\left(r\right)=N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)$$
16	15	fveq2d	$$⊢\left(n=N\wedge r=R\right)\to {\mathrm{Base}}_{\left(n\mathrm{Mat}{\mathrm{Poly}}_1\left(r\right)\right)}={\mathrm{Base}}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}$$
17	1	oveq2i	$$⊢N\mathrm{Mat}P=N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)$$
18	2 17	eqtri	$$⊢C=N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)$$
19	18	fveq2i	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}$$
20	3 19	eqtri	$$⊢B={\mathrm{Base}}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}$$
21	16 20	eqtr4di	$$⊢\left(n=N\wedge r=R\right)\to {\mathrm{Base}}_{\left(n\mathrm{Mat}{\mathrm{Poly}}_1\left(r\right)\right)}=B$$
22	21	adantl	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in V\right)\wedge \left(n=N\wedge r=R\right)\right)\to {\mathrm{Base}}_{\left(n\mathrm{Mat}{\mathrm{Poly}}_1\left(r\right)\right)}=B$$
23		ovex	$$⊢n\mathrm{Mat}r\in \mathrm{V}$$
24		fvexd	$$⊢a=n\mathrm{Mat}r\to {\mathrm{Poly}}_1\left(a\right)\in \mathrm{V}$$
25		simpr	$$⊢\left(a=n\mathrm{Mat}r\wedge q={\mathrm{Poly}}_1\left(a\right)\right)\to q={\mathrm{Poly}}_1\left(a\right)$$
26		fveq2	$$⊢a=n\mathrm{Mat}r\to {\mathrm{Poly}}_1\left(a\right)={\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)$$
27	26	adantr	$$⊢\left(a=n\mathrm{Mat}r\wedge q={\mathrm{Poly}}_1\left(a\right)\right)\to {\mathrm{Poly}}_1\left(a\right)={\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)$$
28	25 27	eqtrd	$$⊢\left(a=n\mathrm{Mat}r\wedge q={\mathrm{Poly}}_1\left(a\right)\right)\to q={\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)$$
29	28	fveq2d	$$⊢\left(a=n\mathrm{Mat}r\wedge q={\mathrm{Poly}}_1\left(a\right)\right)\to {\cdot }_q={\cdot }_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}$$
30		eqidd	$$⊢\left(a=n\mathrm{Mat}r\wedge q={\mathrm{Poly}}_1\left(a\right)\right)\to m\mathrm{decompPMat}k=m\mathrm{decompPMat}k$$
31	28	fveq2d	$$⊢\left(a=n\mathrm{Mat}r\wedge q={\mathrm{Poly}}_1\left(a\right)\right)\to {\mathrm{mulGrp}}_q={\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}$$
32	31	fveq2d	$$⊢\left(a=n\mathrm{Mat}r\wedge q={\mathrm{Poly}}_1\left(a\right)\right)\to {\cdot }_{{\mathrm{mulGrp}}_q}={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}}$$
33		eqidd	$$⊢\left(a=n\mathrm{Mat}r\wedge q={\mathrm{Poly}}_1\left(a\right)\right)\to k=k$$
34		fveq2	$$⊢a=n\mathrm{Mat}r\to {\mathrm{var}}_1\left(a\right)={\mathrm{var}}_1\left(n\mathrm{Mat}r\right)$$
35	34	adantr	$$⊢\left(a=n\mathrm{Mat}r\wedge q={\mathrm{Poly}}_1\left(a\right)\right)\to {\mathrm{var}}_1\left(a\right)={\mathrm{var}}_1\left(n\mathrm{Mat}r\right)$$
36	32 33 35	oveq123d	$$⊢\left(a=n\mathrm{Mat}r\wedge q={\mathrm{Poly}}_1\left(a\right)\right)\to k{\cdot }_{{\mathrm{mulGrp}}_q}{\mathrm{var}}_1\left(a\right)=k{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}}{\mathrm{var}}_1\left(n\mathrm{Mat}r\right)$$
37	29 30 36	oveq123d	$$⊢\left(a=n\mathrm{Mat}r\wedge q={\mathrm{Poly}}_1\left(a\right)\right)\to \left(m\mathrm{decompPMat}k\right){\cdot }_q\left(k{\cdot }_{{\mathrm{mulGrp}}_q}{\mathrm{var}}_1\left(a\right)\right)=\left(m\mathrm{decompPMat}k\right){\cdot }_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}\left(k{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}}{\mathrm{var}}_1\left(n\mathrm{Mat}r\right)\right)$$
38	37	mpteq2dv	$$⊢\left(a=n\mathrm{Mat}r\wedge q={\mathrm{Poly}}_1\left(a\right)\right)\to \left(k\in {\mathbb{N}}_0⟼\left(m\mathrm{decompPMat}k\right){\cdot }_q\left(k{\cdot }_{{\mathrm{mulGrp}}_q}{\mathrm{var}}_1\left(a\right)\right)\right)=\left(k\in {\mathbb{N}}_0⟼\left(m\mathrm{decompPMat}k\right){\cdot }_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}\left(k{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}}{\mathrm{var}}_1\left(n\mathrm{Mat}r\right)\right)\right)$$
39	28 38	oveq12d	$$⊢\left(a=n\mathrm{Mat}r\wedge q={\mathrm{Poly}}_1\left(a\right)\right)\to \underset{k\in {\mathbb{N}}_0}{{\sum }_q}\left(\left(m\mathrm{decompPMat}k\right){\cdot }_q\left(k{\cdot }_{{\mathrm{mulGrp}}_q}{\mathrm{var}}_1\left(a\right)\right)\right)=\underset{k\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}}\left(\left(m\mathrm{decompPMat}k\right){\cdot }_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}\left(k{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}}{\mathrm{var}}_1\left(n\mathrm{Mat}r\right)\right)\right)$$
40	24 39	csbied	$$⊢a=n\mathrm{Mat}r\to ⦋{\mathrm{Poly}}_1\left(a\right)/q⦌\left(\underset{k\in {\mathbb{N}}_0}{{\sum }_q},\left(\left(m\mathrm{decompPMat}k\right){\cdot }_q\left(k{\cdot }_{{\mathrm{mulGrp}}_q}{\mathrm{var}}_1\left(a\right)\right)\right)\right)=\underset{k\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}}\left(\left(m\mathrm{decompPMat}k\right){\cdot }_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}\left(k{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}}{\mathrm{var}}_1\left(n\mathrm{Mat}r\right)\right)\right)$$
41	23 40	csbie	$$⊢⦋\left(n\mathrm{Mat}r\right)/a⦌⦋{\mathrm{Poly}}_1\left(a\right)/q⦌\left(\underset{k\in {\mathbb{N}}_0}{{\sum }_q},\left(\left(m\mathrm{decompPMat}k\right){\cdot }_q\left(k{\cdot }_{{\mathrm{mulGrp}}_q}{\mathrm{var}}_1\left(a\right)\right)\right)\right)=\underset{k\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}}\left(\left(m\mathrm{decompPMat}k\right){\cdot }_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}\left(k{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}}{\mathrm{var}}_1\left(n\mathrm{Mat}r\right)\right)\right)$$
42		oveq12	$$⊢\left(n=N\wedge r=R\right)\to n\mathrm{Mat}r=N\mathrm{Mat}R$$
43	42	fveq2d	$$⊢\left(n=N\wedge r=R\right)\to {\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)={\mathrm{Poly}}_1\left(N\mathrm{Mat}R\right)$$
44	7	fveq2i	$$⊢{\mathrm{Poly}}_1\left(A\right)={\mathrm{Poly}}_1\left(N\mathrm{Mat}R\right)$$
45	8 44	eqtri	$$⊢Q={\mathrm{Poly}}_1\left(N\mathrm{Mat}R\right)$$
46	43 45	eqtr4di	$$⊢\left(n=N\wedge r=R\right)\to {\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)=Q$$
47	43	fveq2d	$$⊢\left(n=N\wedge r=R\right)\to {\cdot }_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}={\cdot }_{{\mathrm{Poly}}_1\left(N\mathrm{Mat}R\right)}$$
48	45	fveq2i	$$⊢{\cdot }_Q={\cdot }_{{\mathrm{Poly}}_1\left(N\mathrm{Mat}R\right)}$$
49	4 48	eqtri	$$⊢\underset{\dot{}}{\ast }={\cdot }_{{\mathrm{Poly}}_1\left(N\mathrm{Mat}R\right)}$$
50	47 49	eqtr4di	$$⊢\left(n=N\wedge r=R\right)\to {\cdot }_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}=\underset{\dot{}}{\ast }$$
51		eqidd	$$⊢\left(n=N\wedge r=R\right)\to m\mathrm{decompPMat}k=m\mathrm{decompPMat}k$$
52	43	fveq2d	$$⊢\left(n=N\wedge r=R\right)\to {\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}={\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(N\mathrm{Mat}R\right)}$$
53	52	fveq2d	$$⊢\left(n=N\wedge r=R\right)\to {\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}}={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(N\mathrm{Mat}R\right)}}$$
54	45	fveq2i	$$⊢{\mathrm{mulGrp}}_Q={\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(N\mathrm{Mat}R\right)}$$
55	54	fveq2i	$$⊢{\cdot }_{{\mathrm{mulGrp}}_Q}={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(N\mathrm{Mat}R\right)}}$$
56	5 55	eqtri	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(N\mathrm{Mat}R\right)}}$$
57	53 56	eqtr4di	$$⊢\left(n=N\wedge r=R\right)\to {\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}}=\underset{\dot{}}{\times }$$
58		eqidd	$$⊢\left(n=N\wedge r=R\right)\to k=k$$
59	42	fveq2d	$$⊢\left(n=N\wedge r=R\right)\to {\mathrm{var}}_1\left(n\mathrm{Mat}r\right)={\mathrm{var}}_1\left(N\mathrm{Mat}R\right)$$
60	7	fveq2i	$$⊢{\mathrm{var}}_1\left(A\right)={\mathrm{var}}_1\left(N\mathrm{Mat}R\right)$$
61	6 60	eqtri	$$⊢X={\mathrm{var}}_1\left(N\mathrm{Mat}R\right)$$
62	59 61	eqtr4di	$$⊢\left(n=N\wedge r=R\right)\to {\mathrm{var}}_1\left(n\mathrm{Mat}r\right)=X$$
63	57 58 62	oveq123d	$$⊢\left(n=N\wedge r=R\right)\to k{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}}{\mathrm{var}}_1\left(n\mathrm{Mat}r\right)=k\underset{\dot{}}{\times }X$$
64	50 51 63	oveq123d	$$⊢\left(n=N\wedge r=R\right)\to \left(m\mathrm{decompPMat}k\right){\cdot }_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}\left(k{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}}{\mathrm{var}}_1\left(n\mathrm{Mat}r\right)\right)=\left(m\mathrm{decompPMat}k\right)\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)$$
65	64	mpteq2dv	$$⊢\left(n=N\wedge r=R\right)\to \left(k\in {\mathbb{N}}_0⟼\left(m\mathrm{decompPMat}k\right){\cdot }_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}\left(k{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}}{\mathrm{var}}_1\left(n\mathrm{Mat}r\right)\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)$$
66	46 65	oveq12d	$$⊢\left(n=N\wedge r=R\right)\to \underset{k\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}}\left(\left(m\mathrm{decompPMat}k\right){\cdot }_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}\left(k{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}}{\mathrm{var}}_1\left(n\mathrm{Mat}r\right)\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)$$
67	66	adantl	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in V\right)\wedge \left(n=N\wedge r=R\right)\right)\to \underset{k\in {\mathbb{N}}_0}{{\sum }_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}}\left(\left(m\mathrm{decompPMat}k\right){\cdot }_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}\left(k{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left(n\mathrm{Mat}r\right)}}{\mathrm{var}}_1\left(n\mathrm{Mat}r\right)\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)$$
68	41 67	syl5eq	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in V\right)\wedge \left(n=N\wedge r=R\right)\right)\to ⦋\left(n\mathrm{Mat}r\right)/a⦌⦋{\mathrm{Poly}}_1\left(a\right)/q⦌\left(\underset{k\in {\mathbb{N}}_0}{{\sum }_q},\left(\left(m\mathrm{decompPMat}k\right){\cdot }_q\left(k{\cdot }_{{\mathrm{mulGrp}}_q}{\mathrm{var}}_1\left(a\right)\right)\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)$$
69	22 68	mpteq12dv	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in V\right)\wedge \left(n=N\wedge r=R\right)\right)\to \left(m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}{\mathrm{Poly}}_1\left(r\right)\right)}⟼⦋\left(n\mathrm{Mat}r\right)/a⦌⦋{\mathrm{Poly}}_1\left(a\right)/q⦌\left(\underset{k\in {\mathbb{N}}_0}{{\sum }_q},\left(\left(m\mathrm{decompPMat}k\right){\cdot }_q\left(k{\cdot }_{{\mathrm{mulGrp}}_q}{\mathrm{var}}_1\left(a\right)\right)\right)\right)\right)=\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)$$
70		simpl	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to N\in \mathrm{Fin}$$
71		elex	$$⊢R\in V\to R\in \mathrm{V}$$
72	71	adantl	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to R\in \mathrm{V}$$
73	3	fvexi	$$⊢B\in \mathrm{V}$$
74	73	mptex	$$⊢\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)\in \mathrm{V}$$
75	74	a1i	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to \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)\in \mathrm{V}$$
76	11 69 70 72 75	ovmpod	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to N\mathrm{pMatToMatPoly}R=\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)$$
77	9 76	syl5eq	$$⊢\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)$$