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 )