Theorem lkrval

Description: Value of the kernel of a functional. (Contributed by NM, 15-Apr-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	lkrval	$$⊢\left(W\in X\wedge G\in F\right)\to K\left(G\right)=G^{-1}\left[\left\{\underset{\dot{}}{0}\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	1 2 3 4	lkrfval	$$⊢W\in X\to K=\left(f\in F⟼f^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\right)$$
6	5	fveq1d	$$⊢W\in X\to K\left(G\right)=\left(f\in F⟼f^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\right)\left(G\right)$$
7		cnvexg	$$⊢G\in F\to G^{-1}\in \mathrm{V}$$
8		imaexg	$$⊢G^{-1}\in \mathrm{V}\to G^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{V}$$
9	7 8	syl	$$⊢G\in F\to G^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{V}$$
10		cnveq	$$⊢f=G\to f^{-1}=G^{-1}$$
11	10	imaeq1d	$$⊢f=G\to f^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]=G^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$
12		eqid	$$⊢\left(f\in F⟼f^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\right)=\left(f\in F⟼f^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\right)$$
13	11 12	fvmptg	$$⊢\left(G\in F\wedge G^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{V}\right)\to \left(f\in F⟼f^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\right)\left(G\right)=G^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$
14	9 13	mpdan	$$⊢G\in F\to \left(f\in F⟼f^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\right)\left(G\right)=G^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$
15	6 14	sylan9eq	$$⊢\left(W\in X\wedge G\in F\right)\to K\left(G\right)=G^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$