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 ‘ 𝑈 )
	kerlmhm.k	⊢ 𝐾 = ( 𝑉 ↾s ( ◡ 𝐹 “ { 0 } ) )
Assertion	kerlmhm	⊢ ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) → 𝐾 ∈ LVec )

Proof

Step	Hyp	Ref	Expression
1		kerlmhm.1	⊢ 0 = ( 0g ‘ 𝑈 )
2		kerlmhm.k	⊢ 𝐾 = ( 𝑉 ↾s ( ◡ 𝐹 “ { 0 } ) )
3		eqid	⊢ ( ◡ 𝐹 “ { 0 } ) = ( ◡ 𝐹 “ { 0 } )
4		eqid	⊢ ( LSubSp ‘ 𝑉 ) = ( LSubSp ‘ 𝑉 )
5	3 1 4	lmhmkerlss	⊢ ( 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) → ( ◡ 𝐹 “ { 0 } ) ∈ ( LSubSp ‘ 𝑉 ) )
6	2 4	lsslvec	⊢ ( ( 𝑉 ∈ LVec ∧ ( ◡ 𝐹 “ { 0 } ) ∈ ( LSubSp ‘ 𝑉 ) ) → 𝐾 ∈ LVec )
7	5 6	sylan2	⊢ ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) → 𝐾 ∈ LVec )