Theorem kerlmhm

Description: The kernel of a vector space homomorphism is a vector space itself. (Contributed by Thierry Arnoux, 7-May-2023)

	Ref	Expression
Hypotheses	kerlmhm.1	|- .0. = ( 0g ` U )
	kerlmhm.k	|- K = ( V |`s ( `' F " { .0. } ) )
Assertion	kerlmhm	|- ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> K e. LVec )

Proof

Step	Hyp	Ref	Expression
1		kerlmhm.1	|- .0. = ( 0g ` U )
2		kerlmhm.k	|- K = ( V |`s ( `' F " { .0. } ) )
3		eqid	|- ( `' F " { .0. } ) = ( `' F " { .0. } )
4		eqid	|- ( LSubSp ` V ) = ( LSubSp ` V )
5	3 1 4	lmhmkerlss	|- ( F e. ( V LMHom U ) -> ( `' F " { .0. } ) e. ( LSubSp ` V ) )
6	2 4	lsslvec	|- ( ( V e. LVec /\ ( `' F " { .0. } ) e. ( LSubSp ` V ) ) -> K e. LVec )
7	5 6	sylan2	|- ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> K e. LVec )