Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cpmat2mat Structured version   Visualization version   GIF version

Definition df-cpmat2mat 21311
 Description: Transformation of a constant polynomial matrix (over a ring) into a matrix over the corresponding ring. Since this function is the inverse function of matToPolyMat, see m2cpminv 21363, it is also called "inverse matrix transformation" in the following. (Contributed by AV, 14-Dec-2019.)
Assertion
Ref Expression
df-cpmat2mat cPolyMatToMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥𝑛, 𝑦𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))))
Distinct variable group:   𝑚,𝑛,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-cpmat2mat
StepHypRef Expression
1 ccpmat2mat 21308 . 2 class cPolyMatToMat
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cfn 8496 . . 3 class Fin
5 cvv 3469 . . 3 class V
6 vm . . . 4 setvar 𝑚
72cv 1537 . . . . 5 class 𝑛
83cv 1537 . . . . 5 class 𝑟
9 ccpmat 21306 . . . . 5 class ConstPolyMat
107, 8, 9co 7140 . . . 4 class (𝑛 ConstPolyMat 𝑟)
11 vx . . . . 5 setvar 𝑥
12 vy . . . . 5 setvar 𝑦
13 cc0 10526 . . . . . 6 class 0
1411cv 1537 . . . . . . . 8 class 𝑥
1512cv 1537 . . . . . . . 8 class 𝑦
166cv 1537 . . . . . . . 8 class 𝑚
1714, 15, 16co 7140 . . . . . . 7 class (𝑥𝑚𝑦)
18 cco1 20805 . . . . . . 7 class coe1
1917, 18cfv 6334 . . . . . 6 class (coe1‘(𝑥𝑚𝑦))
2013, 19cfv 6334 . . . . 5 class ((coe1‘(𝑥𝑚𝑦))‘0)
2111, 12, 7, 7, 20cmpo 7142 . . . 4 class (𝑥𝑛, 𝑦𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))
226, 10, 21cmpt 5122 . . 3 class (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥𝑛, 𝑦𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0)))
232, 3, 4, 5, 22cmpo 7142 . 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥𝑛, 𝑦𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))))
241, 23wceq 1538 1 wff cPolyMatToMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥𝑛, 𝑦𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))))
 Colors of variables: wff setvar class This definition is referenced by:  cpm2mfval  21352
 Copyright terms: Public domain W3C validator