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 ⊢ 𝐾 = ( ◡ 𝐹 “ { 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 𝑇 ) → 𝐾 ∈ 𝑈 )