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 20359
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 20358 . 2 class pMatToMatPoly
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cfn 7818 . . 3 class Fin
5 cvv 3172 . . 3 class V
6 vm . . . 4 setvar 𝑚
72cv 1473 . . . . . 6 class 𝑛
83cv 1473 . . . . . . 7 class 𝑟
9 cpl1 19314 . . . . . . 7 class Poly1
108, 9cfv 5790 . . . . . 6 class (Poly1𝑟)
11 cmat 19974 . . . . . 6 class Mat
127, 10, 11co 6527 . . . . 5 class (𝑛 Mat (Poly1𝑟))
13 cbs 15641 . . . . 5 class Base
1412, 13cfv 5790 . . . 4 class (Base‘(𝑛 Mat (Poly1𝑟)))
15 va . . . . 5 setvar 𝑎
167, 8, 11co 6527 . . . . 5 class (𝑛 Mat 𝑟)
17 vq . . . . . 6 setvar 𝑞
1815cv 1473 . . . . . . 7 class 𝑎
1918, 9cfv 5790 . . . . . 6 class (Poly1𝑎)
2017cv 1473 . . . . . . 7 class 𝑞
21 vk . . . . . . . 8 setvar 𝑘
22 cn0 11139 . . . . . . . 8 class 0
236cv 1473 . . . . . . . . . 10 class 𝑚
2421cv 1473 . . . . . . . . . 10 class 𝑘
25 cdecpmat 20328 . . . . . . . . . 10 class decompPMat
2623, 24, 25co 6527 . . . . . . . . 9 class (𝑚 decompPMat 𝑘)
27 cv1 19313 . . . . . . . . . . 11 class var1
2818, 27cfv 5790 . . . . . . . . . 10 class (var1𝑎)
29 cmgp 18258 . . . . . . . . . . . 12 class mulGrp
3020, 29cfv 5790 . . . . . . . . . . 11 class (mulGrp‘𝑞)
31 cmg 17309 . . . . . . . . . . 11 class .g
3230, 31cfv 5790 . . . . . . . . . 10 class (.g‘(mulGrp‘𝑞))
3324, 28, 32co 6527 . . . . . . . . 9 class (𝑘(.g‘(mulGrp‘𝑞))(var1𝑎))
34 cvsca 15718 . . . . . . . . . 10 class ·𝑠
3520, 34cfv 5790 . . . . . . . . 9 class ( ·𝑠𝑞)
3626, 33, 35co 6527 . . . . . . . 8 class ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))
3721, 22, 36cmpt 4637 . . . . . . 7 class (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎))))
38 cgsu 15870 . . . . . . 7 class Σg
3920, 37, 38co 6527 . . . . . 6 class (𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))))
4017, 19, 39csb 3498 . . . . 5 class (Poly1𝑎) / 𝑞(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))))
4115, 16, 40csb 3498 . . . 4 class (𝑛 Mat 𝑟) / 𝑎(Poly1𝑎) / 𝑞(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))))
426, 14, 41cmpt 4637 . . 3 class (𝑚 ∈ (Base‘(𝑛 Mat (Poly1𝑟))) ↦ (𝑛 Mat 𝑟) / 𝑎(Poly1𝑎) / 𝑞(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎))))))
432, 3, 4, 5, 42cmpt2 6529 . 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat (Poly1𝑟))) ↦ (𝑛 Mat 𝑟) / 𝑎(Poly1𝑎) / 𝑞(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))))))
441, 43wceq 1474 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  20361
  Copyright terms: Public domain W3C validator