This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lmhmlmod2

Description: A homomorphism of left modules has a left module as codomain. (Contributed by Stefan O'Rear, 1-Jan-2015)

		Ref	Expression
	Assertion	lmhmlmod2	$⊢ F \in (S LMHom T) \to T \in LMod$

Step	Hyp	Ref	Expression
1		eqid	$⊢ Scalar (S) = Scalar (S)$
2		eqid	$⊢ Scalar (T) = Scalar (T)$
3	1 2	lmhmlem	$⊢ F \in (S LMHom T) \to ((S \in LMod \land T \in LMod) \land (F \in (S GrpHom T) \land Scalar (T) = Scalar (S)))$
4	3	simplrd	$⊢ F \in (S LMHom T) \to T \in LMod$