Theorem nlfnval

Description: Value of the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nlfnval	$$⊢T:\mathscr{H}⟶ℂ\to \mathrm{null}\left(T\right)=T^{-1}\left[\left\{0\right\}\right]$$

Proof

Step	Hyp	Ref	Expression
1		cnex	$$⊢ℂ\in \mathrm{V}$$
2		ax-hilex	$$⊢\mathscr{H}\in \mathrm{V}$$
3	1 2	elmap	$$⊢T\in \left({ℂ}^{\mathscr{H}}\right)\leftrightarrow T:\mathscr{H}⟶ℂ$$
4		cnvexg	$$⊢T\in \left({ℂ}^{\mathscr{H}}\right)\to T^{-1}\in \mathrm{V}$$
5		imaexg	$$⊢T^{-1}\in \mathrm{V}\to T^{-1}\left[\left\{0\right\}\right]\in \mathrm{V}$$
6	4 5	syl	$$⊢T\in \left({ℂ}^{\mathscr{H}}\right)\to T^{-1}\left[\left\{0\right\}\right]\in \mathrm{V}$$
7		cnveq	$$⊢t=T\to t^{-1}=T^{-1}$$
8	7	imaeq1d	$$⊢t=T\to t^{-1}\left[\left\{0\right\}\right]=T^{-1}\left[\left\{0\right\}\right]$$
9		df-nlfn	$$⊢\mathrm{null}=\left(t\in \left({ℂ}^{\mathscr{H}}\right)⟼t^{-1}\left[\left\{0\right\}\right]\right)$$
10	8 9	fvmptg	$$⊢\left(T\in \left({ℂ}^{\mathscr{H}}\right)\wedge T^{-1}\left[\left\{0\right\}\right]\in \mathrm{V}\right)\to \mathrm{null}\left(T\right)=T^{-1}\left[\left\{0\right\}\right]$$
11	6 10	mpdan	$$⊢T\in \left({ℂ}^{\mathscr{H}}\right)\to \mathrm{null}\left(T\right)=T^{-1}\left[\left\{0\right\}\right]$$
12	3 11	sylbir	$$⊢T:\mathscr{H}⟶ℂ\to \mathrm{null}\left(T\right)=T^{-1}\left[\left\{0\right\}\right]$$