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	$$⊢\mathrm{ScMat}=\left(n\in \mathrm{Fin},r\in \mathrm{V}⟼⦋\left(n\mathrm{Mat}r\right)/a⦌\left\{m\in {\mathrm{Base}}_a|\exists c\in {\mathrm{Base}}_{r}m=c{\cdot }_a{1}_a\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cscmat	$$class\mathrm{ScMat}$$
1		vn	$$setvarn$$
2		cfn	$$class\mathrm{Fin}$$
3		vr	$$setvarr$$
4		cvv	$$class\mathrm{V}$$
5	1	cv	$$setvarn$$
6		cmat	$$class\mathrm{Mat}$$
7	3	cv	$$setvarr$$
8	5 7 6	co	$$class\left(n\mathrm{Mat}r\right)$$
9		va	$$setvara$$
10		vm	$$setvarm$$
11		cbs	$$class\mathrm{Base}$$
12	9	cv	$$setvara$$
13	12 11	cfv	$$class{\mathrm{Base}}_a$$
14		vc	$$setvarc$$
15	7 11	cfv	$$class{\mathrm{Base}}_r$$
16	10	cv	$$setvarm$$
17	14	cv	$$setvarc$$
18		cvsca	$$class{\cdot }_{𝑠}$$
19	12 18	cfv	$$class{\cdot }_a$$
20		cur	$$class{1}_r$$
21	12 20	cfv	$$class{1}_a$$
22	17 21 19	co	$$class\left(c{\cdot }_a{1}_a\right)$$
23	16 22	wceq	$$wffm=c{\cdot }_a{1}_a$$
24	23 14 15	wrex	$$wff\exists c\in {\mathrm{Base}}_{r}m=c{\cdot }_a{1}_a$$
25	24 10 13	crab	$$class\left\{m\in {\mathrm{Base}}_a|\exists c\in {\mathrm{Base}}_{r}m=c{\cdot }_a{1}_a\right\}$$
26	9 8 25	csb	$$class⦋\left(n\mathrm{Mat}r\right)/a⦌\left\{m\in {\mathrm{Base}}_a|\exists c\in {\mathrm{Base}}_{r}m=c{\cdot }_a{1}_a\right\}$$
27	1 3 2 4 26	cmpo	$$class\left(n\in \mathrm{Fin},r\in \mathrm{V}⟼⦋\left(n\mathrm{Mat}r\right)/a⦌\left\{m\in {\mathrm{Base}}_a|\exists c\in {\mathrm{Base}}_{r}m=c{\cdot }_a{1}_a\right\}\right)$$
28	0 27	wceq	$$wff\mathrm{ScMat}=\left(n\in \mathrm{Fin},r\in \mathrm{V}⟼⦋\left(n\mathrm{Mat}r\right)/a⦌\left\{m\in {\mathrm{Base}}_a|\exists c\in {\mathrm{Base}}_{r}m=c{\cdot }_a{1}_a\right\}\right)$$