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

Metamath Proof Explorer

Theorem rnghmval2

Description: The non-unital ring homomorphisms between two non-unital rings. (Contributed by AV, 1-Mar-2020)

Ref Expression
Assertion rnghmval2 ⊢ R ∈ Rng ∧ S ∈ Rng → R RngHom S = R GrpHom S ∩ mulGrp R MgmHom mulGrp S

Proof

Step Hyp Ref Expression
1 eqid ⊢ mulGrp R = mulGrp R
2 eqid ⊢ mulGrp S = mulGrp S
3 1 2 isrnghmmul ⊢ h ∈ R RngHom S ↔ R ∈ Rng ∧ S ∈ Rng ∧ h ∈ R GrpHom S ∧ h ∈ mulGrp R MgmHom mulGrp S
4 elin ⊢ h ∈ R GrpHom S ∩ mulGrp R MgmHom mulGrp S ↔ h ∈ R GrpHom S ∧ h ∈ mulGrp R MgmHom mulGrp S
5 ibar ⊢ R ∈ Rng ∧ S ∈ Rng → h ∈ R GrpHom S ∧ h ∈ mulGrp R MgmHom mulGrp S ↔ R ∈ Rng ∧ S ∈ Rng ∧ h ∈ R GrpHom S ∧ h ∈ mulGrp R MgmHom mulGrp S
6 4 5 bitr2id ⊢ R ∈ Rng ∧ S ∈ Rng → R ∈ Rng ∧ S ∈ Rng ∧ h ∈ R GrpHom S ∧ h ∈ mulGrp R MgmHom mulGrp S ↔ h ∈ R GrpHom S ∩ mulGrp R MgmHom mulGrp S
7 3 6 bitrid ⊢ R ∈ Rng ∧ S ∈ Rng → h ∈ R RngHom S ↔ h ∈ R GrpHom S ∩ mulGrp R MgmHom mulGrp S
8 7 eqrdv ⊢ R ∈ Rng ∧ S ∈ Rng → R RngHom S = R GrpHom S ∩ mulGrp R MgmHom mulGrp S