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	⊢ null = ( 𝑡 ∈ ( ℂ ↑m ℋ ) ↦ ( ◡ 𝑡 “ { 0 } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnl	⊢ null
1		vt	⊢ 𝑡
2		cc	⊢ ℂ
3		cmap	⊢ ↑m
4		chba	⊢ ℋ
5	2 4 3	co	⊢ ( ℂ ↑m ℋ )
6	1	cv	⊢ 𝑡
7	6	ccnv	⊢ ◡ 𝑡
8		cc0	⊢ 0
9	8	csn	⊢ { 0 }
10	7 9	cima	⊢ ( ◡ 𝑡 “ { 0 } )
11	1 5 10	cmpt	⊢ ( 𝑡 ∈ ( ℂ ↑m ℋ ) ↦ ( ◡ 𝑡 “ { 0 } ) )
12	0 11	wceq	⊢ null = ( 𝑡 ∈ ( ℂ ↑m ℋ ) ↦ ( ◡ 𝑡 “ { 0 } ) )