# Metamath Proof Explorer

## 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

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cpm2mp ${class}\mathrm{pMatToMatPoly}$
1 vn ${setvar}{n}$
2 cfn ${class}\mathrm{Fin}$
3 vr ${setvar}{r}$
4 cvv ${class}\mathrm{V}$
5 vm ${setvar}{m}$
6 cbs ${class}\mathrm{Base}$
7 1 cv ${setvar}{n}$
8 cmat ${class}\mathrm{Mat}$
9 cpl1 ${class}{\mathrm{Poly}}_{1}$
10 3 cv ${setvar}{r}$
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 ${setvar}{a}$
16 15 cv ${setvar}{a}$
17 16 9 cfv ${class}{\mathrm{Poly}}_{1}\left({a}\right)$
18 vq ${setvar}{q}$
19 18 cv ${setvar}{q}$
20 cgsu ${class}{\Sigma }_{𝑔}$
21 vk ${setvar}{k}$
22 cn0 ${class}{ℕ}_{0}$
23 5 cv ${setvar}{m}$
24 cdecpmat ${class}\mathrm{decompPMat}$
25 21 cv ${setvar}{k}$
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}{\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 {ℕ}_{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 {ℕ}_{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
40 15 14 39 csb
41 5 13 40 cmpt
42 1 3 2 4 41 cmpo
43 0 42 wceq