Theorem ricgic

Description: If two rings are (ring) isomorphic, their additive groups are (group) isomorphic. (Contributed by AV, 24-Dec-2019)

	Ref	Expression
Assertion	ricgic	|- ( R ~=r S -> R ~=g S )

Proof

Step	Hyp	Ref	Expression
1		brric2	|- ( R ~=r S <-> ( ( R e. Ring /\ S e. Ring ) /\ E. f f e. ( R RingIso S ) ) )
2		rimgim	|- ( f e. ( R RingIso S ) -> f e. ( R GrpIso S ) )
3		brgici	|- ( f e. ( R GrpIso S ) -> R ~=g S )
4	2 3	syl	|- ( f e. ( R RingIso S ) -> R ~=g S )
5	4	exlimiv	|- ( E. f f e. ( R RingIso S ) -> R ~=g S )
6	1 5	simplbiim	|- ( R ~=r S -> R ~=g S )