This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 1 3 isrim ⊢ F ∈ R RingIso A ↔ F ∈ R RingHom A ∧ F : K ⟶ 1-1 onto B
9 6 7 8 sylanbrc ⊢ R ∈ Ring ∧ E ∈ V → F ∈ R RingIso A