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 | |
|
dmatbas.b | |
||
dmatbas.0 | |
||
dmatbas.d | |
||
Assertion | dmatbas | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dmatbas.a | |
|
2 | dmatbas.b | |
|
3 | dmatbas.0 | |
|
4 | dmatbas.d | |
|
5 | 1 2 3 4 | dmatval | |
6 | elex | |
|
7 | eqid | |
|
8 | 1 2 3 7 | dmatALTbas | |
9 | 6 8 | sylan2 | |
10 | 5 9 | eqtr4d | |