Metamath Proof Explorer


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=NMatR
dmatbas.b B=BaseA
dmatbas.0 0˙=0R
dmatbas.d D=NDMatR
Assertion dmatbas NFinRVD=BaseNDMatALTR

Proof

Step Hyp Ref Expression
1 dmatbas.a A=NMatR
2 dmatbas.b B=BaseA
3 dmatbas.0 0˙=0R
4 dmatbas.d D=NDMatR
5 1 2 3 4 dmatval NFinRVD=mB|iNjNijimj=0˙
6 elex RVRV
7 eqid NDMatALTR=NDMatALTR
8 1 2 3 7 dmatALTbas NFinRVBaseNDMatALTR=mB|iNjNijimj=0˙
9 6 8 sylan2 NFinRVBaseNDMatALTR=mB|iNjNijimj=0˙
10 5 9 eqtr4d NFinRVD=BaseNDMatALTR