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

Definition df-pm2mp 20818
 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 20817 . 2 class pMatToMatPoly
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cfn 8109 . . 3 class Fin
5 cvv 3351 . . 3 class V
6 vm . . . 4 setvar 𝑚
72cv 1630 . . . . . 6 class 𝑛
83cv 1630 . . . . . . 7 class 𝑟
9 cpl1 19762 . . . . . . 7 class Poly1
108, 9cfv 6031 . . . . . 6 class (Poly1𝑟)
11 cmat 20430 . . . . . 6 class Mat
127, 10, 11co 6793 . . . . 5 class (𝑛 Mat (Poly1𝑟))
13 cbs 16064 . . . . 5 class Base
1412, 13cfv 6031 . . . 4 class (Base‘(𝑛 Mat (Poly1𝑟)))
15 va . . . . 5 setvar 𝑎
167, 8, 11co 6793 . . . . 5 class (𝑛 Mat 𝑟)
17 vq . . . . . 6 setvar 𝑞
1815cv 1630 . . . . . . 7 class 𝑎
1918, 9cfv 6031 . . . . . 6 class (Poly1𝑎)
2017cv 1630 . . . . . . 7 class 𝑞
21 vk . . . . . . . 8 setvar 𝑘
22 cn0 11494 . . . . . . . 8 class 0
236cv 1630 . . . . . . . . . 10 class 𝑚
2421cv 1630 . . . . . . . . . 10 class 𝑘
25 cdecpmat 20787 . . . . . . . . . 10 class decompPMat
2623, 24, 25co 6793 . . . . . . . . 9 class (𝑚 decompPMat 𝑘)
27 cv1 19761 . . . . . . . . . . 11 class var1
2818, 27cfv 6031 . . . . . . . . . 10 class (var1𝑎)
29 cmgp 18697 . . . . . . . . . . . 12 class mulGrp
3020, 29cfv 6031 . . . . . . . . . . 11 class (mulGrp‘𝑞)
31 cmg 17748 . . . . . . . . . . 11 class .g
3230, 31cfv 6031 . . . . . . . . . 10 class (.g‘(mulGrp‘𝑞))
3324, 28, 32co 6793 . . . . . . . . 9 class (𝑘(.g‘(mulGrp‘𝑞))(var1𝑎))
34 cvsca 16153 . . . . . . . . . 10 class ·𝑠
3520, 34cfv 6031 . . . . . . . . 9 class ( ·𝑠𝑞)
3626, 33, 35co 6793 . . . . . . . 8 class ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))
3721, 22, 36cmpt 4863 . . . . . . 7 class (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎))))
38 cgsu 16309 . . . . . . 7 class Σg
3920, 37, 38co 6793 . . . . . 6 class (𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))))
4017, 19, 39csb 3682 . . . . 5 class (Poly1𝑎) / 𝑞(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))))
4115, 16, 40csb 3682 . . . 4 class (𝑛 Mat 𝑟) / 𝑎(Poly1𝑎) / 𝑞(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))))
426, 14, 41cmpt 4863 . . 3 class (𝑚 ∈ (Base‘(𝑛 Mat (Poly1𝑟))) ↦ (𝑛 Mat 𝑟) / 𝑎(Poly1𝑎) / 𝑞(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎))))))
432, 3, 4, 5, 42cmpt2 6795 . 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat (Poly1𝑟))) ↦ (𝑛 Mat 𝑟) / 𝑎(Poly1𝑎) / 𝑞(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1𝑎)))))))
441, 43wceq 1631 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  20820
 Copyright terms: Public domain W3C validator