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 = ( t e. ( CC ^m ~H ) |-> ( `' t " { 0 } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnl 
 |-  null
1 vt 
 |-  t
2 cc 
 |-  CC
3 cmap 
 |-  ^m
4 chba 
 |-  ~H
5 2 4 3 co 
 |-  ( CC ^m ~H )
6 1 cv 
 |-  t
7 6 ccnv 
 |-  `' t
8 cc0 
 |-  0
9 8 csn 
 |-  { 0 }
10 7 9 cima 
 |-  ( `' t " { 0 } )
11 1 5 10 cmpt 
 |-  ( t e. ( CC ^m ~H ) |-> ( `' t " { 0 } ) )
12 0 11 wceq 
 |-  null = ( t e. ( CC ^m ~H ) |-> ( `' t " { 0 } ) )