This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } ) )