Definition df-nlfn

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

	Ref	Expression
Assertion	df-nlfn	$$⊢\mathrm{null}=\left(t\in \left({ℂ}^{\mathscr{H}}\right)⟼t^{-1}\left[\left\{0\right\}\right]\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnl	$$class\mathrm{null}$$
1		vt	$$setvart$$
2		cc	$$classℂ$$
3		cmap	$$class{\uparrow }_{𝑚}$$
4		chba	$$class\mathscr{H}$$
5	2 4 3	co	$$class\left({ℂ}^{\mathscr{H}}\right)$$
6	1	cv	$$setvart$$
7	6	ccnv	$$class{t}^{-1}$$
8		cc0	$$class0$$
9	8	csn	$$class\left\{0\right\}$$
10	7 9	cima	$$class{t}^{-1}\left[\left\{0\right\}\right]$$
11	1 5 10	cmpt	$$class\left(t\in \left({ℂ}^{\mathscr{H}}\right)⟼t^{-1}\left[\left\{0\right\}\right]\right)$$
12	0 11	wceq	$$wff\mathrm{null}=\left(t\in \left({ℂ}^{\mathscr{H}}\right)⟼t^{-1}\left[\left\{0\right\}\right]\right)$$