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 e. ( R LMIso S ) -> F e. ( R GrpIso S ) )

Proof

Step	Hyp	Ref	Expression
1		lmimlmhm	|- ( F e. ( R LMIso S ) -> F e. ( R LMHom S ) )
2		lmghm	|- ( F e. ( R LMHom S ) -> F e. ( R GrpHom S ) )
3	1 2	syl	|- ( F e. ( R LMIso S ) -> F e. ( R GrpHom S ) )
4		eqid	|- ( Base ` R ) = ( Base ` R )
5		eqid	|- ( Base ` S ) = ( Base ` S )
6	4 5	lmimf1o	|- ( F e. ( R LMIso 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 LMIso S ) -> F e. ( R GrpIso S ) )