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

Definition df-pm2mp 21395
 Description: Transformation of a polynomial matrix (over a ring) into a polynomial over matrices (over the same ring). (Contributed by AV, 5-Dec-2019.)
Assertion
Ref Expression
df-pm2mp pMatToMatPoly = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat (Poly1𝑟))) ↦ (𝑛 Mat 𝑟) / 𝑎(Poly1𝑎) / 𝑞(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))))))
Distinct variable group:   𝑘,𝑎,𝑛,𝑚,𝑞,𝑟

Detailed syntax breakdown of Definition df-pm2mp
StepHypRef Expression
1 cpm2mp 21394 . 2 class pMatToMatPoly
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cfn 8503 . . 3 class Fin
5 cvv 3494 . . 3 class V
6 vm . . . 4 setvar 𝑚
72cv 1532 . . . . . 6 class 𝑛
83cv 1532 . . . . . . 7 class 𝑟
9 cpl1 20339 . . . . . . 7 class Poly1
108, 9cfv 6349 . . . . . 6 class (Poly1𝑟)
11 cmat 21010 . . . . . 6 class Mat
127, 10, 11co 7150 . . . . 5 class (𝑛 Mat (Poly1𝑟))
13 cbs 16477 . . . . 5 class Base
1412, 13cfv 6349 . . . 4 class (Base‘(𝑛 Mat (Poly1𝑟)))
15 va . . . . 5 setvar 𝑎
167, 8, 11co 7150 . . . . 5 class (𝑛 Mat 𝑟)
17 vq . . . . . 6 setvar 𝑞
1815cv 1532 . . . . . . 7 class 𝑎
1918, 9cfv 6349 . . . . . 6 class (Poly1𝑎)
2017cv 1532 . . . . . . 7 class 𝑞
21 vk . . . . . . . 8 setvar 𝑘
22 cn0 11891 . . . . . . . 8 class 0
236cv 1532 . . . . . . . . . 10 class 𝑚
2421cv 1532 . . . . . . . . . 10 class 𝑘
25 cdecpmat 21364 . . . . . . . . . 10 class decompPMat
2623, 24, 25co 7150 . . . . . . . . 9 class (𝑚 decompPMat 𝑘)
27 cv1 20338 . . . . . . . . . . 11 class var1
2818, 27cfv 6349 . . . . . . . . . 10 class (var1𝑎)
29 cmgp 19233 . . . . . . . . . . . 12 class mulGrp
3020, 29cfv 6349 . . . . . . . . . . 11 class (mulGrp‘𝑞)
31 cmg 18218 . . . . . . . . . . 11 class .g
3230, 31cfv 6349 . . . . . . . . . 10 class (.g‘(mulGrp‘𝑞))
3324, 28, 32co 7150 . . . . . . . . 9 class (𝑘(.g‘(mulGrp‘𝑞))(var1𝑎))
34 cvsca 16563 . . . . . . . . . 10 class ·𝑠
3520, 34cfv 6349 . . . . . . . . 9 class ( ·𝑠𝑞)
3626, 33, 35co 7150 . . . . . . . 8 class ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))
3721, 22, 36cmpt 5138 . . . . . . 7 class (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎))))
38 cgsu 16708 . . . . . . 7 class Σg
3920, 37, 38co 7150 . . . . . 6 class (𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))))
4017, 19, 39csb 3882 . . . . 5 class (Poly1𝑎) / 𝑞(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))))
4115, 16, 40csb 3882 . . . 4 class (𝑛 Mat 𝑟) / 𝑎(Poly1𝑎) / 𝑞(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))))
426, 14, 41cmpt 5138 . . 3 class (𝑚 ∈ (Base‘(𝑛 Mat (Poly1𝑟))) ↦ (𝑛 Mat 𝑟) / 𝑎(Poly1𝑎) / 𝑞(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎))))))
432, 3, 4, 5, 42cmpo 7152 . 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat (Poly1𝑟))) ↦ (𝑛 Mat 𝑟) / 𝑎(Poly1𝑎) / 𝑞(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))))))
441, 43wceq 1533 1 wff pMatToMatPoly = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat (Poly1𝑟))) ↦ (𝑛 Mat 𝑟) / 𝑎(Poly1𝑎) / 𝑞(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))))))
 Colors of variables: wff setvar class This definition is referenced by:  pm2mpval  21397
 Copyright terms: Public domain W3C validator