Metamath Proof Explorer

Theorem scmatrngiso

Description: There is a ring isomorphism from a ring to the ring of scalar matrices over this ring with positive dimension. (Contributed by AV, 29-Dec-2019)

Ref Expression
Hypotheses scmatrhmval.k ⊢ K = Base R
scmatrhmval.a ⊢ A = N Mat R
scmatrhmval.o ⊢ 1 ˙ = 1 A
scmatrhmval.t ⊢ ∗ ˙ = ⋅ A
scmatrhmval.f ⊢ F = x ∈ K ⟼ x ∗ ˙ 1 ˙
scmatrhmval.c ⊢ C = N ScMat R
scmatghm.s ⊢ S = A ↾ 𝑠 C
Assertion scmatrngiso ⊢ N ∈ Fin ∧ N ≠ ∅ ∧ R ∈ Ring → F ∈ R RingIso S

Proof

Step Hyp Ref Expression
1 scmatrhmval.k ⊢ K = Base R
2 scmatrhmval.a ⊢ A = N Mat R
3 scmatrhmval.o ⊢ 1 ˙ = 1 A
4 scmatrhmval.t ⊢ ∗ ˙ = ⋅ A
5 scmatrhmval.f ⊢ F = x ∈ K ⟼ x ∗ ˙ 1 ˙
6 scmatrhmval.c ⊢ C = N ScMat R
7 scmatghm.s ⊢ S = A ↾ 𝑠 C
8 1 2 3 4 5 6 7 scmatrhm ⊢ N ∈ Fin ∧ R ∈ Ring → F ∈ R RingHom S
9 8 3adant2 ⊢ N ∈ Fin ∧ N ≠ ∅ ∧ R ∈ Ring → F ∈ R RingHom S
10 1 2 3 4 5 6 scmatf1o ⊢ N ∈ Fin ∧ N ≠ ∅ ∧ R ∈ Ring → F : K ⟶ 1-1 onto C
11 2 6 7 scmatstrbas ⊢ N ∈ Fin ∧ R ∈ Ring → Base S = C
12 11 3adant2 ⊢ N ∈ Fin ∧ N ≠ ∅ ∧ R ∈ Ring → Base S = C
13 12 f1oeq3d ⊢ N ∈ Fin ∧ N ≠ ∅ ∧ R ∈ Ring → F : K ⟶ 1-1 onto Base S ↔ F : K ⟶ 1-1 onto C
14 10 13 mpbird ⊢ N ∈ Fin ∧ N ≠ ∅ ∧ R ∈ Ring → F : K ⟶ 1-1 onto Base S
15 simp3 ⊢ N ∈ Fin ∧ N ≠ ∅ ∧ R ∈ Ring → R ∈ Ring
16 eqid ⊢ Base A = Base A
17 eqid ⊢ 0 R = 0 R
18 2 16 1 17 6 scmatsrng ⊢ N ∈ Fin ∧ R ∈ Ring → C ∈ SubRing ⁡ A
19 7 subrgring ⊢ C ∈ SubRing ⁡ A → S ∈ Ring
20 18 19 syl ⊢ N ∈ Fin ∧ R ∈ Ring → S ∈ Ring
21 eqid ⊢ Base S = Base S
22 1 21 isrim ⊢ R ∈ Ring ∧ S ∈ Ring → F ∈ R RingIso S ↔ F ∈ R RingHom S ∧ F : K ⟶ 1-1 onto Base S
23 15 20 22 3imp3i2an ⊢ N ∈ Fin ∧ N ≠ ∅ ∧ R ∈ Ring → F ∈ R RingIso S ↔ F ∈ R RingHom S ∧ F : K ⟶ 1-1 onto Base S
24 9 14 23 mpbir2and ⊢ N ∈ Fin ∧ N ≠ ∅ ∧ R ∈ Ring → F ∈ R RingIso S