This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lmhmkerlss

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

Ref Expression
Hypotheses lmhmkerlss.k 
|- K = ( `' F " { .0. } )
lmhmkerlss.z 
|- .0. = ( 0g ` T )
lmhmkerlss.u 
|- U = ( LSubSp ` S )
Assertion lmhmkerlss 
|- ( F e. ( S LMHom T ) -> K e. U )

Proof

Step Hyp Ref Expression
1 lmhmkerlss.k 
 |-  K = ( `' F " { .0. } )
2 lmhmkerlss.z 
 |-  .0. = ( 0g ` T )
3 lmhmkerlss.u 
 |-  U = ( LSubSp ` S )
4 lmhmlmod2 
 |-  ( F e. ( S LMHom T ) -> T e. LMod )
5 eqid 
 |-  ( LSubSp ` T ) = ( LSubSp ` T )
6 2 5 lsssn0 
 |-  ( T e. LMod -> { .0. } e. ( LSubSp ` T ) )
7 4 6 syl 
 |-  ( F e. ( S LMHom T ) -> { .0. } e. ( LSubSp ` T ) )
8 3 5 lmhmpreima 
 |-  ( ( F e. ( S LMHom T ) /\ { .0. } e. ( LSubSp ` T ) ) -> ( `' F " { .0. } ) e. U )
9 7 8 mpdan 
 |-  ( F e. ( S LMHom T ) -> ( `' F " { .0. } ) e. U )
10 1 9 eqeltrid 
 |-  ( F e. ( S LMHom T ) -> K e. U )