Definition df-dmatalt 42187

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

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

Detailed syntax breakdown of Definition df-dmatalt

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

This definition is referenced by:  dmatALTval  42189