Theorem ellkr2

Description: Membership in the kernel of a functional. (Contributed by NM, 12-Jan-2015)

	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)$$
	ellkr2.w	$$⊢\phi \to W\in Y$$
	ellkr2.g	$$⊢\phi \to G\in F$$
	ellkr2.x	$$⊢\phi \to X\in V$$
Assertion	ellkr2	$$⊢\phi \to \left(X\in K\left(G\right)\leftrightarrow 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		ellkr2.w	$$⊢\phi \to W\in Y$$
7		ellkr2.g	$$⊢\phi \to G\in F$$
8		ellkr2.x	$$⊢\phi \to X\in V$$
9	1 2 3 4 5	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)$$
10	6 7 9	syl2anc	$$⊢\phi \to \left(X\in K\left(G\right)\leftrightarrow \left(X\in V\wedge G\left(X\right)=\underset{\dot{}}{0}\right)\right)$$
11	8	biantrurd	$$⊢\phi \to \left(G\left(X\right)=\underset{\dot{}}{0}\leftrightarrow \left(X\in V\wedge G\left(X\right)=\underset{\dot{}}{0}\right)\right)$$
12	10 11	bitr4d	$$⊢\phi \to \left(X\in K\left(G\right)\leftrightarrow G\left(X\right)=\underset{\dot{}}{0}\right)$$