Description: The ring of matrices over a commutative ring is isomorphic to the ring of scalar matrices over the same ring. (Contributed by AV, 30-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | matcpmric.a | |
|
matcpmric.p | |
||
matcpmric.c | |
||
matcpmric.s | |
||
matcpmric.u | |
||
Assertion | matcpmric | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | matcpmric.a | |
|
2 | matcpmric.p | |
|
3 | matcpmric.c | |
|
4 | matcpmric.s | |
|
5 | matcpmric.u | |
|
6 | eqid | |
|
7 | eqid | |
|
8 | 4 6 1 7 2 3 5 | m2cpmrngiso | |
9 | 8 | ne0d | |
10 | brric | |
|
11 | 9 10 | sylibr | |