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

Metamath Proof Explorer

Theorem idrnghm

Description: The identity homomorphism on a non-unital ring. (Contributed by AV, 27-Feb-2020)

Ref Expression
Hypothesis idrnghm.b ⊢ B = Base R
Assertion idrnghm ⊢ R ∈ Rng → I ↾ B ∈ R RngHom R

Proof

Step Hyp Ref Expression
1 idrnghm.b ⊢ B = Base R
2 id ⊢ R ∈ Rng → R ∈ Rng
3 2 2 jca ⊢ R ∈ Rng → R ∈ Rng ∧ R ∈ Rng
4 rngabl ⊢ R ∈ Rng → R ∈ Abel
5 ablgrp ⊢ R ∈ Abel → R ∈ Grp
6 1 idghm ⊢ R ∈ Grp → I ↾ B ∈ R GrpHom R
7 4 5 6 3syl ⊢ R ∈ Rng → I ↾ B ∈ R GrpHom R
8 eqid ⊢ mulGrp R = mulGrp R
9 8 rngmgp ⊢ R ∈ Rng → mulGrp R ∈ Smgrp
10 sgrpmgm ⊢ mulGrp R ∈ Smgrp → mulGrp R ∈ Mgm
11 8 1 mgpbas ⊢ B = Base mulGrp R
12 11 idmgmhm ⊢ mulGrp R ∈ Mgm → I ↾ B ∈ mulGrp R MgmHom mulGrp R
13 9 10 12 3syl ⊢ R ∈ Rng → I ↾ B ∈ mulGrp R MgmHom mulGrp R
14 7 13 jca ⊢ R ∈ Rng → I ↾ B ∈ R GrpHom R ∧ I ↾ B ∈ mulGrp R MgmHom mulGrp R
15 8 8 isrnghmmul ⊢ I ↾ B ∈ R RngHom R ↔ R ∈ Rng ∧ R ∈ Rng ∧ I ↾ B ∈ R GrpHom R ∧ I ↾ B ∈ mulGrp R MgmHom mulGrp R
16 3 14 15 sylanbrc ⊢ R ∈ Rng → I ↾ B ∈ R RngHom R