Metamath Proof Explorer

Definition df-dmat

Description: Define the set of n x n diagonal (square) matrices over a set (usually a ring) r, see definition in Roman p. 4 or Definition 3.12 in Hefferon p. 240. (Contributed by AV, 8-Dec-2019)

Ref Expression
Assertion df-dmat 
|- DMat = ( n e. Fin , r e. _V |-> { m e. ( Base ` ( n Mat r ) ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdmat 
 |-  DMat
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 vi 
 |-  i
13 vj 
 |-  j
14 12 cv 
 |-  i
15 13 cv 
 |-  j
16 14 15 wne 
 |-  i =/= j
17 5 cv 
 |-  m
18 14 15 17 co 
 |-  ( i m j )
19 c0g 
 |-  0g
20 9 19 cfv 
 |-  ( 0g ` r )
21 18 20 wceq 
 |-  ( i m j ) = ( 0g ` r )
22 16 21 wi 
 |-  ( i =/= j -> ( i m j ) = ( 0g ` r ) )
23 22 13 7 wral 
 |-  A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) )
24 23 12 7 wral 
 |-  A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) )
25 24 5 11 crab 
 |-  { m e. ( Base ` ( n Mat r ) ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) }
26 1 3 2 4 25 cmpo 
 |-  ( n e. Fin , r e. _V |-> { m e. ( Base ` ( n Mat r ) ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } )
27 0 26 wceq 
 |-  DMat = ( n e. Fin , r e. _V |-> { m e. ( Base ` ( n Mat r ) ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } )