Theorem dmatALTbasel

Description: An element of the base set of the algebra of N x N diagonal matrices over a ring R , i.e. an N x N diagonal matrix over the ring R . (Contributed by AV, 8-Dec-2019)

	Ref	Expression
Hypotheses	dmatALTval.a	$$⊢A=N\mathrm{Mat}R$$
	dmatALTval.b	$$⊢B={\mathrm{Base}}_A$$
	dmatALTval.0	$$⊢\underset{\dot{}}{0}=0_R$$
	dmatALTval.d	$$⊢D=N\mathrm{DMatALT}R$$
Assertion	dmatALTbasel	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)\to \left(M\in {\mathrm{Base}}_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		dmatALTval.a	$$⊢A=N\mathrm{Mat}R$$
2		dmatALTval.b	$$⊢B={\mathrm{Base}}_A$$
3		dmatALTval.0	$$⊢\underset{\dot{}}{0}=0_R$$
4		dmatALTval.d	$$⊢D=N\mathrm{DMatALT}R$$
5	1 2 3 4	dmatALTbas	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)\to {\mathrm{Base}}_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 \mathrm{V}\right)\to \left(M\in {\mathrm{Base}}_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 \mathrm{V}\right)\to \left(M\in {\mathrm{Base}}_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)$$