Theorem lkrssv

Description: The kernel of a linear functional is a set of vectors. (Contributed by NM, 1-Jan-2015)

	Ref	Expression
Hypotheses	lkrssv.v	$$⊢V={\mathrm{Base}}_W$$
	lkrssv.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	lkrssv.k	$$⊢K=\mathrm{LKer}\left(W\right)$$
	lkrssv.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lkrssv.g	$$⊢\phi \to G\in F$$
Assertion	lkrssv	$$⊢\phi \to K\left(G\right)\subseteq V$$

Proof

Step	Hyp	Ref	Expression
1		lkrssv.v	$$⊢V={\mathrm{Base}}_W$$
2		lkrssv.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
3		lkrssv.k	$$⊢K=\mathrm{LKer}\left(W\right)$$
4		lkrssv.w	$$⊢\phi \to W\in \mathrm{LMod}$$
5		lkrssv.g	$$⊢\phi \to G\in F$$
6		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
7	2 3 6	lkrlss	$$⊢\left(W\in \mathrm{LMod}\wedge G\in F\right)\to K\left(G\right)\in \mathrm{LSubSp}\left(W\right)$$
8	4 5 7	syl2anc	$$⊢\phi \to K\left(G\right)\in \mathrm{LSubSp}\left(W\right)$$
9	1 6	lssss	$$⊢K\left(G\right)\in \mathrm{LSubSp}\left(W\right)\to K\left(G\right)\subseteq V$$
10	8 9	syl	$$⊢\phi \to K\left(G\right)\subseteq V$$