Metamath Proof Explorer

Theorem lmhmrnlss

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

Ref Expression
Assertion lmhmrnlss ⊢ F ∈ S LMHom T → ran ⁡ F ∈ LSubSp ⁡ T

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base S = Base S
2 eqid ⊢ Base T = Base T
3 1 2 lmhmf ⊢ F ∈ S LMHom T → F : Base S ⟶ Base T
4 ffn ⊢ F : Base S ⟶ Base T → F Fn Base S
5 fnima ⊢ F Fn Base S → F Base S = ran ⁡ F
6 3 4 5 3syl ⊢ F ∈ S LMHom T → F Base S = ran ⁡ F
7 lmhmlmod1 ⊢ F ∈ S LMHom T → S ∈ LMod
8 eqid ⊢ LSubSp ⁡ S = LSubSp ⁡ S
9 1 8 lss1 ⊢ S ∈ LMod → Base S ∈ LSubSp ⁡ S
10 7 9 syl ⊢ F ∈ S LMHom T → Base S ∈ LSubSp ⁡ S
11 eqid ⊢ LSubSp ⁡ T = LSubSp ⁡ T
12 8 11 lmhmima ⊢ F ∈ S LMHom T ∧ Base S ∈ LSubSp ⁡ S → F Base S ∈ LSubSp ⁡ T
13 10 12 mpdan ⊢ F ∈ S LMHom T → F Base S ∈ LSubSp ⁡ T
14 6 13 eqeltrrd ⊢ F ∈ S LMHom T → ran ⁡ F ∈ LSubSp ⁡ T