rimgim

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

		Ref	Expression
	Assertion	rimgim	$⊢ F \in (R RingIso S) \to F \in (R GrpIso S)$

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{R} = {Base}_{R}$
2		eqid	$⊢ {Base}_{S} = {Base}_{S}$
3	1 2	rimrhm	$⊢ F \in (R RingIso S) \to F \in (R RingHom S)$
4		rhmghm	$⊢ F \in (R RingHom S) \to F \in (R GrpHom S)$
5	3 4	syl	$⊢ F \in (R RingIso S) \to F \in (R GrpHom S)$
6	1 2	rimf1o	$⊢ F \in (R RingIso S) \to F : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S}$
7	1 2	isgim	$⊢ F \in (R GrpIso S) \leftrightarrow (F \in (R GrpHom S) \land F : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S})$
8	5 6 7	sylanbrc	$⊢ F \in (R RingIso S) \to F \in (R GrpIso S)$

Metamath Proof Explorer