lmhmkerlss

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

Step	Hyp	Ref	Expression
1		lmhmkerlss.k	$⊢ K = F^{-1} [\{\underset{˙}{0}\}]$
2		lmhmkerlss.z	$⊢ \underset{˙}{0} = 0_{T}$
3		lmhmkerlss.u	$⊢ U = LSubSp (S)$
4		lmhmlmod2	$⊢ F \in (S LMHom T) \to T \in LMod$
5		eqid	$⊢ LSubSp (T) = LSubSp (T)$
6	2 5	lsssn0	$⊢ T \in LMod \to \{\underset{˙}{0}\} \in LSubSp (T)$
7	4 6	syl	$⊢ F \in (S LMHom T) \to \{\underset{˙}{0}\} \in LSubSp (T)$
8	3 5	lmhmpreima	$⊢ (F \in (S LMHom T) \land \{\underset{˙}{0}\} \in LSubSp (T)) \to F^{-1} [\{\underset{˙}{0}\}] \in U$
9	7 8	mpdan	$⊢ F \in (S LMHom T) \to F^{-1} [\{\underset{˙}{0}\}] \in U$
10	1 9	eqeltrid	$⊢ F \in (S LMHom T) \to K \in U$

Metamath Proof Explorer