# Metamath Proof Explorer

## Definition df-mat2pmat

Description: Transformation of a matrix (over a ring) into a matrix over the corresponding polynomial ring. (Contributed by AV, 31-Jul-2019)

Ref Expression
Assertion df-mat2pmat ${⊢}\mathrm{matToPolyMat}=\left({n}\in \mathrm{Fin},{r}\in \mathrm{V}⟼\left({m}\in {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}⟼\left({x}\in {n},{y}\in {n}⟼\mathrm{algSc}\left({\mathrm{Poly}}_{1}\left({r}\right)\right)\left({x}{m}{y}\right)\right)\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cmat2pmat ${class}\mathrm{matToPolyMat}$
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 3 cv ${setvar}{r}$
10 7 9 8 co ${class}\left({n}\mathrm{Mat}{r}\right)$
11 10 6 cfv ${class}{\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}$
12 vx ${setvar}{x}$
13 vy ${setvar}{y}$
14 cascl ${class}\mathrm{algSc}$
15 cpl1 ${class}{\mathrm{Poly}}_{1}$
16 9 15 cfv ${class}{\mathrm{Poly}}_{1}\left({r}\right)$
17 16 14 cfv ${class}\mathrm{algSc}\left({\mathrm{Poly}}_{1}\left({r}\right)\right)$
18 12 cv ${setvar}{x}$
19 5 cv ${setvar}{m}$
20 13 cv ${setvar}{y}$
21 18 20 19 co ${class}\left({x}{m}{y}\right)$
22 21 17 cfv ${class}\mathrm{algSc}\left({\mathrm{Poly}}_{1}\left({r}\right)\right)\left({x}{m}{y}\right)$
23 12 13 7 7 22 cmpo ${class}\left({x}\in {n},{y}\in {n}⟼\mathrm{algSc}\left({\mathrm{Poly}}_{1}\left({r}\right)\right)\left({x}{m}{y}\right)\right)$
24 5 11 23 cmpt ${class}\left({m}\in {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}⟼\left({x}\in {n},{y}\in {n}⟼\mathrm{algSc}\left({\mathrm{Poly}}_{1}\left({r}\right)\right)\left({x}{m}{y}\right)\right)\right)$
25 1 3 2 4 24 cmpo ${class}\left({n}\in \mathrm{Fin},{r}\in \mathrm{V}⟼\left({m}\in {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}⟼\left({x}\in {n},{y}\in {n}⟼\mathrm{algSc}\left({\mathrm{Poly}}_{1}\left({r}\right)\right)\left({x}{m}{y}\right)\right)\right)\right)$
26 0 25 wceq ${wff}\mathrm{matToPolyMat}=\left({n}\in \mathrm{Fin},{r}\in \mathrm{V}⟼\left({m}\in {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}⟼\left({x}\in {n},{y}\in {n}⟼\mathrm{algSc}\left({\mathrm{Poly}}_{1}\left({r}\right)\right)\left({x}{m}{y}\right)\right)\right)\right)$