Theorem dmatALTbas

Description: The base set of the algebra of N x N diagonal matrices over a ring R , i.e. the set of all N x N diagonal matrices 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	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\}$$

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	dmatALTval	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)\to D=A{\upharpoonright }_{𝑠}\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	fveq2d	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)\to {\mathrm{Base}}_D={\mathrm{Base}}_{\left(A{\upharpoonright }_{𝑠}\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	2	fvexi	$$⊢B\in \mathrm{V}$$
8		rabexg	$$⊢B\in \mathrm{V}\to \left\{m\in B|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}\in \mathrm{V}$$
9	7 8	mp1i	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)\to \left\{m\in B|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}\in \mathrm{V}$$
10		eqid	$$⊢A{\upharpoonright }_{𝑠}\left\{m\in B|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}=A{\upharpoonright }_{𝑠}\left\{m\in B|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}$$
11	10 2	ressbas	$$⊢\left\{m\in B|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}\in \mathrm{V}\to \left\{m\in B|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}\cap B={\mathrm{Base}}_{\left(A{\upharpoonright }_{𝑠}\left\{m\in B|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}\right)}$$
12	9 11	syl	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)\to \left\{m\in B|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}\cap B={\mathrm{Base}}_{\left(A{\upharpoonright }_{𝑠}\left\{m\in B|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}\right)}$$
13		inrab2	$$⊢\left\{m\in B|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}\cap B=\left\{m\in \left(B\cap B\right)|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}$$
14		inidm	$$⊢B\cap B=B$$
15		rabeq	$$⊢B\cap B=B\to \left\{m\in \left(B\cap B\right)|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}=\left\{m\in B|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}$$
16	14 15	mp1i	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)\to \left\{m\in \left(B\cap B\right)|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}=\left\{m\in B|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}$$
17	13 16	syl5eq	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)\to \left\{m\in B|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}\cap B=\left\{m\in B|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}$$
18	6 12 17	3eqtr2d	$$⊢\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\}$$