Definition df-scmat 20297

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-scmat	|- ScMat = ( n e. Fin , r e. _V |-> [_ ( n Mat r ) / a ]_ { m e. ( Base ` a ) | E. c e. ( Base ` r ) m = ( c ( .s ` a ) ( 1r ` a ) ) } )

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

Detailed syntax breakdown of Definition df-scmat

Step	Hyp	Ref	Expression
1		cscmat 20295	. 2 class ScMat
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		vm	. . . . . . . 8 setvar m
12	11	cv 1482	. . . . . . 7 class m
13		vc	. . . . . . . . 9 setvar c
14	13	cv 1482	. . . . . . . 8 class c
15	6	cv 1482	. . . . . . . . 9 class a
16		cur 18501	. . . . . . . . 9 class 1r
17	15, 16	cfv 5888	. . . . . . . 8 class ( 1r ` a )
18		cvsca 15945	. . . . . . . . 9 class .s
19	15, 18	cfv 5888	. . . . . . . 8 class ( .s ` a )
20	14, 17, 19	co 6650	. . . . . . 7 class ( c ( .s ` a ) ( 1r ` a ) )
21	12, 20	wceq 1483	. . . . . 6 wff m = ( c ( .s ` a ) ( 1r ` a ) )
22		cbs 15857	. . . . . . 7 class Base
23	8, 22	cfv 5888	. . . . . 6 class ( Base ` r )
24	21, 13, 23	wrex 2913	. . . . 5 wff E. c e. ( Base ` r ) m = ( c ( .s ` a ) ( 1r ` a ) )
25	15, 22	cfv 5888	. . . . 5 class ( Base ` a )
26	24, 11, 25	crab 2916	. . . 4 class { m e. ( Base ` a ) | E. c e. ( Base ` r ) m = ( c ( .s ` a ) ( 1r ` a ) ) }
27	6, 10, 26	csb 3533	. . 3 class [_ ( n Mat r ) / a ]_ { m e. ( Base ` a ) | E. c e. ( Base ` r ) m = ( c ( .s ` a ) ( 1r ` a ) ) }
28	2, 3, 4, 5, 27	cmpt2 6652	. 2 class ( n e. Fin , r e. _V |-> [_ ( n Mat r ) / a ]_ { m e. ( Base ` a ) | E. c e. ( Base ` r ) m = ( c ( .s ` a ) ( 1r ` a ) ) } )
29	1, 28	wceq 1483	1 wff ScMat = ( n e. Fin , r e. _V |-> [_ ( n Mat r ) / a ]_ { m e. ( Base ` a ) | E. c e. ( Base ` r ) m = ( c ( .s ` a ) ( 1r ` a ) ) } )

This definition is referenced by:  scmatval  20310