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

Definition df-pm2mp 21952
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 21951 . 2 class pMatToMatPoly
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cfn 8720 . . 3 class Fin
5 cvv 3429 . . 3 class V
6 vm . . . 4 setvar 𝑚
72cv 1538 . . . . . 6 class 𝑛
83cv 1538 . . . . . . 7 class 𝑟
9 cpl1 21358 . . . . . . 7 class Poly1
108, 9cfv 6426 . . . . . 6 class (Poly1𝑟)
11 cmat 21564 . . . . . 6 class Mat
127, 10, 11co 7267 . . . . 5 class (𝑛 Mat (Poly1𝑟))
13 cbs 16922 . . . . 5 class Base
1412, 13cfv 6426 . . . 4 class (Base‘(𝑛 Mat (Poly1𝑟)))
15 va . . . . 5 setvar 𝑎
167, 8, 11co 7267 . . . . 5 class (𝑛 Mat 𝑟)
17 vq . . . . . 6 setvar 𝑞
1815cv 1538 . . . . . . 7 class 𝑎
1918, 9cfv 6426 . . . . . 6 class (Poly1𝑎)
2017cv 1538 . . . . . . 7 class 𝑞
21 vk . . . . . . . 8 setvar 𝑘
22 cn0 12243 . . . . . . . 8 class 0
236cv 1538 . . . . . . . . . 10 class 𝑚
2421cv 1538 . . . . . . . . . 10 class 𝑘
25 cdecpmat 21921 . . . . . . . . . 10 class decompPMat
2623, 24, 25co 7267 . . . . . . . . 9 class (𝑚 decompPMat 𝑘)
27 cv1 21357 . . . . . . . . . . 11 class var1
2818, 27cfv 6426 . . . . . . . . . 10 class (var1𝑎)
29 cmgp 19730 . . . . . . . . . . . 12 class mulGrp
3020, 29cfv 6426 . . . . . . . . . . 11 class (mulGrp‘𝑞)
31 cmg 18710 . . . . . . . . . . 11 class .g
3230, 31cfv 6426 . . . . . . . . . 10 class (.g‘(mulGrp‘𝑞))
3324, 28, 32co 7267 . . . . . . . . 9 class (𝑘(.g‘(mulGrp‘𝑞))(var1𝑎))
34 cvsca 16976 . . . . . . . . . 10 class ·𝑠
3520, 34cfv 6426 . . . . . . . . 9 class ( ·𝑠𝑞)
3626, 33, 35co 7267 . . . . . . . 8 class ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))
3721, 22, 36cmpt 5156 . . . . . . 7 class (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎))))
38 cgsu 17161 . . . . . . 7 class Σg
3920, 37, 38co 7267 . . . . . 6 class (𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))))
4017, 19, 39csb 3831 . . . . 5 class (Poly1𝑎) / 𝑞(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))))
4115, 16, 40csb 3831 . . . 4 class (𝑛 Mat 𝑟) / 𝑎(Poly1𝑎) / 𝑞(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))))
426, 14, 41cmpt 5156 . . 3 class (𝑚 ∈ (Base‘(𝑛 Mat (Poly1𝑟))) ↦ (𝑛 Mat 𝑟) / 𝑎(Poly1𝑎) / 𝑞(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎))))))
432, 3, 4, 5, 42cmpo 7269 . 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat (Poly1𝑟))) ↦ (𝑛 Mat 𝑟) / 𝑎(Poly1𝑎) / 𝑞(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))))))
441, 43wceq 1539 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  21954
  Copyright terms: Public domain W3C validator