dmatval

Description: The set of N x N diagonal matrices over (a ring) R . (Contributed by AV, 8-Dec-2019)

	Ref	Expression
Hypotheses	dmatval.a	$⊢ A = N Mat R$
	dmatval.b	$⊢ B = {Base}_{A}$
	dmatval.0	$⊢ \underset{˙}{0} = 0_{R}$
	dmatval.d	$⊢ D = N DMat R$
Assertion	dmatval	$⊢ (N \in Fin \land R \in V) \to D = \{m \in B \| \forall i \in N \forall j \in N (i \neq j \to i m j = \underset{˙}{0})\}$

Proof

Step	Hyp	Ref	Expression
1		dmatval.a	$⊢ A = N Mat R$
2		dmatval.b	$⊢ B = {Base}_{A}$
3		dmatval.0	$⊢ \underset{˙}{0} = 0_{R}$
4		dmatval.d	$⊢ D = N DMat R$
5		df-dmat	$⊢ DMat = (n \in Fin, r \in V ⟼ \{m \in {Base}_{(n Mat r)} \| \forall i \in n \forall j \in n (i \neq j \to i m j = 0_{r})\})$
6	5	a1i	$⊢ (N \in Fin \land R \in V) \to DMat = (n \in Fin, r \in V ⟼ \{m \in {Base}_{(n Mat r)} \| \forall i \in n \forall j \in n (i \neq j \to i m j = 0_{r})\})$
7		oveq12	$⊢ (n = N \land r = R) \to n Mat r = N Mat R$
8	7	fveq2d	$⊢ (n = N \land r = R) \to {Base}_{(n Mat r)} = {Base}_{(N Mat R)}$
9	1	fveq2i	$⊢ {Base}_{A} = {Base}_{(N Mat R)}$
10	2 9	eqtri	$⊢ B = {Base}_{(N Mat R)}$
11	8 10	eqtr4di	$⊢ (n = N \land r = R) \to {Base}_{(n Mat r)} = B$
12		simpl	$⊢ (n = N \land r = R) \to n = N$
13		fveq2	$⊢ r = R \to 0_{r} = 0_{R}$
14	13 3	eqtr4di	$⊢ r = R \to 0_{r} = \underset{˙}{0}$
15	14	adantl	$⊢ (n = N \land r = R) \to 0_{r} = \underset{˙}{0}$
16	15	eqeq2d	$⊢ (n = N \land r = R) \to (i m j = 0_{r} \leftrightarrow i m j = \underset{˙}{0})$
17	16	imbi2d	$⊢ (n = N \land r = R) \to ((i \neq j \to i m j = 0_{r}) \leftrightarrow (i \neq j \to i m j = \underset{˙}{0}))$
18	12 17	raleqbidv	$⊢ (n = N \land r = R) \to (\forall j \in n (i \neq j \to i m j = 0_{r}) \leftrightarrow \forall j \in N (i \neq j \to i m j = \underset{˙}{0}))$
19	12 18	raleqbidv	$⊢ (n = N \land r = R) \to (\forall i \in n \forall j \in n (i \neq j \to i m j = 0_{r}) \leftrightarrow \forall i \in N \forall j \in N (i \neq j \to i m j = \underset{˙}{0}))$
20	11 19	rabeqbidv	$⊢ (n = N \land r = R) \to \{m \in {Base}_{(n Mat r)} \| \forall i \in n \forall j \in n (i \neq j \to i m j = 0_{r})\} = \{m \in B \| \forall i \in N \forall j \in N (i \neq j \to i m j = \underset{˙}{0})\}$
21	20	adantl	$⊢ ((N \in Fin \land R \in V) \land (n = N \land r = R)) \to \{m \in {Base}_{(n Mat r)} \| \forall i \in n \forall j \in n (i \neq j \to i m j = 0_{r})\} = \{m \in B \| \forall i \in N \forall j \in N (i \neq j \to i m j = \underset{˙}{0})\}$
22		simpl	$⊢ (N \in Fin \land R \in V) \to N \in Fin$
23		elex	$⊢ R \in V \to R \in V$
24	23	adantl	$⊢ (N \in Fin \land R \in V) \to R \in V$
25	2	fvexi	$⊢ B \in V$
26		rabexg	$⊢ B \in V \to \{m \in B \| \forall i \in N \forall j \in N (i \neq j \to i m j = \underset{˙}{0})\} \in V$
27	25 26	mp1i	$⊢ (N \in Fin \land R \in V) \to \{m \in B \| \forall i \in N \forall j \in N (i \neq j \to i m j = \underset{˙}{0})\} \in V$
28	6 21 22 24 27	ovmpod	$⊢ (N \in Fin \land R \in V) \to N DMat R = \{m \in B \| \forall i \in N \forall j \in N (i \neq j \to i m j = \underset{˙}{0})\}$
29	4 28	eqtrid	$⊢ (N \in Fin \land R \in V) \to D = \{m \in B \| \forall i \in N \forall j \in N (i \neq j \to i m j = \underset{˙}{0})\}$

Metamath Proof Explorer

Theorem dmatval

Proof