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 20432
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 20484, 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 20429 . 2 class cPolyMatToMat
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cfn 7899 . . 3 class Fin
5 cvv 3186 . . 3 class V
6 vm . . . 4 setvar 𝑚
72cv 1479 . . . . 5 class 𝑛
83cv 1479 . . . . 5 class 𝑟
9 ccpmat 20427 . . . . 5 class ConstPolyMat
107, 8, 9co 6604 . . . 4 class (𝑛 ConstPolyMat 𝑟)
11 vx . . . . 5 setvar 𝑥
12 vy . . . . 5 setvar 𝑦
13 cc0 9880 . . . . . 6 class 0
1411cv 1479 . . . . . . . 8 class 𝑥
1512cv 1479 . . . . . . . 8 class 𝑦
166cv 1479 . . . . . . . 8 class 𝑚
1714, 15, 16co 6604 . . . . . . 7 class (𝑥𝑚𝑦)
18 cco1 19467 . . . . . . 7 class coe1
1917, 18cfv 5847 . . . . . 6 class (coe1‘(𝑥𝑚𝑦))
2013, 19cfv 5847 . . . . 5 class ((coe1‘(𝑥𝑚𝑦))‘0)
2111, 12, 7, 7, 20cmpt2 6606 . . . 4 class (𝑥𝑛, 𝑦𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))
226, 10, 21cmpt 4673 . . 3 class (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥𝑛, 𝑦𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0)))
232, 3, 4, 5, 22cmpt2 6606 . 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥𝑛, 𝑦𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))))
241, 23wceq 1480 1 wff cPolyMatToMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥𝑛, 𝑦𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))))
Colors of variables: wff setvar class
This definition is referenced by:  cpm2mfval  20473
  Copyright terms: Public domain W3C validator