Theorem ellkr

Description: Membership in the kernel of a functional. ( elnlfn analog.) (Contributed by NM, 16-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	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)=\underset{\dot{}}{0}\right)\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	2 3 4 5	lkrval	$$⊢\left(W\in Y\wedge G\in F\right)\to K\left(G\right)=G^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$
7	6	eleq2d	$$⊢\left(W\in Y\wedge G\in F\right)\to \left(X\in K\left(G\right)\leftrightarrow X\in G^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\right)$$
8		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
9	2 8 1 4	lflf	$$⊢\left(W\in Y\wedge G\in F\right)\to G:V⟶{\mathrm{Base}}_D$$
10		ffn	$$⊢G:V⟶{\mathrm{Base}}_D\to GFnV$$
11		elpreima	$$⊢GFnV\to \left(X\in G^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\leftrightarrow \left(X\in V\wedge G\left(X\right)\in \left\{\underset{\dot{}}{0}\right\}\right)\right)$$
12	9 10 11	3syl	$$⊢\left(W\in Y\wedge G\in F\right)\to \left(X\in G^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\leftrightarrow \left(X\in V\wedge G\left(X\right)\in \left\{\underset{\dot{}}{0}\right\}\right)\right)$$
13		fvex	$$⊢G\left(X\right)\in \mathrm{V}$$
14	13	elsn	$$⊢G\left(X\right)\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow G\left(X\right)=\underset{\dot{}}{0}$$
15	14	anbi2i	$$⊢\left(X\in V\wedge G\left(X\right)\in \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(X\in V\wedge G\left(X\right)=\underset{\dot{}}{0}\right)$$
16	12 15	bitrdi	$$⊢\left(W\in Y\wedge G\in F\right)\to \left(X\in G^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\leftrightarrow \left(X\in V\wedge G\left(X\right)=\underset{\dot{}}{0}\right)\right)$$
17	7 16	bitrd	$$⊢\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)=\underset{\dot{}}{0}\right)\right)$$