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

Definition df-mat2pmat 22430
Description: Transformation of a matrix (over a ring) into a matrix over the corresponding polynomial ring. (Contributed by AV, 31-Jul-2019.)
Assertion
Ref Expression
df-mat2pmat matToPolyMat = (𝑛 ∈ Fin, π‘Ÿ ∈ V ↦ (π‘š ∈ (Baseβ€˜(𝑛 Mat π‘Ÿ)) ↦ (π‘₯ ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algScβ€˜(Poly1β€˜π‘Ÿ))β€˜(π‘₯π‘šπ‘¦)))))
Distinct variable group:   π‘š,𝑛,π‘Ÿ,π‘₯,𝑦

Detailed syntax breakdown of Definition df-mat2pmat
StepHypRef Expression
1 cmat2pmat 22427 . 2 class matToPolyMat
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar π‘Ÿ
4 cfn 8943 . . 3 class Fin
5 cvv 3473 . . 3 class V
6 vm . . . 4 setvar π‘š
72cv 1539 . . . . . 6 class 𝑛
83cv 1539 . . . . . 6 class π‘Ÿ
9 cmat 22128 . . . . . 6 class Mat
107, 8, 9co 7412 . . . . 5 class (𝑛 Mat π‘Ÿ)
11 cbs 17149 . . . . 5 class Base
1210, 11cfv 6543 . . . 4 class (Baseβ€˜(𝑛 Mat π‘Ÿ))
13 vx . . . . 5 setvar π‘₯
14 vy . . . . 5 setvar 𝑦
1513cv 1539 . . . . . . 7 class π‘₯
1614cv 1539 . . . . . . 7 class 𝑦
176cv 1539 . . . . . . 7 class π‘š
1815, 16, 17co 7412 . . . . . 6 class (π‘₯π‘šπ‘¦)
19 cpl1 21921 . . . . . . . 8 class Poly1
208, 19cfv 6543 . . . . . . 7 class (Poly1β€˜π‘Ÿ)
21 cascl 21627 . . . . . . 7 class algSc
2220, 21cfv 6543 . . . . . 6 class (algScβ€˜(Poly1β€˜π‘Ÿ))
2318, 22cfv 6543 . . . . 5 class ((algScβ€˜(Poly1β€˜π‘Ÿ))β€˜(π‘₯π‘šπ‘¦))
2413, 14, 7, 7, 23cmpo 7414 . . . 4 class (π‘₯ ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algScβ€˜(Poly1β€˜π‘Ÿ))β€˜(π‘₯π‘šπ‘¦)))
256, 12, 24cmpt 5231 . . 3 class (π‘š ∈ (Baseβ€˜(𝑛 Mat π‘Ÿ)) ↦ (π‘₯ ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algScβ€˜(Poly1β€˜π‘Ÿ))β€˜(π‘₯π‘šπ‘¦))))
262, 3, 4, 5, 25cmpo 7414 . 2 class (𝑛 ∈ Fin, π‘Ÿ ∈ V ↦ (π‘š ∈ (Baseβ€˜(𝑛 Mat π‘Ÿ)) ↦ (π‘₯ ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algScβ€˜(Poly1β€˜π‘Ÿ))β€˜(π‘₯π‘šπ‘¦)))))
271, 26wceq 1540 1 wff matToPolyMat = (𝑛 ∈ Fin, π‘Ÿ ∈ V ↦ (π‘š ∈ (Baseβ€˜(𝑛 Mat π‘Ÿ)) ↦ (π‘₯ ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algScβ€˜(Poly1β€˜π‘Ÿ))β€˜(π‘₯π‘šπ‘¦)))))
Colors of variables: wff setvar class
This definition is referenced by:  mat2pmatfval  22446
  Copyright terms: Public domain W3C validator