Definition df-pm2mp

Description: Transformation of a polynomial matrix (over a ring) into a polynomial over matrices (over the same ring). (Contributed by AV, 5-Dec-2019)

	Ref	Expression
Assertion	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)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpm2mp	$$class\mathrm{pMatToMatPoly}$$
1		vn	$$setvarn$$
2		cfn	$$class\mathrm{Fin}$$
3		vr	$$setvarr$$
4		cvv	$$class\mathrm{V}$$
5		vm	$$setvarm$$
6		cbs	$$class\mathrm{Base}$$
7	1	cv	$$setvarn$$
8		cmat	$$class\mathrm{Mat}$$
9		cpl1	$$class{\mathrm{Poly}}_1$$
10	3	cv	$$setvarr$$
11	10 9	cfv	$$class{\mathrm{Poly}}_1\left(r\right)$$
12	7 11 8	co	$$class\left(n\mathrm{Mat}{\mathrm{Poly}}_1\left(r\right)\right)$$
13	12 6	cfv	$$class{\mathrm{Base}}_{\left(n\mathrm{Mat}{\mathrm{Poly}}_1\left(r\right)\right)}$$
14	7 10 8	co	$$class\left(n\mathrm{Mat}r\right)$$
15		va	$$setvara$$
16	15	cv	$$setvara$$
17	16 9	cfv	$$class{\mathrm{Poly}}_1\left(a\right)$$
18		vq	$$setvarq$$
19	18	cv	$$setvarq$$
20		cgsu	$$class{\Sigma }_{𝑔}$$
21		vk	$$setvark$$
22		cn0	$$class{\mathbb{N}}_0$$
23	5	cv	$$setvarm$$
24		cdecpmat	$$class\mathrm{decompPMat}$$
25	21	cv	$$setvark$$
26	23 25 24	co	$$class\left(m\mathrm{decompPMat}k\right)$$
27		cvsca	$$class{\cdot }_{𝑠}$$
28	19 27	cfv	$$class{\cdot }_q$$
29		cmg	$$class{\mathrm{\cdot }}_{𝑔}$$
30		cmgp	$$class\mathrm{mulGrp}$$
31	19 30	cfv	$$class{\mathrm{mulGrp}}_q$$
32	31 29	cfv	$$class{\cdot }_{{\mathrm{mulGrp}}_q}$$
33		cv1	$$class{\mathrm{var}}_1$$
34	16 33	cfv	$$class{\mathrm{var}}_1\left(a\right)$$
35	25 34 32	co	$$class\left(k{\cdot }_{{\mathrm{mulGrp}}_q}{\mathrm{var}}_1\left(a\right)\right)$$
36	26 35 28	co	$$class\left(\left(m\mathrm{decompPMat}k\right){\cdot }_q\left(k{\cdot }_{{\mathrm{mulGrp}}_q}{\mathrm{var}}_1\left(a\right)\right)\right)$$
37	21 22 36	cmpt	$$class\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)$$
38	19 37 20	co	$$class\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)$$
39	18 17 38	csb	$$class⦋{\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)$$
40	15 14 39	csb	$$class⦋\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)$$
41	5 13 40	cmpt	$$class\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)$$
42	1 3 2 4 41	cmpo	$$class\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)$$
43	0 42	wceq	$$wff\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)$$