Theorem lkrcl

Description: A member of the kernel of a functional is a vector. (Contributed by NM, 16-Apr-2014)

	Ref	Expression
Hypotheses	lkrcl.v	$$⊢V={\mathrm{Base}}_W$$
	lkrcl.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	lkrcl.k	$$⊢K=\mathrm{LKer}\left(W\right)$$
Assertion	lkrcl	$$⊢\left(W\in Y\wedge G\in F\wedge X\in K\left(G\right)\right)\to X\in V$$

Proof

Step	Hyp	Ref	Expression
1		lkrcl.v	$$⊢V={\mathrm{Base}}_W$$
2		lkrcl.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
3		lkrcl.k	$$⊢K=\mathrm{LKer}\left(W\right)$$
4		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
5		eqid	$$⊢0_{\mathrm{Scalar}\left(W\right)}=0_{\mathrm{Scalar}\left(W\right)}$$
6	1 4 5 2 3	ellkr	$$⊢\left(W\in Y\wedge G\in F\right)\to \left(X\in K\left(G\right)\leftrightarrow \left(X\in V\wedge G\left(X\right)=0_{\mathrm{Scalar}\left(W\right)}\right)\right)$$
7	6	simprbda	$$⊢\left(\left(W\in Y\wedge G\in F\right)\wedge X\in K\left(G\right)\right)\to X\in V$$
8	7	3impa	$$⊢\left(W\in Y\wedge G\in F\wedge X\in K\left(G\right)\right)\to X\in V$$