Metamath Proof Explorer

Theorem scmatric

Description: A ring is isomorphic to every ring of scalar matrices over this ring with positive dimension. (Contributed by AV, 29-Dec-2019)

Ref Expression
Hypotheses scmatric.a ⊢ A = N Mat R
scmatric.c ⊢ C = N ScMat R
scmatric.s ⊢ S = A ↾ 𝑠 C
Assertion scmatric ⊢ N ∈ Fin ∧ N ≠ ∅ ∧ R ∈ Ring → R ≃ 𝑟 S

Proof

Step Hyp Ref Expression
1 scmatric.a ⊢ A = N Mat R
2 scmatric.c ⊢ C = N ScMat R
3 scmatric.s ⊢ S = A ↾ 𝑠 C
4 eqid ⊢ Base R = Base R
5 eqid ⊢ 1 A = 1 A
6 eqid ⊢ ⋅ A = ⋅ A
7 eqid ⊢ x ∈ Base R ⟼ x ⋅ A 1 A = x ∈ Base R ⟼ x ⋅ A 1 A
8 4 1 5 6 7 2 3 scmatrngiso ⊢ N ∈ Fin ∧ N ≠ ∅ ∧ R ∈ Ring → x ∈ Base R ⟼ x ⋅ A 1 A ∈ R RingIso S
9 8 ne0d ⊢ N ∈ Fin ∧ N ≠ ∅ ∧ R ∈ Ring → R RingIso S ≠ ∅
10 brric ⊢ R ≃ 𝑟 S ↔ R RingIso S ≠ ∅
11 9 10 sylibr ⊢ N ∈ Fin ∧ N ≠ ∅ ∧ R ∈ Ring → R ≃ 𝑟 S