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 RngHomo 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 RngHomo 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 syl5bb R Rng S Rng h R RngHomo S h R GrpHom S mulGrp R MgmHom mulGrp S
8 7 eqrdv R Rng S Rng R RngHomo S = R GrpHom S mulGrp R MgmHom mulGrp S