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

Metamath Proof Explorer

Theorem mat1rhm

Description: There is a ring homomorphism 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 mat1rhm ⊢ R ∈ Ring ∧ E ∈ V → F ∈ R RingHom 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 simpl ⊢ R ∈ Ring ∧ E ∈ V → R ∈ Ring
7 snfi ⊢ E ∈ Fin
8 2 matring ⊢ E ∈ Fin ∧ R ∈ Ring → A ∈ Ring
9 7 6 8 sylancr ⊢ R ∈ Ring ∧ E ∈ V → A ∈ Ring
10 1 2 3 4 5 mat1ghm ⊢ R ∈ Ring ∧ E ∈ V → F ∈ R GrpHom A
11 eqid ⊢ mulGrp R = mulGrp R
12 eqid ⊢ mulGrp A = mulGrp A
13 1 2 3 4 5 11 12 mat1mhm ⊢ R ∈ Ring ∧ E ∈ V → F ∈ mulGrp R MndHom mulGrp A
14 10 13 jca ⊢ R ∈ Ring ∧ E ∈ V → F ∈ R GrpHom A ∧ F ∈ mulGrp R MndHom mulGrp A
15 11 12 isrhm ⊢ F ∈ R RingHom A ↔ R ∈ Ring ∧ A ∈ Ring ∧ F ∈ R GrpHom A ∧ F ∈ mulGrp R MndHom mulGrp A
16 6 9 14 15 syl21anbrc ⊢ R ∈ Ring ∧ E ∈ V → F ∈ R RingHom A