Theorem lmhmrnlss

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

	Ref	Expression
Assertion	lmhmrnlss	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ran 𝐹 ∈ ( LSubSp ‘ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
2		eqid	⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
3	1 2	lmhmf	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
4		ffn	⊢ ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) → 𝐹 Fn ( Base ‘ 𝑆 ) )
5		fnima	⊢ ( 𝐹 Fn ( Base ‘ 𝑆 ) → ( 𝐹 “ ( Base ‘ 𝑆 ) ) = ran 𝐹 )
6	3 4 5	3syl	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( 𝐹 “ ( Base ‘ 𝑆 ) ) = ran 𝐹 )
7		lmhmlmod1	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑆 ∈ LMod )
8		eqid	⊢ ( LSubSp ‘ 𝑆 ) = ( LSubSp ‘ 𝑆 )
9	1 8	lss1	⊢ ( 𝑆 ∈ LMod → ( Base ‘ 𝑆 ) ∈ ( LSubSp ‘ 𝑆 ) )
10	7 9	syl	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( Base ‘ 𝑆 ) ∈ ( LSubSp ‘ 𝑆 ) )
11		eqid	⊢ ( LSubSp ‘ 𝑇 ) = ( LSubSp ‘ 𝑇 )
12	8 11	lmhmima	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ( Base ‘ 𝑆 ) ∈ ( LSubSp ‘ 𝑆 ) ) → ( 𝐹 “ ( Base ‘ 𝑆 ) ) ∈ ( LSubSp ‘ 𝑇 ) )
13	10 12	mpdan	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( 𝐹 “ ( Base ‘ 𝑆 ) ) ∈ ( LSubSp ‘ 𝑇 ) )
14	6 13	eqeltrrd	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ran 𝐹 ∈ ( LSubSp ‘ 𝑇 ) )