Theorem lkrfval

Description: The kernel of a functional. (Contributed by NM, 15-Apr-2014) (Revised by Mario Carneiro, 24-Jun-2014)

	Ref	Expression
Hypotheses	lkrfval.d	$$⊢D=\mathrm{Scalar}\left(W\right)$$
	lkrfval.o	$$⊢\underset{\dot{}}{0}=0_D$$
	lkrfval.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	lkrfval.k	$$⊢K=\mathrm{LKer}\left(W\right)$$
Assertion	lkrfval	$$⊢W\in X\to K=\left(f\in F⟼f^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\right)$$

Proof

Step	Hyp	Ref	Expression
1		lkrfval.d	$$⊢D=\mathrm{Scalar}\left(W\right)$$
2		lkrfval.o	$$⊢\underset{\dot{}}{0}=0_D$$
3		lkrfval.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
4		lkrfval.k	$$⊢K=\mathrm{LKer}\left(W\right)$$
5		elex	$$⊢W\in X\to W\in \mathrm{V}$$
6		fveq2	$$⊢w=W\to \mathrm{LFnl}\left(w\right)=\mathrm{LFnl}\left(W\right)$$
7	6 3	eqtr4di	$$⊢w=W\to \mathrm{LFnl}\left(w\right)=F$$
8		fveq2	$$⊢w=W\to \mathrm{Scalar}\left(w\right)=\mathrm{Scalar}\left(W\right)$$
9	8 1	eqtr4di	$$⊢w=W\to \mathrm{Scalar}\left(w\right)=D$$
10	9	fveq2d	$$⊢w=W\to 0_{\mathrm{Scalar}\left(w\right)}=0_D$$
11	10 2	eqtr4di	$$⊢w=W\to 0_{\mathrm{Scalar}\left(w\right)}=\underset{\dot{}}{0}$$
12	11	sneqd	$$⊢w=W\to \left\{0_{\mathrm{Scalar}\left(w\right)}\right\}=\left\{\underset{\dot{}}{0}\right\}$$
13	12	imaeq2d	$$⊢w=W\to f^{-1}\left[\left\{0_{\mathrm{Scalar}\left(w\right)}\right\}\right]=f^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$
14	7 13	mpteq12dv	$$⊢w=W\to \left(f\in \mathrm{LFnl}\left(w\right)⟼f^{-1}\left[\left\{0_{\mathrm{Scalar}\left(w\right)}\right\}\right]\right)=\left(f\in F⟼f^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\right)$$
15		df-lkr	$$⊢\mathrm{LKer}=\left(w\in \mathrm{V}⟼\left(f\in \mathrm{LFnl}\left(w\right)⟼f^{-1}\left[\left\{0_{\mathrm{Scalar}\left(w\right)}\right\}\right]\right)\right)$$
16	14 15 3	mptfvmpt	$$⊢W\in \mathrm{V}\to \mathrm{LKer}\left(W\right)=\left(f\in F⟼f^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\right)$$
17	4 16	syl5eq	$$⊢W\in \mathrm{V}\to K=\left(f\in F⟼f^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\right)$$
18	5 17	syl	$$⊢W\in X\to K=\left(f\in F⟼f^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\right)$$