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

Metamath Proof Explorer

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 : ~H --> CC -> ( null ` T ) = ( `' T " { 0 } ) )

Proof

Step Hyp Ref Expression
1 cnex 
 |-  CC e. _V
2 ax-hilex 
 |-  ~H e. _V
3 1 2 elmap 
 |-  ( T e. ( CC ^m ~H ) <-> T : ~H --> CC )
4 cnvexg 
 |-  ( T e. ( CC ^m ~H ) -> `' T e. _V )
5 imaexg 
 |-  ( `' T e. _V -> ( `' T " { 0 } ) e. _V )
6 4 5 syl 
 |-  ( T e. ( CC ^m ~H ) -> ( `' T " { 0 } ) e. _V )
7 cnveq 
 |-  ( t = T -> `' t = `' T )
8 7 imaeq1d 
 |-  ( t = T -> ( `' t " { 0 } ) = ( `' T " { 0 } ) )
9 df-nlfn 
 |-  null = ( t e. ( CC ^m ~H ) |-> ( `' t " { 0 } ) )
10 8 9 fvmptg 
 |-  ( ( T e. ( CC ^m ~H ) /\ ( `' T " { 0 } ) e. _V ) -> ( null ` T ) = ( `' T " { 0 } ) )
11 6 10 mpdan 
 |-  ( T e. ( CC ^m ~H ) -> ( null ` T ) = ( `' T " { 0 } ) )
12 3 11 sylbir 
 |-  ( T : ~H --> CC -> ( null ` T ) = ( `' T " { 0 } ) )