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 e. ( S LMHom T ) -> ran F e. ( LSubSp ` T ) )

Proof

Step Hyp Ref Expression
1 eqid
 |-  ( Base ` S ) = ( Base ` S )
2 eqid
 |-  ( Base ` T ) = ( Base ` T )
3 1 2 lmhmf
 |-  ( F e. ( 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 e. ( S LMHom T ) -> ( F " ( Base ` S ) ) = ran F )
7 lmhmlmod1
 |-  ( F e. ( S LMHom T ) -> S e. LMod )
8 eqid
 |-  ( LSubSp ` S ) = ( LSubSp ` S )
9 1 8 lss1
 |-  ( S e. LMod -> ( Base ` S ) e. ( LSubSp ` S ) )
10 7 9 syl
 |-  ( F e. ( S LMHom T ) -> ( Base ` S ) e. ( LSubSp ` S ) )
11 eqid
 |-  ( LSubSp ` T ) = ( LSubSp ` T )
12 8 11 lmhmima
 |-  ( ( F e. ( S LMHom T ) /\ ( Base ` S ) e. ( LSubSp ` S ) ) -> ( F " ( Base ` S ) ) e. ( LSubSp ` T ) )
13 10 12 mpdan
 |-  ( F e. ( S LMHom T ) -> ( F " ( Base ` S ) ) e. ( LSubSp ` T ) )
14 6 13 eqeltrrd
 |-  ( F e. ( S LMHom T ) -> ran F e. ( LSubSp ` T ) )