Metamath Proof Explorer

Definition df-dmatalt

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-dmatalt 
|- DMatALT = ( n e. Fin , r e. _V |-> [_ ( n Mat r ) / a ]_ ( a |`s { m e. ( Base ` a ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdmatalt 
 |-  DMatALT
1 vn 
 |-  n
2 cfn 
 |-  Fin
3 vr 
 |-  r
4 cvv 
 |-  _V
5 1 cv 
 |-  n
6 cmat 
 |-  Mat
7 3 cv 
 |-  r
8 5 7 6 co 
 |-  ( n Mat r )
9 va 
 |-  a
10 9 cv 
 |-  a
11 cress 
 |-  |`s
12 vm 
 |-  m
13 cbs 
 |-  Base
14 10 13 cfv 
 |-  ( Base ` a )
15 vi 
 |-  i
16 vj 
 |-  j
17 15 cv 
 |-  i
18 16 cv 
 |-  j
19 17 18 wne 
 |-  i =/= j
20 12 cv 
 |-  m
21 17 18 20 co 
 |-  ( i m j )
22 c0g 
 |-  0g
23 7 22 cfv 
 |-  ( 0g ` r )
24 21 23 wceq 
 |-  ( i m j ) = ( 0g ` r )
25 19 24 wi 
 |-  ( i =/= j -> ( i m j ) = ( 0g ` r ) )
26 25 16 5 wral 
 |-  A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) )
27 26 15 5 wral 
 |-  A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) )
28 27 12 14 crab 
 |-  { m e. ( Base ` a ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) }
29 10 28 11 co 
 |-  ( a |`s { m e. ( Base ` a ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } )
30 9 8 29 csb 
 |-  [_ ( n Mat r ) / a ]_ ( a |`s { m e. ( Base ` a ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } )
31 1 3 2 4 30 cmpo 
 |-  ( n e. Fin , r e. _V |-> [_ ( n Mat r ) / a ]_ ( a |`s { m e. ( Base ` a ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } ) )
32 0 31 wceq 
 |-  DMatALT = ( n e. Fin , r e. _V |-> [_ ( n Mat r ) / a ]_ ( a |`s { m e. ( Base ` a ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } ) )