Theorem dmatel

Description: A N x N diagonal matrix over (a ring) R . (Contributed by AV, 18-Dec-2019)

	Ref	Expression
Hypotheses	dmatval.a	$$⊢A=N\mathrm{Mat}R$$
	dmatval.b	$$⊢B={\mathrm{Base}}_A$$
	dmatval.0	$$⊢\underset{\dot{}}{0}=0_R$$
	dmatval.d	$$⊢D=N\mathrm{DMat}R$$
Assertion	dmatel	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to \left(M\in D\leftrightarrow \left(M\in B\wedge \forall i\in N\forall j\in N\left(i\ne j\to iMj=\underset{\dot{}}{0}\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dmatval.a	$$⊢A=N\mathrm{Mat}R$$
2		dmatval.b	$$⊢B={\mathrm{Base}}_A$$
3		dmatval.0	$$⊢\underset{\dot{}}{0}=0_R$$
4		dmatval.d	$$⊢D=N\mathrm{DMat}R$$
5	1 2 3 4	dmatval	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to D=\left\{m\in B|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}$$
6	5	eleq2d	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to \left(M\in D\leftrightarrow M\in \left\{m\in B|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}\right)$$
7		oveq	$$⊢m=M\to imj=iMj$$
8	7	eqeq1d	$$⊢m=M\to \left(imj=\underset{\dot{}}{0}\leftrightarrow iMj=\underset{\dot{}}{0}\right)$$
9	8	imbi2d	$$⊢m=M\to \left(\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\leftrightarrow \left(i\ne j\to iMj=\underset{\dot{}}{0}\right)\right)$$
10	9	2ralbidv	$$⊢m=M\to \left(\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\leftrightarrow \forall i\in N\forall j\in N\left(i\ne j\to iMj=\underset{\dot{}}{0}\right)\right)$$
11	10	elrab	$$⊢M\in \left\{m\in B|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}\leftrightarrow \left(M\in B\wedge \forall i\in N\forall j\in N\left(i\ne j\to iMj=\underset{\dot{}}{0}\right)\right)$$
12	6 11	bitrdi	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to \left(M\in D\leftrightarrow \left(M\in B\wedge \forall i\in N\forall j\in N\left(i\ne j\to iMj=\underset{\dot{}}{0}\right)\right)\right)$$