Metamath Proof Explorer

Theorem idrhm

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

Ref Expression
Hypothesis idrhm.b ⊢ B = Base R
Assertion idrhm ⊢ R ∈ Ring → I ↾ B ∈ R RingHom R

Proof

Step Hyp Ref Expression
1 idrhm.b ⊢ B = Base R
2 id ⊢ R ∈ Ring → R ∈ Ring
3 ringgrp ⊢ R ∈ Ring → R ∈ Grp
4 1 idghm ⊢ R ∈ Grp → I ↾ B ∈ R GrpHom R
5 3 4 syl ⊢ R ∈ Ring → I ↾ B ∈ R GrpHom R
6 eqid ⊢ mulGrp R = mulGrp R
7 6 ringmgp ⊢ R ∈ Ring → mulGrp R ∈ Mnd
8 6 1 mgpbas ⊢ B = Base mulGrp R
9 8 idmhm ⊢ mulGrp R ∈ Mnd → I ↾ B ∈ mulGrp R MndHom mulGrp R
10 7 9 syl ⊢ R ∈ Ring → I ↾ B ∈ mulGrp R MndHom mulGrp R
11 5 10 jca ⊢ R ∈ Ring → I ↾ B ∈ R GrpHom R ∧ I ↾ B ∈ mulGrp R MndHom mulGrp R
12 6 6 isrhm ⊢ I ↾ B ∈ R RingHom R ↔ R ∈ Ring ∧ R ∈ Ring ∧ I ↾ B ∈ R GrpHom R ∧ I ↾ B ∈ mulGrp R MndHom mulGrp R
13 2 2 11 12 syl21anbrc ⊢ R ∈ Ring → I ↾ B ∈ R RingHom R