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

Definition df-cpmat2mat 22729
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 22781, 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 22726 . 2 class cPolyMatToMat
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cfn 8983 . . 3 class Fin
5 cvv 3477 . . 3 class V
6 vm . . . 4 setvar 𝑚
72cv 1535 . . . . 5 class 𝑛
83cv 1535 . . . . 5 class 𝑟
9 ccpmat 22724 . . . . 5 class ConstPolyMat
107, 8, 9co 7430 . . . 4 class (𝑛 ConstPolyMat 𝑟)
11 vx . . . . 5 setvar 𝑥
12 vy . . . . 5 setvar 𝑦
13 cc0 11152 . . . . . 6 class 0
1411cv 1535 . . . . . . . 8 class 𝑥
1512cv 1535 . . . . . . . 8 class 𝑦
166cv 1535 . . . . . . . 8 class 𝑚
1714, 15, 16co 7430 . . . . . . 7 class (𝑥𝑚𝑦)
18 cco1 22194 . . . . . . 7 class coe1
1917, 18cfv 6562 . . . . . 6 class (coe1‘(𝑥𝑚𝑦))
2013, 19cfv 6562 . . . . 5 class ((coe1‘(𝑥𝑚𝑦))‘0)
2111, 12, 7, 7, 20cmpo 7432 . . . 4 class (𝑥𝑛, 𝑦𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))
226, 10, 21cmpt 5230 . . 3 class (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥𝑛, 𝑦𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0)))
232, 3, 4, 5, 22cmpo 7432 . 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥𝑛, 𝑦𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))))
241, 23wceq 1536 1 wff cPolyMatToMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥𝑛, 𝑦𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))))
Colors of variables: wff setvar class
This definition is referenced by:  cpm2mfval  22770
  Copyright terms: Public domain W3C validator