Definition df-scmat

Description: Define the algebra of n x n scalar matrices over a set (usually a ring) r, see definition in Connell p. 57: "Ascalar 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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cscmat	|- ScMat
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		vm	|- m
11		cbs	|- Base
12	9	cv	|- a
13	12 11	cfv	|- ( Base ` a )
14		vc	|- c
15	7 11	cfv	|- ( Base ` r )
16	10	cv	|- m
17	14	cv	|- c
18		cvsca	|- .s
19	12 18	cfv	|- ( .s ` a )
20		cur	|- 1r
21	12 20	cfv	|- ( 1r ` a )
22	17 21 19	co	|- ( c ( .s ` a ) ( 1r ` a ) )
23	16 22	wceq	|- m = ( c ( .s ` a ) ( 1r ` a ) )
24	23 14 15	wrex	|- E. c e. ( Base ` r ) m = ( c ( .s ` a ) ( 1r ` a ) )
25	24 10 13	crab	|- { m e. ( Base ` a ) | E. c e. ( Base ` r ) m = ( c ( .s ` a ) ( 1r ` a ) ) }
26	9 8 25	csb	|- [_ ( n Mat r ) / a ]_ { m e. ( Base ` a ) | E. c e. ( Base ` r ) m = ( c ( .s ` a ) ( 1r ` a ) ) }
27	1 3 2 4 26	cmpo	|- ( 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 ) ) } )
28	0 27	wceq	|- 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 ) ) } )