Theorem lkrf0

Description: The value of a functional at a member of its kernel is zero. (Contributed by NM, 16-Apr-2014)

	Ref	Expression
Hypotheses	lkrf0.d	$$⊢D=\mathrm{Scalar}\left(W\right)$$
	lkrf0.o	$$⊢\underset{\dot{}}{0}=0_D$$
	lkrf0.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	lkrf0.k	$$⊢K=\mathrm{LKer}\left(W\right)$$
Assertion	lkrf0	$$⊢\left(W\in Y\wedge G\in F\wedge X\in K\left(G\right)\right)\to G\left(X\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		lkrf0.d	$$⊢D=\mathrm{Scalar}\left(W\right)$$
2		lkrf0.o	$$⊢\underset{\dot{}}{0}=0_D$$
3		lkrf0.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
4		lkrf0.k	$$⊢K=\mathrm{LKer}\left(W\right)$$
5		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
6	5 1 2 3 4	ellkr	$$⊢\left(W\in Y\wedge G\in F\right)\to \left(X\in K\left(G\right)\leftrightarrow \left(X\in {\mathrm{Base}}_W\wedge G\left(X\right)=\underset{\dot{}}{0}\right)\right)$$
7	6	simplbda	$$⊢\left(\left(W\in Y\wedge G\in F\right)\wedge X\in K\left(G\right)\right)\to G\left(X\right)=\underset{\dot{}}{0}$$
8	7	3impa	$$⊢\left(W\in Y\wedge G\in F\wedge X\in K\left(G\right)\right)\to G\left(X\right)=\underset{\dot{}}{0}$$