Theorem dmatbas

Description: The set of all N x N diagonal matrices over (the ring) R is the base set of the algebra of N x N diagonal matrices over (the ring) R . (Contributed by AV, 8-Dec-2019)

	Ref	Expression
Hypotheses	dmatbas.a	$$⊢A=N\mathrm{Mat}R$$
	dmatbas.b	$$⊢B={\mathrm{Base}}_A$$
	dmatbas.0	$$⊢\underset{\dot{}}{0}=0_R$$
	dmatbas.d	$$⊢D=N\mathrm{DMat}R$$
Assertion	dmatbas	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to D={\mathrm{Base}}_{\left(N\mathrm{DMatALT}R\right)}$$

Proof

Step	Hyp	Ref	Expression
1		dmatbas.a	$$⊢A=N\mathrm{Mat}R$$
2		dmatbas.b	$$⊢B={\mathrm{Base}}_A$$
3		dmatbas.0	$$⊢\underset{\dot{}}{0}=0_R$$
4		dmatbas.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		elex	$$⊢R\in V\to R\in \mathrm{V}$$
7		eqid	$$⊢N\mathrm{DMatALT}R=N\mathrm{DMatALT}R$$
8	1 2 3 7	dmatALTbas	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)\to {\mathrm{Base}}_{\left(N\mathrm{DMatALT}R\right)}=\left\{m\in B|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}$$
9	6 8	sylan2	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to {\mathrm{Base}}_{\left(N\mathrm{DMatALT}R\right)}=\left\{m\in B|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}$$
10	5 9	eqtr4d	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to D={\mathrm{Base}}_{\left(N\mathrm{DMatALT}R\right)}$$