Metamath Proof Explorer

Theorem lmimlmhm

Description: An isomorphism of modules is a homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015)

		Ref	Expression
	Assertion	lmimlmhm	$⊢ F \in (R LMIso S) \to F \in (R LMHom S)$

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{R} = {Base}_{R}$
2		eqid	$⊢ {Base}_{S} = {Base}_{S}$
3	1 2	islmim	$⊢ F \in (R LMIso S) \leftrightarrow (F \in (R LMHom S) \land F : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S})$
4	3	simplbi	$⊢ F \in (R LMIso S) \to F \in (R LMHom S)$