Definition df-dmat

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)

	Ref	Expression
Assertion	df-dmat	$$⊢\mathrm{DMat}=\left(n\in \mathrm{Fin},r\in \mathrm{V}⟼\left\{m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}|\forall i\in n\forall j\in n\left(i\ne j\to imj=0_r\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdmat	$$class\mathrm{DMat}$$
1		vn	$$setvarn$$
2		cfn	$$class\mathrm{Fin}$$
3		vr	$$setvarr$$
4		cvv	$$class\mathrm{V}$$
5		vm	$$setvarm$$
6		cbs	$$class\mathrm{Base}$$
7	1	cv	$$setvarn$$
8		cmat	$$class\mathrm{Mat}$$
9	3	cv	$$setvarr$$
10	7 9 8	co	$$class\left(n\mathrm{Mat}r\right)$$
11	10 6	cfv	$$class{\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}$$
12		vi	$$setvari$$
13		vj	$$setvarj$$
14	12	cv	$$setvari$$
15	13	cv	$$setvarj$$
16	14 15	wne	$$wffi\ne j$$
17	5	cv	$$setvarm$$
18	14 15 17	co	$$class\left(imj\right)$$
19		c0g	$$class{0}_{𝑔}$$
20	9 19	cfv	$$class{0}_r$$
21	18 20	wceq	$$wffimj=0_r$$
22	16 21	wi	$$wff\left(i\ne j\to imj=0_r\right)$$
23	22 13 7	wral	$$wff\forall j\in n\left(i\ne j\to imj=0_r\right)$$
24	23 12 7	wral	$$wff\forall i\in n\forall j\in n\left(i\ne j\to imj=0_r\right)$$
25	24 5 11	crab	$$class\left\{m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}|\forall i\in n\forall j\in n\left(i\ne j\to imj=0_r\right)\right\}$$
26	1 3 2 4 25	cmpo	$$class\left(n\in \mathrm{Fin},r\in \mathrm{V}⟼\left\{m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}|\forall i\in n\forall j\in n\left(i\ne j\to imj=0_r\right)\right\}\right)$$
27	0 26	wceq	$$wff\mathrm{DMat}=\left(n\in \mathrm{Fin},r\in \mathrm{V}⟼\left\{m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}|\forall i\in n\forall j\in n\left(i\ne j\to imj=0_r\right)\right\}\right)$$