lmhmrnlss

Description: The range of a homomorphism is a submodule. (Contributed by Stefan O'Rear, 1-Jan-2015)

		Ref	Expression
	Assertion	lmhmrnlss	$⊢ F \in (S LMHom T) \to ran F \in LSubSp (T)$

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{S} = {Base}_{S}$
2		eqid	$⊢ {Base}_{T} = {Base}_{T}$
3	1 2	lmhmf	$⊢ F \in (S LMHom T) \to F : {Base}_{S} ⟶ {Base}_{T}$
4		ffn	$⊢ F : {Base}_{S} ⟶ {Base}_{T} \to F Fn {Base}_{S}$
5		fnima	$⊢ F Fn {Base}_{S} \to F [{Base}_{S}] = ran F$
6	3 4 5	3syl	$⊢ F \in (S LMHom T) \to F [{Base}_{S}] = ran F$
7		lmhmlmod1	$⊢ F \in (S LMHom T) \to S \in LMod$
8		eqid	$⊢ LSubSp (S) = LSubSp (S)$
9	1 8	lss1	$⊢ S \in LMod \to {Base}_{S} \in LSubSp (S)$
10	7 9	syl	$⊢ F \in (S LMHom T) \to {Base}_{S} \in LSubSp (S)$
11		eqid	$⊢ LSubSp (T) = LSubSp (T)$
12	8 11	lmhmima	$⊢ (F \in (S LMHom T) \land {Base}_{S} \in LSubSp (S)) \to F [{Base}_{S}] \in LSubSp (T)$
13	10 12	mpdan	$⊢ F \in (S LMHom T) \to F [{Base}_{S}] \in LSubSp (T)$
14	6 13	eqeltrrd	$⊢ F \in (S LMHom T) \to ran F \in LSubSp (T)$

Metamath Proof Explorer