Metamath Proof Explorer

Theorem lmimgim

Description: An isomorphism of modules is an isomorphism of groups. (Contributed by Stefan O'Rear, 21-Jan-2015) (Revised by Mario Carneiro, 6-May-2015)

		Ref	Expression
	Assertion	lmimgim	$⊢ F \in (R LMIso S) \to F \in (R GrpIso S)$

Proof

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