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

Metamath Proof Explorer

Theorem rimgim

Description: An isomorphism of rings is an isomorphism of their additive groups. (Contributed by AV, 24-Dec-2019)

Ref Expression
Assertion rimgim 
|- ( F e. ( R RingIso S ) -> F e. ( R GrpIso S ) )

Proof

Step Hyp Ref Expression
1 rimrhm 
 |-  ( F e. ( R RingIso S ) -> F e. ( R RingHom S ) )
2 rhmghm 
 |-  ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) )
3 1 2 syl 
 |-  ( F e. ( R RingIso S ) -> F e. ( R GrpHom S ) )
4 eqid 
 |-  ( Base ` R ) = ( Base ` R )
5 eqid 
 |-  ( Base ` S ) = ( Base ` S )
6 4 5 rimf1o 
 |-  ( F e. ( R RingIso S ) -> F : ( Base ` R ) -1-1-onto-> ( Base ` S ) )
7 4 5 isgim 
 |-  ( F e. ( R GrpIso S ) <-> ( F e. ( R GrpHom S ) /\ F : ( Base ` R ) -1-1-onto-> ( Base ` S ) ) )
8 3 6 7 sylanbrc 
 |-  ( F e. ( R RingIso S ) -> F e. ( R GrpIso S ) )