Metamath Proof Explorer

Theorem rnghmghm

Description: A non-unital ring homomorphism is an additive group homomorphism. (Contributed by AV, 23-Feb-2020)

Ref Expression
Assertion rnghmghm 
|- ( F e. ( R RngHomo S ) -> F e. ( R GrpHom S ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` R ) = ( Base ` R )
2 eqid 
 |-  ( .r ` R ) = ( .r ` R )
3 eqid 
 |-  ( .r ` S ) = ( .r ` S )
4 1 2 3 isrnghm 
 |-  ( F e. ( R RngHomo S ) <-> ( ( R e. Rng /\ S e. Rng ) /\ ( F e. ( R GrpHom S ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) ( .r ` S ) ( F ` y ) ) ) ) )
5 simprl 
 |-  ( ( ( R e. Rng /\ S e. Rng ) /\ ( F e. ( R GrpHom S ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) ( .r ` S ) ( F ` y ) ) ) ) -> F e. ( R GrpHom S ) )
6 4 5 sylbi 
 |-  ( F e. ( R RngHomo S ) -> F e. ( R GrpHom S ) )