Metamath Proof Explorer

Definition df-cpmat2mat

Description: Transformation of a constant polynomial matrix (over a ring) into a matrix over the corresponding ring. Since this function is the inverse function of matToPolyMat , see m2cpminv , it is also called "inverse matrix transformation" in the following. (Contributed by AV, 14-Dec-2019)

Ref Expression
Assertion df-cpmat2mat 
|- cPolyMatToMat = ( n e. Fin , r e. _V |-> ( m e. ( n ConstPolyMat r ) |-> ( x e. n , y e. n |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccpmat2mat 
 |-  cPolyMatToMat
1 vn 
 |-  n
2 cfn 
 |-  Fin
3 vr 
 |-  r
4 cvv 
 |-  _V
5 vm 
 |-  m
6 1 cv 
 |-  n
7 ccpmat 
 |-  ConstPolyMat
8 3 cv 
 |-  r
9 6 8 7 co 
 |-  ( n ConstPolyMat r )
10 vx 
 |-  x
11 vy 
 |-  y
12 cco1 
 |-  coe1
13 10 cv 
 |-  x
14 5 cv 
 |-  m
15 11 cv 
 |-  y
16 13 15 14 co 
 |-  ( x m y )
17 16 12 cfv 
 |-  ( coe1 ` ( x m y ) )
18 cc0 
 |-  0
19 18 17 cfv 
 |-  ( ( coe1 ` ( x m y ) ) ` 0 )
20 10 11 6 6 19 cmpo 
 |-  ( x e. n , y e. n |-> ( ( coe1 ` ( x m y ) ) ` 0 ) )
21 5 9 20 cmpt 
 |-  ( m e. ( n ConstPolyMat r ) |-> ( x e. n , y e. n |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) )
22 1 3 2 4 21 cmpo 
 |-  ( n e. Fin , r e. _V |-> ( m e. ( n ConstPolyMat r ) |-> ( x e. n , y e. n |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) )
23 0 22 wceq 
 |-  cPolyMatToMat = ( n e. Fin , r e. _V |-> ( m e. ( n ConstPolyMat r ) |-> ( x e. n , y e. n |-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) )