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 22158
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 22157 . 2 class pMatToMatPoly
2 vn . . 3 setvar ๐‘›
3 vr . . 3 setvar ๐‘Ÿ
4 cfn 8886 . . 3 class Fin
5 cvv 3444 . . 3 class V
6 vm . . . 4 setvar ๐‘š
72cv 1541 . . . . . 6 class ๐‘›
83cv 1541 . . . . . . 7 class ๐‘Ÿ
9 cpl1 21564 . . . . . . 7 class Poly1
108, 9cfv 6497 . . . . . 6 class (Poly1โ€˜๐‘Ÿ)
11 cmat 21770 . . . . . 6 class Mat
127, 10, 11co 7358 . . . . 5 class (๐‘› Mat (Poly1โ€˜๐‘Ÿ))
13 cbs 17088 . . . . 5 class Base
1412, 13cfv 6497 . . . 4 class (Baseโ€˜(๐‘› Mat (Poly1โ€˜๐‘Ÿ)))
15 va . . . . 5 setvar ๐‘Ž
167, 8, 11co 7358 . . . . 5 class (๐‘› Mat ๐‘Ÿ)
17 vq . . . . . 6 setvar ๐‘ž
1815cv 1541 . . . . . . 7 class ๐‘Ž
1918, 9cfv 6497 . . . . . 6 class (Poly1โ€˜๐‘Ž)
2017cv 1541 . . . . . . 7 class ๐‘ž
21 vk . . . . . . . 8 setvar ๐‘˜
22 cn0 12418 . . . . . . . 8 class โ„•0
236cv 1541 . . . . . . . . . 10 class ๐‘š
2421cv 1541 . . . . . . . . . 10 class ๐‘˜
25 cdecpmat 22127 . . . . . . . . . 10 class decompPMat
2623, 24, 25co 7358 . . . . . . . . 9 class (๐‘š decompPMat ๐‘˜)
27 cv1 21563 . . . . . . . . . . 11 class var1
2818, 27cfv 6497 . . . . . . . . . 10 class (var1โ€˜๐‘Ž)
29 cmgp 19901 . . . . . . . . . . . 12 class mulGrp
3020, 29cfv 6497 . . . . . . . . . . 11 class (mulGrpโ€˜๐‘ž)
31 cmg 18877 . . . . . . . . . . 11 class .g
3230, 31cfv 6497 . . . . . . . . . 10 class (.gโ€˜(mulGrpโ€˜๐‘ž))
3324, 28, 32co 7358 . . . . . . . . 9 class (๐‘˜(.gโ€˜(mulGrpโ€˜๐‘ž))(var1โ€˜๐‘Ž))
34 cvsca 17142 . . . . . . . . . 10 class ยท๐‘ 
3520, 34cfv 6497 . . . . . . . . 9 class ( ยท๐‘  โ€˜๐‘ž)
3626, 33, 35co 7358 . . . . . . . 8 class ((๐‘š decompPMat ๐‘˜)( ยท๐‘  โ€˜๐‘ž)(๐‘˜(.gโ€˜(mulGrpโ€˜๐‘ž))(var1โ€˜๐‘Ž)))
3721, 22, 36cmpt 5189 . . . . . . 7 class (๐‘˜ โˆˆ โ„•0 โ†ฆ ((๐‘š decompPMat ๐‘˜)( ยท๐‘  โ€˜๐‘ž)(๐‘˜(.gโ€˜(mulGrpโ€˜๐‘ž))(var1โ€˜๐‘Ž))))
38 cgsu 17327 . . . . . . 7 class ฮฃg
3920, 37, 38co 7358 . . . . . 6 class (๐‘ž ฮฃg (๐‘˜ โˆˆ โ„•0 โ†ฆ ((๐‘š decompPMat ๐‘˜)( ยท๐‘  โ€˜๐‘ž)(๐‘˜(.gโ€˜(mulGrpโ€˜๐‘ž))(var1โ€˜๐‘Ž)))))
4017, 19, 39csb 3856 . . . . 5 class โฆ‹(Poly1โ€˜๐‘Ž) / ๐‘žโฆŒ(๐‘ž ฮฃg (๐‘˜ โˆˆ โ„•0 โ†ฆ ((๐‘š decompPMat ๐‘˜)( ยท๐‘  โ€˜๐‘ž)(๐‘˜(.gโ€˜(mulGrpโ€˜๐‘ž))(var1โ€˜๐‘Ž)))))
4115, 16, 40csb 3856 . . . 4 class โฆ‹(๐‘› Mat ๐‘Ÿ) / ๐‘ŽโฆŒโฆ‹(Poly1โ€˜๐‘Ž) / ๐‘žโฆŒ(๐‘ž ฮฃg (๐‘˜ โˆˆ โ„•0 โ†ฆ ((๐‘š decompPMat ๐‘˜)( ยท๐‘  โ€˜๐‘ž)(๐‘˜(.gโ€˜(mulGrpโ€˜๐‘ž))(var1โ€˜๐‘Ž)))))
426, 14, 41cmpt 5189 . . 3 class (๐‘š โˆˆ (Baseโ€˜(๐‘› Mat (Poly1โ€˜๐‘Ÿ))) โ†ฆ โฆ‹(๐‘› Mat ๐‘Ÿ) / ๐‘ŽโฆŒโฆ‹(Poly1โ€˜๐‘Ž) / ๐‘žโฆŒ(๐‘ž ฮฃg (๐‘˜ โˆˆ โ„•0 โ†ฆ ((๐‘š decompPMat ๐‘˜)( ยท๐‘  โ€˜๐‘ž)(๐‘˜(.gโ€˜(mulGrpโ€˜๐‘ž))(var1โ€˜๐‘Ž))))))
432, 3, 4, 5, 42cmpo 7360 . 2 class (๐‘› โˆˆ Fin, ๐‘Ÿ โˆˆ V โ†ฆ (๐‘š โˆˆ (Baseโ€˜(๐‘› Mat (Poly1โ€˜๐‘Ÿ))) โ†ฆ โฆ‹(๐‘› Mat ๐‘Ÿ) / ๐‘ŽโฆŒโฆ‹(Poly1โ€˜๐‘Ž) / ๐‘žโฆŒ(๐‘ž ฮฃg (๐‘˜ โˆˆ โ„•0 โ†ฆ ((๐‘š decompPMat ๐‘˜)( ยท๐‘  โ€˜๐‘ž)(๐‘˜(.gโ€˜(mulGrpโ€˜๐‘ž))(var1โ€˜๐‘Ž)))))))
441, 43wceq 1542 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  22160
  Copyright terms: Public domain W3C validator