df-dmatalt

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-dmatalt	$⊢ DMatALT = (n \in Fin, r \in V ⟼ ⦋ (n Mat r) / a ⦌ (a ↾_{𝑠} \{m \in {Base}_{a} \| \forall i \in n \forall j \in n (i \neq j \to i m j = 0_{r})\}))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdmatalt	$class DMatALT$
1		vn	$setvar n$
2		cfn	$class Fin$
3		vr	$setvar r$
4		cvv	$class V$
5	1	cv	$setvar n$
6		cmat	$class Mat$
7	3	cv	$setvar r$
8	5 7 6	co	$class (n Mat r)$
9		va	$setvar a$
10	9	cv	$setvar a$
11		cress	$class ↾_{𝑠}$
12		vm	$setvar m$
13		cbs	$class Base$
14	10 13	cfv	$class {Base}_{a}$
15		vi	$setvar i$
16		vj	$setvar j$
17	15	cv	$setvar i$
18	16	cv	$setvar j$
19	17 18	wne	$wff i \neq j$
20	12	cv	$setvar m$
21	17 18 20	co	$class (i m j)$
22		c0g	$class 0_{𝑔}$
23	7 22	cfv	$class 0_{r}$
24	21 23	wceq	$wff i m j = 0_{r}$
25	19 24	wi	$wff (i \neq j \to i m j = 0_{r})$
26	25 16 5	wral	$wff \forall j \in n (i \neq j \to i m j = 0_{r})$
27	26 15 5	wral	$wff \forall i \in n \forall j \in n (i \neq j \to i m j = 0_{r})$
28	27 12 14	crab	$class \{m \in {Base}_{a} \| \forall i \in n \forall j \in n (i \neq j \to i m j = 0_{r})\}$
29	10 28 11	co	$class (a ↾_{𝑠} \{m \in {Base}_{a} \| \forall i \in n \forall j \in n (i \neq j \to i m j = 0_{r})\})$
30	9 8 29	csb	$class ⦋ (n Mat r) / a ⦌ (a ↾_{𝑠} \{m \in {Base}_{a} \| \forall i \in n \forall j \in n (i \neq j \to i m j = 0_{r})\})$
31	1 3 2 4 30	cmpo	$class (n \in Fin, r \in V ⟼ ⦋ (n Mat r) / a ⦌ (a ↾_{𝑠} \{m \in {Base}_{a} \| \forall i \in n \forall j \in n (i \neq j \to i m j = 0_{r})\}))$
32	0 31	wceq	$wff DMatALT = (n \in Fin, r \in V ⟼ ⦋ (n Mat r) / a ⦌ (a ↾_{𝑠} \{m \in {Base}_{a} \| \forall i \in n \forall j \in n (i \neq j \to i m j = 0_{r})\}))$

Metamath Proof Explorer

Definition df-dmatalt

Detailed syntax breakdown