Metamath Proof Explorer

Definition df-pm2mp

Description: Transformation of a polynomial matrix (over a ring) into a polynomial over matrices (over the same ring). (Contributed by AV, 5-Dec-2019)

Ref Expression
Assertion df-pm2mp 
|- pMatToMatPoly = ( n e. Fin , r e. _V |-> ( m e. ( Base ` ( n Mat ( Poly1 ` r ) ) ) |-> [_ ( n Mat r ) / a ]_ [_ ( Poly1 ` a ) / q ]_ ( q gsum ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k ( .g ` ( mulGrp ` q ) ) ( var1 ` a ) ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpm2mp 
 |-  pMatToMatPoly
1 vn 
 |-  n
2 cfn 
 |-  Fin
3 vr 
 |-  r
4 cvv 
 |-  _V
5 vm 
 |-  m
6 cbs 
 |-  Base
7 1 cv 
 |-  n
8 cmat 
 |-  Mat
9 cpl1 
 |-  Poly1
10 3 cv 
 |-  r
11 10 9 cfv 
 |-  ( Poly1 ` r )
12 7 11 8 co 
 |-  ( n Mat ( Poly1 ` r ) )
13 12 6 cfv 
 |-  ( Base ` ( n Mat ( Poly1 ` r ) ) )
14 7 10 8 co 
 |-  ( n Mat r )
15 va 
 |-  a
16 15 cv 
 |-  a
17 16 9 cfv 
 |-  ( Poly1 ` a )
18 vq 
 |-  q
19 18 cv 
 |-  q
20 cgsu 
 |-  gsum
21 vk 
 |-  k
22 cn0 
 |-  NN0
23 5 cv 
 |-  m
24 cdecpmat 
 |-  decompPMat
25 21 cv 
 |-  k
26 23 25 24 co 
 |-  ( m decompPMat k )
27 cvsca 
 |-  .s
28 19 27 cfv 
 |-  ( .s ` q )
29 cmg 
 |-  .g
30 cmgp 
 |-  mulGrp
31 19 30 cfv 
 |-  ( mulGrp ` q )
32 31 29 cfv 
 |-  ( .g ` ( mulGrp ` q ) )
33 cv1 
 |-  var1
34 16 33 cfv 
 |-  ( var1 ` a )
35 25 34 32 co 
 |-  ( k ( .g ` ( mulGrp ` q ) ) ( var1 ` a ) )
36 26 35 28 co 
 |-  ( ( m decompPMat k ) ( .s ` q ) ( k ( .g ` ( mulGrp ` q ) ) ( var1 ` a ) ) )
37 21 22 36 cmpt 
 |-  ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k ( .g ` ( mulGrp ` q ) ) ( var1 ` a ) ) ) )
38 19 37 20 co 
 |-  ( q gsum ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k ( .g ` ( mulGrp ` q ) ) ( var1 ` a ) ) ) ) )
39 18 17 38 csb 
 |-  [_ ( Poly1 ` a ) / q ]_ ( q gsum ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k ( .g ` ( mulGrp ` q ) ) ( var1 ` a ) ) ) ) )
40 15 14 39 csb 
 |-  [_ ( n Mat r ) / a ]_ [_ ( Poly1 ` a ) / q ]_ ( q gsum ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k ( .g ` ( mulGrp ` q ) ) ( var1 ` a ) ) ) ) )
41 5 13 40 cmpt 
 |-  ( m e. ( Base ` ( n Mat ( Poly1 ` r ) ) ) |-> [_ ( n Mat r ) / a ]_ [_ ( Poly1 ` a ) / q ]_ ( q gsum ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k ( .g ` ( mulGrp ` q ) ) ( var1 ` a ) ) ) ) ) )
42 1 3 2 4 41 cmpo 
 |-  ( n e. Fin , r e. _V |-> ( m e. ( Base ` ( n Mat ( Poly1 ` r ) ) ) |-> [_ ( n Mat r ) / a ]_ [_ ( Poly1 ` a ) / q ]_ ( q gsum ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k ( .g ` ( mulGrp ` q ) ) ( var1 ` a ) ) ) ) ) ) )
43 0 42 wceq 
 |-  pMatToMatPoly = ( n e. Fin , r e. _V |-> ( m e. ( Base ` ( n Mat ( Poly1 ` r ) ) ) |-> [_ ( n Mat r ) / a ]_ [_ ( Poly1 ` a ) / q ]_ ( q gsum ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k ( .g ` ( mulGrp ` q ) ) ( var1 ` a ) ) ) ) ) ) )