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 RngHomo 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 Could not format ( R e. Rng -> ( mulGrp ` R ) e. Smgrp ) : No typesetting found for |- ( R e. Rng -> ( mulGrp ` R ) e. Smgrp ) with typecode |-
10 sgrpmgm Could not format ( ( mulGrp ` R ) e. Smgrp -> ( mulGrp ` R ) e. Mgm ) : No typesetting found for |- ( ( mulGrp ` R ) e. Smgrp -> ( mulGrp ` R ) e. Mgm ) with typecode |-
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 RngHomo 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 RngHomo R