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	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	dmatbas.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	dmatbas.0	⊢ 0 = ( 0g ‘ 𝑅 )
	dmatbas.d	⊢ 𝐷 = ( 𝑁 DMat 𝑅 )
Assertion	dmatbas	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝐷 = ( Base ‘ ( 𝑁 DMatALT 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dmatbas.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		dmatbas.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		dmatbas.0	⊢ 0 = ( 0g ‘ 𝑅 )
4		dmatbas.d	⊢ 𝐷 = ( 𝑁 DMat 𝑅 )
5	1 2 3 4	dmatval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝐷 = { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } )
6		elex	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
7		eqid	⊢ ( 𝑁 DMatALT 𝑅 ) = ( 𝑁 DMatALT 𝑅 )
8	1 2 3 7	dmatALTbas	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( Base ‘ ( 𝑁 DMatALT 𝑅 ) ) = { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } )
9	6 8	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( Base ‘ ( 𝑁 DMatALT 𝑅 ) ) = { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } )
10	5 9	eqtr4d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝐷 = ( Base ‘ ( 𝑁 DMatALT 𝑅 ) ) )