Theorem dmatmat

Description: An N x N diagonal matrix over (the ring) R is an N x N matrix over (the 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	dmatmat	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to \left(M\in D\to M\in B\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	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)$$
6		simpl	$$⊢\left(M\in B\wedge \forall i\in N\forall j\in N\left(i\ne j\to iMj=\underset{\dot{}}{0}\right)\right)\to M\in B$$
7	5 6	syl6bi	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to \left(M\in D\to M\in B\right)$$