Theorem lmhmkerlss

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

	Ref	Expression
Hypotheses	lmhmkerlss.k	⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
	lmhmkerlss.z	⊢ 0 = ( 0g ‘ 𝑇 )
	lmhmkerlss.u	⊢ 𝑈 = ( LSubSp ‘ 𝑆 )
Assertion	lmhmkerlss	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐾 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		lmhmkerlss.k	⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
2		lmhmkerlss.z	⊢ 0 = ( 0g ‘ 𝑇 )
3		lmhmkerlss.u	⊢ 𝑈 = ( LSubSp ‘ 𝑆 )
4		lmhmlmod2	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑇 ∈ LMod )
5		eqid	⊢ ( LSubSp ‘ 𝑇 ) = ( LSubSp ‘ 𝑇 )
6	2 5	lsssn0	⊢ ( 𝑇 ∈ LMod → { 0 } ∈ ( LSubSp ‘ 𝑇 ) )
7	4 6	syl	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → { 0 } ∈ ( LSubSp ‘ 𝑇 ) )
8	3 5	lmhmpreima	⊢ ( ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ { 0 } ∈ ( LSubSp ‘ 𝑇 ) ) → ( ◡ 𝐹 “ { 0 } ) ∈ 𝑈 )
9	7 8	mpdan	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → ( ◡ 𝐹 “ { 0 } ) ∈ 𝑈 )
10	1 9	eqeltrid	⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐾 ∈ 𝑈 )