Definition df-dmat 20296

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.)

Assertion

Ref	Expression
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 ) ) } )

Distinct variable group:   i, j, m, n, r

Detailed syntax breakdown of Definition df-dmat

Step	Hyp	Ref	Expression
1		cdmat 20294	. 2 class DMat
2		vn	. . 3 setvar n
3		vr	. . 3 setvar r
4		cfn 7955	. . 3 class Fin
5		cvv 3200	. . 3 class _V
6		vi	. . . . . . . . 9 setvar i
7	6	cv 1482	. . . . . . . 8 class i
8		vj	. . . . . . . . 9 setvar j
9	8	cv 1482	. . . . . . . 8 class j
10	7, 9	wne 2794	. . . . . . 7 wff i =/= j
11		vm	. . . . . . . . . 10 setvar m
12	11	cv 1482	. . . . . . . . 9 class m
13	7, 9, 12	co 6650	. . . . . . . 8 class ( i m j )
14	3	cv 1482	. . . . . . . . 9 class r
15		c0g 16100	. . . . . . . . 9 class 0g
16	14, 15	cfv 5888	. . . . . . . 8 class ( 0g ` r )
17	13, 16	wceq 1483	. . . . . . 7 wff ( i m j ) = ( 0g ` r )
18	10, 17	wi 4	. . . . . 6 wff ( i =/= j -> ( i m j ) = ( 0g ` r ) )
19	2	cv 1482	. . . . . 6 class n
20	18, 8, 19	wral 2912	. . . . 5 wff A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) )
21	20, 6, 19	wral 2912	. . . 4 wff A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) )
22		cmat 20213	. . . . . 6 class Mat
23	19, 14, 22	co 6650	. . . . 5 class ( n Mat r )
24		cbs 15857	. . . . 5 class Base
25	23, 24	cfv 5888	. . . 4 class ( Base ` ( n Mat r ) )
26	21, 11, 25	crab 2916	. . 3 class { m e. ( Base ` ( n Mat r ) ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) }
27	2, 3, 4, 5, 26	cmpt2 6652	. 2 class ( 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 ) ) } )
28	1, 27	wceq 1483	1 wff 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 ) ) } )

This definition is referenced by:  dmatval  20298