Theorem dmatval

Description: The set of N x N diagonal matrices over (a ring) R . (Contributed by AV, 8-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	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\}$$

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		df-dmat	$$⊢\mathrm{DMat}=\left(n\in \mathrm{Fin},r\in \mathrm{V}⟼\left\{m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}|\forall i\in n\forall j\in n\left(i\ne j\to imj=0_r\right)\right\}\right)$$
6	5	a1i	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to \mathrm{DMat}=\left(n\in \mathrm{Fin},r\in \mathrm{V}⟼\left\{m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}|\forall i\in n\forall j\in n\left(i\ne j\to imj=0_r\right)\right\}\right)$$
7		oveq12	$$⊢\left(n=N\wedge r=R\right)\to n\mathrm{Mat}r=N\mathrm{Mat}R$$
8	7	fveq2d	$$⊢\left(n=N\wedge r=R\right)\to {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}={\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}$$
9	1	fveq2i	$$⊢{\mathrm{Base}}_A={\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}$$
10	2 9	eqtri	$$⊢B={\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}$$
11	8 10	eqtr4di	$$⊢\left(n=N\wedge r=R\right)\to {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}=B$$
12		simpl	$$⊢\left(n=N\wedge r=R\right)\to n=N$$
13		fveq2	$$⊢r=R\to 0_r=0_R$$
14	13 3	eqtr4di	$$⊢r=R\to 0_r=\underset{\dot{}}{0}$$
15	14	adantl	$$⊢\left(n=N\wedge r=R\right)\to 0_r=\underset{\dot{}}{0}$$
16	15	eqeq2d	$$⊢\left(n=N\wedge r=R\right)\to \left(imj=0_r\leftrightarrow imj=\underset{\dot{}}{0}\right)$$
17	16	imbi2d	$$⊢\left(n=N\wedge r=R\right)\to \left(\left(i\ne j\to imj=0_r\right)\leftrightarrow \left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right)$$
18	12 17	raleqbidv	$$⊢\left(n=N\wedge r=R\right)\to \left(\forall j\in n\left(i\ne j\to imj=0_r\right)\leftrightarrow \forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right)$$
19	12 18	raleqbidv	$$⊢\left(n=N\wedge r=R\right)\to \left(\forall i\in n\forall j\in n\left(i\ne j\to imj=0_r\right)\leftrightarrow \forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right)$$
20	11 19	rabeqbidv	$$⊢\left(n=N\wedge r=R\right)\to \left\{m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}|\forall i\in n\forall j\in n\left(i\ne j\to imj=0_r\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\}$$
21	20	adantl	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in V\right)\wedge \left(n=N\wedge r=R\right)\right)\to \left\{m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}|\forall i\in n\forall j\in n\left(i\ne j\to imj=0_r\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\}$$
22		simpl	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to N\in \mathrm{Fin}$$
23		elex	$$⊢R\in V\to R\in \mathrm{V}$$
24	23	adantl	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to R\in \mathrm{V}$$
25	2	fvexi	$$⊢B\in \mathrm{V}$$
26		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}$$
27	25 26	mp1i	$$⊢\left(N\in \mathrm{Fin}\wedge R\in 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}$$
28	6 21 22 24 27	ovmpod	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to N\mathrm{DMat}R=\left\{m\in B|\forall i\in N\forall j\in N\left(i\ne j\to imj=\underset{\dot{}}{0}\right)\right\}$$
29	4 28	syl5eq	$$⊢\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\}$$