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	$$⊢\underset{\dot{}}{0}=0_U$$
	kerlmhm.k	$$⊢K=V{\upharpoonright }_{𝑠}{F}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$
Assertion	kerlmhm	$$⊢\left(V\in \mathrm{LVec}\wedge F\in \left(V\mathrm{LMHom}U\right)\right)\to K\in \mathrm{LVec}$$

Proof

Step	Hyp	Ref	Expression
1		kerlmhm.1	$$⊢\underset{\dot{}}{0}=0_U$$
2		kerlmhm.k	$$⊢K=V{\upharpoonright }_{𝑠}{F}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$
3		eqid	$$⊢F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]=F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$
4		eqid	$$⊢\mathrm{LSubSp}\left(V\right)=\mathrm{LSubSp}\left(V\right)$$
5	3 1 4	lmhmkerlss	$$⊢F\in \left(V\mathrm{LMHom}U\right)\to F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{LSubSp}\left(V\right)$$
6	2 4	lsslvec	$$⊢\left(V\in \mathrm{LVec}\wedge F^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{LSubSp}\left(V\right)\right)\to K\in \mathrm{LVec}$$
7	5 6	sylan2	$$⊢\left(V\in \mathrm{LVec}\wedge F\in \left(V\mathrm{LMHom}U\right)\right)\to K\in \mathrm{LVec}$$