Theorem lmhmkerlss

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

	Ref	Expression
Hypotheses	lmhmkerlss.k	$$⊢K=F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$
	lmhmkerlss.z	$$⊢\underset{\dot{}}{0}=0_T$$
	lmhmkerlss.u	$$⊢U=\mathrm{LSubSp}\left(S\right)$$
Assertion	lmhmkerlss	$$⊢F\in \left(S\mathrm{LMHom}T\right)\to K\in U$$

Proof

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