Metamath Proof Explorer

Definition df-mat2pmat

Description: Transformation of a matrix (over a ring) into a matrix over the corresponding polynomial ring. (Contributed by AV, 31-Jul-2019)

Ref Expression
Assertion df-mat2pmat 
|- matToPolyMat = ( n e. Fin , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( x e. n , y e. n |-> ( ( algSc ` ( Poly1 ` r ) ) ` ( x m y ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmat2pmat 
 |-  matToPolyMat
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 3 cv 
 |-  r
10 7 9 8 co 
 |-  ( n Mat r )
11 10 6 cfv 
 |-  ( Base ` ( n Mat r ) )
12 vx 
 |-  x
13 vy 
 |-  y
14 cascl 
 |-  algSc
15 cpl1 
 |-  Poly1
16 9 15 cfv 
 |-  ( Poly1 ` r )
17 16 14 cfv 
 |-  ( algSc ` ( Poly1 ` r ) )
18 12 cv 
 |-  x
19 5 cv 
 |-  m
20 13 cv 
 |-  y
21 18 20 19 co 
 |-  ( x m y )
22 21 17 cfv 
 |-  ( ( algSc ` ( Poly1 ` r ) ) ` ( x m y ) )
23 12 13 7 7 22 cmpo 
 |-  ( x e. n , y e. n |-> ( ( algSc ` ( Poly1 ` r ) ) ` ( x m y ) ) )
24 5 11 23 cmpt 
 |-  ( m e. ( Base ` ( n Mat r ) ) |-> ( x e. n , y e. n |-> ( ( algSc ` ( Poly1 ` r ) ) ` ( x m y ) ) ) )
25 1 3 2 4 24 cmpo 
 |-  ( n e. Fin , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( x e. n , y e. n |-> ( ( algSc ` ( Poly1 ` r ) ) ` ( x m y ) ) ) ) )
26 0 25 wceq 
 |-  matToPolyMat = ( n e. Fin , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( x e. n , y e. n |-> ( ( algSc ` ( Poly1 ` r ) ) ` ( x m y ) ) ) ) )