Metamath Proof Explorer

Theorem mat1rngiso

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

Ref Expression
Hypotheses mat1rhmval.k ⊢ K = Base R
mat1rhmval.a ⊢ A = E Mat R
mat1rhmval.b ⊢ B = Base A
mat1rhmval.o ⊢ O = E E
mat1rhmval.f ⊢ F = x ∈ K ⟼ O x
Assertion mat1rngiso ⊢ R ∈ Ring ∧ E ∈ V → F ∈ R RingIso A

Proof

Step Hyp Ref Expression
1 mat1rhmval.k ⊢ K = Base R
2 mat1rhmval.a ⊢ A = E Mat R
3 mat1rhmval.b ⊢ B = Base A
4 mat1rhmval.o ⊢ O = E E
5 mat1rhmval.f ⊢ F = x ∈ K ⟼ O x
6 1 2 3 4 5 mat1rhm ⊢ R ∈ Ring ∧ E ∈ V → F ∈ R RingHom A
7 1 2 3 4 5 mat1f1o ⊢ R ∈ Ring ∧ E ∈ V → F : K ⟶ 1-1 onto B
8 snfi ⊢ E ∈ Fin
9 simpl ⊢ R ∈ Ring ∧ E ∈ V → R ∈ Ring
10 2 matring ⊢ E ∈ Fin ∧ R ∈ Ring → A ∈ Ring
11 8 9 10 sylancr ⊢ R ∈ Ring ∧ E ∈ V → A ∈ Ring
12 1 3 isrim ⊢ R ∈ Ring ∧ A ∈ Ring → F ∈ R RingIso A ↔ F ∈ R RingHom A ∧ F : K ⟶ 1-1 onto B
13 11 12 syldan ⊢ R ∈ Ring ∧ E ∈ V → F ∈ R RingIso A ↔ F ∈ R RingHom A ∧ F : K ⟶ 1-1 onto B
14 6 7 13 mpbir2and ⊢ R ∈ Ring ∧ E ∈ V → F ∈ R RingIso A