Definition df-scmatalt 42188

Description: Define the algebra of n x n scalar matrices over a set (usually a ring) r, see definition in [Connell] p. 57: "A scalar matrix is a diagonal matrix for which all the diagonal terms are equal, i.e., a matrix of the form cI_n";. (Contributed by AV, 8-Dec-2019.)

Assertion

Ref	Expression
df-scmatalt	|- ScMatALT = ( n e. Fin , r e. _V |-> [_ ( n Mat r ) / a ]_ ( a ↾s { m e. ( Base ` a ) | E. c e. ( Base ` r ) A. i e. n A. j e. n ( i m j ) = if ( i = j , c , ( 0g ` r ) ) } ) )

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

Detailed syntax breakdown of Definition df-scmatalt

Step	Hyp	Ref	Expression
1		cscmatalt 42186	. 2 class ScMatALT
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	. . . . . . . . . . . 12 setvar i
13	12	cv 1482	. . . . . . . . . . 11 class i
14		vj	. . . . . . . . . . . 12 setvar j
15	14	cv 1482	. . . . . . . . . . 11 class j
16		vm	. . . . . . . . . . . 12 setvar m
17	16	cv 1482	. . . . . . . . . . 11 class m
18	13, 15, 17	co 6650	. . . . . . . . . 10 class ( i m j )
19	12, 14	weq 1874	. . . . . . . . . . 11 wff i = j
20		vc	. . . . . . . . . . . 12 setvar c
21	20	cv 1482	. . . . . . . . . . 11 class c
22		c0g 16100	. . . . . . . . . . . 12 class 0g
23	8, 22	cfv 5888	. . . . . . . . . . 11 class ( 0g ` r )
24	19, 21, 23	cif 4086	. . . . . . . . . 10 class if ( i = j , c , ( 0g ` r ) )
25	18, 24	wceq 1483	. . . . . . . . 9 wff ( i m j ) = if ( i = j , c , ( 0g ` r ) )
26	25, 14, 7	wral 2912	. . . . . . . 8 wff A. j e. n ( i m j ) = if ( i = j , c , ( 0g ` r ) )
27	26, 12, 7	wral 2912	. . . . . . 7 wff A. i e. n A. j e. n ( i m j ) = if ( i = j , c , ( 0g ` r ) )
28		cbs 15857	. . . . . . . 8 class Base
29	8, 28	cfv 5888	. . . . . . 7 class ( Base ` r )
30	27, 20, 29	wrex 2913	. . . . . 6 wff E. c e. ( Base ` r ) A. i e. n A. j e. n ( i m j ) = if ( i = j , c , ( 0g ` r ) )
31	11, 28	cfv 5888	. . . . . 6 class ( Base ` a )
32	30, 16, 31	crab 2916	. . . . 5 class { m e. ( Base ` a ) | E. c e. ( Base ` r ) A. i e. n A. j e. n ( i m j ) = if ( i = j , c , ( 0g ` r ) ) }
33		cress 15858	. . . . 5 class ↾s
34	11, 32, 33	co 6650	. . . 4 class ( a ↾s { m e. ( Base ` a ) | E. c e. ( Base ` r ) A. i e. n A. j e. n ( i m j ) = if ( i = j , c , ( 0g ` r ) ) } )
35	6, 10, 34	csb 3533	. . 3 class [_ ( n Mat r ) / a ]_ ( a ↾s { m e. ( Base ` a ) | E. c e. ( Base ` r ) A. i e. n A. j e. n ( i m j ) = if ( i = j , c , ( 0g ` r ) ) } )
36	2, 3, 4, 5, 35	cmpt2 6652	. 2 class ( n e. Fin , r e. _V |-> [_ ( n Mat r ) / a ]_ ( a ↾s { m e. ( Base ` a ) | E. c e. ( Base ` r ) A. i e. n A. j e. n ( i m j ) = if ( i = j , c , ( 0g ` r ) ) } ) )
37	1, 36	wceq 1483	1 wff ScMatALT = ( n e. Fin , r e. _V |-> [_ ( n Mat r ) / a ]_ ( a ↾s { m e. ( Base ` a ) | E. c e. ( Base ` r ) A. i e. n A. j e. n ( i m j ) = if ( i = j , c , ( 0g ` r ) ) } ) )

This definition is referenced by: (None)