Metamath Proof Explorer

Definition df-cpmat

Description: The set of all constant polynomial matrices, which are all matrices whose entries are constant polynomials (or "scalar polynomials", see ply1sclf ). (Contributed by AV, 15-Nov-2019)

Ref Expression
Assertion df-cpmat 
|- ConstPolyMat = ( n e. Fin , r e. _V |-> { m e. ( Base ` ( n Mat ( Poly1 ` r ) ) ) | A. i e. n A. j e. n A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccpmat 
 |-  ConstPolyMat
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 vi 
 |-  i
15 vj 
 |-  j
16 vk 
 |-  k
17 cn 
 |-  NN
18 cco1 
 |-  coe1
19 14 cv 
 |-  i
20 5 cv 
 |-  m
21 15 cv 
 |-  j
22 19 21 20 co 
 |-  ( i m j )
23 22 18 cfv 
 |-  ( coe1 ` ( i m j ) )
24 16 cv 
 |-  k
25 24 23 cfv 
 |-  ( ( coe1 ` ( i m j ) ) ` k )
26 c0g 
 |-  0g
27 10 26 cfv 
 |-  ( 0g ` r )
28 25 27 wceq 
 |-  ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r )
29 28 16 17 wral 
 |-  A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r )
30 29 15 7 wral 
 |-  A. j e. n A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r )
31 30 14 7 wral 
 |-  A. i e. n A. j e. n A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r )
32 31 5 13 crab 
 |-  { m e. ( Base ` ( n Mat ( Poly1 ` r ) ) ) | A. i e. n A. j e. n A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) }
33 1 3 2 4 32 cmpo 
 |-  ( n e. Fin , r e. _V |-> { m e. ( Base ` ( n Mat ( Poly1 ` r ) ) ) | A. i e. n A. j e. n A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) } )
34 0 33 wceq 
 |-  ConstPolyMat = ( n e. Fin , r e. _V |-> { m e. ( Base ` ( n Mat ( Poly1 ` r ) ) ) | A. i e. n A. j e. n A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) } )