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 R RingIso S F R GrpIso S

Proof

Step Hyp Ref Expression
1 rimrhm F R RingIso S F R RingHom S
2 rhmghm F R RingHom S F R GrpHom S
3 1 2 syl F R RingIso S F R GrpHom S
4 eqid Base R = Base R
5 eqid Base S = Base S
6 4 5 rimf1o F R RingIso S F : Base R 1-1 onto Base S
7 4 5 isgim F R GrpIso S F R GrpHom S F : Base R 1-1 onto Base S
8 3 6 7 sylanbrc F R RingIso S F R GrpIso S