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 ) )