Theorem dmatALTval

Description: The algebra of N x N diagonal matrices over a 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	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\}$$

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		ovexd	$$⊢\left(n=N\wedge r=R\right)\to n\mathrm{Mat}r\in \mathrm{V}$$
6		id	$$⊢a=n\mathrm{Mat}r\to a=n\mathrm{Mat}r$$
7		fveq2	$$⊢a=n\mathrm{Mat}r\to {\mathrm{Base}}_a={\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}$$
8	7	rabeqdv	$$⊢a=n\mathrm{Mat}r\to \left\{m\in {\mathrm{Base}}_a|\forall i\in n\forall j\in n\left(i\ne j\to imj=0_r\right)\right\}=\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\}$$
9	6 8	oveq12d	$$⊢a=n\mathrm{Mat}r\to a{\upharpoonright }_{𝑠}\left\{m\in {\mathrm{Base}}_a|\forall i\in n\forall j\in n\left(i\ne j\to imj=0_r\right)\right\}=\left(n\mathrm{Mat}r\right){\upharpoonright }_{𝑠}\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\}$$
10	9	adantl	$$⊢\left(\left(n=N\wedge r=R\right)\wedge a=n\mathrm{Mat}r\right)\to a{\upharpoonright }_{𝑠}\left\{m\in {\mathrm{Base}}_a|\forall i\in n\forall j\in n\left(i\ne j\to imj=0_r\right)\right\}=\left(n\mathrm{Mat}r\right){\upharpoonright }_{𝑠}\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\}$$
11	5 10	csbied	$$⊢\left(n=N\wedge r=R\right)\to ⦋\left(n\mathrm{Mat}r\right)/a⦌\left(a{\upharpoonright }_{𝑠}\left\{m\in {\mathrm{Base}}_a|\forall i\in n\forall j\in n\left(i\ne j\to imj=0_r\right)\right\}\right)=\left(n\mathrm{Mat}r\right){\upharpoonright }_{𝑠}\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\}$$
12		oveq12	$$⊢\left(n=N\wedge r=R\right)\to n\mathrm{Mat}r=N\mathrm{Mat}R$$
13	12 1	eqtr4di	$$⊢\left(n=N\wedge r=R\right)\to n\mathrm{Mat}r=A$$
14	13	fveq2d	$$⊢\left(n=N\wedge r=R\right)\to {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}={\mathrm{Base}}_A$$
15	14 2	eqtr4di	$$⊢\left(n=N\wedge r=R\right)\to {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}=B$$
16		simpl	$$⊢\left(n=N\wedge r=R\right)\to n=N$$
17		fveq2	$$⊢r=R\to 0_r=0_R$$
18	17 3	eqtr4di	$$⊢r=R\to 0_r=\underset{\dot{}}{0}$$
19	18	adantl	$$⊢\left(n=N\wedge r=R\right)\to 0_r=\underset{\dot{}}{0}$$
20	19	eqeq2d	$$⊢\left(n=N\wedge r=R\right)\to \left(imj=0_r\leftrightarrow imj=\underset{\dot{}}{0}\right)$$
21	20	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)$$
22	16 21	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)$$
23	16 22	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)$$
24	15 23	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\}$$
25	13 24	oveq12d	$$⊢\left(n=N\wedge r=R\right)\to \left(n\mathrm{Mat}r\right){\upharpoonright }_{𝑠}\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\}=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\}$$
26	11 25	eqtrd	$$⊢\left(n=N\wedge r=R\right)\to ⦋\left(n\mathrm{Mat}r\right)/a⦌\left(a{\upharpoonright }_{𝑠}\left\{m\in {\mathrm{Base}}_a|\forall i\in n\forall j\in n\left(i\ne j\to imj=0_r\right)\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\}$$
27		df-dmatalt	$$⊢\mathrm{DMatALT}=\left(n\in \mathrm{Fin},r\in \mathrm{V}⟼⦋\left(n\mathrm{Mat}r\right)/a⦌\left(a{\upharpoonright }_{𝑠}\left\{m\in {\mathrm{Base}}_a|\forall i\in n\forall j\in n\left(i\ne j\to imj=0_r\right)\right\}\right)\right)$$
28		ovex	$$⊢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\}\in \mathrm{V}$$
29	26 27 28	ovmpoa	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)\to N\mathrm{DMatALT}R=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\}$$
30	4 29	syl5eq	$$⊢\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\}$$