Theorem lkrval2

Description: Value of the kernel of a functional. (Contributed by NM, 15-Apr-2014)

	Ref	Expression
Hypotheses	lkrfval2.v	$$⊢V={\mathrm{Base}}_W$$
	lkrfval2.d	$$⊢D=\mathrm{Scalar}\left(W\right)$$
	lkrfval2.o	$$⊢\underset{\dot{}}{0}=0_D$$
	lkrfval2.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	lkrfval2.k	$$⊢K=\mathrm{LKer}\left(W\right)$$
Assertion	lkrval2	$$⊢\left(W\in X\wedge G\in F\right)\to K\left(G\right)=\left\{x\in V|G\left(x\right)=\underset{\dot{}}{0}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		lkrfval2.v	$$⊢V={\mathrm{Base}}_W$$
2		lkrfval2.d	$$⊢D=\mathrm{Scalar}\left(W\right)$$
3		lkrfval2.o	$$⊢\underset{\dot{}}{0}=0_D$$
4		lkrfval2.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
5		lkrfval2.k	$$⊢K=\mathrm{LKer}\left(W\right)$$
6		elex	$$⊢W\in X\to W\in \mathrm{V}$$
7	1 2 3 4 5	ellkr	$$⊢\left(W\in \mathrm{V}\wedge G\in F\right)\to \left(x\in K\left(G\right)\leftrightarrow \left(x\in V\wedge G\left(x\right)=\underset{\dot{}}{0}\right)\right)$$
8	7	eqabdv	$$⊢\left(W\in \mathrm{V}\wedge G\in F\right)\to K\left(G\right)=\left\{x|\left(x\in V\wedge G\left(x\right)=\underset{\dot{}}{0}\right)\right\}$$
9		df-rab	$$⊢\left\{x\in V|G\left(x\right)=\underset{\dot{}}{0}\right\}=\left\{x|\left(x\in V\wedge G\left(x\right)=\underset{\dot{}}{0}\right)\right\}$$
10	8 9	eqtr4di	$$⊢\left(W\in \mathrm{V}\wedge G\in F\right)\to K\left(G\right)=\left\{x\in V|G\left(x\right)=\underset{\dot{}}{0}\right\}$$
11	6 10	sylan	$$⊢\left(W\in X\wedge G\in F\right)\to K\left(G\right)=\left\{x\in V|G\left(x\right)=\underset{\dot{}}{0}\right\}$$