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