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 e. Rng /\ S e. Rng ) -> ( R RngHom S ) = ( ( R GrpHom S ) i^i ( ( 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 e. ( R RngHom S ) <-> ( ( R e. Rng /\ S e. Rng ) /\ ( h e. ( R GrpHom S ) /\ h e. ( ( mulGrp ` R ) MgmHom ( mulGrp ` S ) ) ) ) )
4 elin 
 |-  ( h e. ( ( R GrpHom S ) i^i ( ( mulGrp ` R ) MgmHom ( mulGrp ` S ) ) ) <-> ( h e. ( R GrpHom S ) /\ h e. ( ( mulGrp ` R ) MgmHom ( mulGrp ` S ) ) ) )
5 ibar 
 |-  ( ( R e. Rng /\ S e. Rng ) -> ( ( h e. ( R GrpHom S ) /\ h e. ( ( mulGrp ` R ) MgmHom ( mulGrp ` S ) ) ) <-> ( ( R e. Rng /\ S e. Rng ) /\ ( h e. ( R GrpHom S ) /\ h e. ( ( mulGrp ` R ) MgmHom ( mulGrp ` S ) ) ) ) ) )
6 4 5 bitr2id 
 |-  ( ( R e. Rng /\ S e. Rng ) -> ( ( ( R e. Rng /\ S e. Rng ) /\ ( h e. ( R GrpHom S ) /\ h e. ( ( mulGrp ` R ) MgmHom ( mulGrp ` S ) ) ) ) <-> h e. ( ( R GrpHom S ) i^i ( ( mulGrp ` R ) MgmHom ( mulGrp ` S ) ) ) ) )
7 3 6 bitrid 
 |-  ( ( R e. Rng /\ S e. Rng ) -> ( h e. ( R RngHom S ) <-> h e. ( ( R GrpHom S ) i^i ( ( mulGrp ` R ) MgmHom ( mulGrp ` S ) ) ) ) )
8 7 eqrdv 
 |-  ( ( R e. Rng /\ S e. Rng ) -> ( R RngHom S ) = ( ( R GrpHom S ) i^i ( ( mulGrp ` R ) MgmHom ( mulGrp ` S ) ) ) )