Metamath Proof Explorer

Theorem elnlfn

Description: Membership in the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006) (Revised by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion elnlfn 
|- ( T : ~H --> CC -> ( A e. ( null ` T ) <-> ( A e. ~H /\ ( T ` A ) = 0 ) ) )

Proof

Step Hyp Ref Expression
1 nlfnval 
 |-  ( T : ~H --> CC -> ( null ` T ) = ( `' T " { 0 } ) )
2 cnvimass 
 |-  ( `' T " { 0 } ) C_ dom T
3 1 2 eqsstrdi 
 |-  ( T : ~H --> CC -> ( null ` T ) C_ dom T )
4 fdm 
 |-  ( T : ~H --> CC -> dom T = ~H )
5 3 4 sseqtrd 
 |-  ( T : ~H --> CC -> ( null ` T ) C_ ~H )
6 5 sseld 
 |-  ( T : ~H --> CC -> ( A e. ( null ` T ) -> A e. ~H ) )
7 6 pm4.71rd 
 |-  ( T : ~H --> CC -> ( A e. ( null ` T ) <-> ( A e. ~H /\ A e. ( null ` T ) ) ) )
8 1 eleq2d 
 |-  ( T : ~H --> CC -> ( A e. ( null ` T ) <-> A e. ( `' T " { 0 } ) ) )
9 8 adantr 
 |-  ( ( T : ~H --> CC /\ A e. ~H ) -> ( A e. ( null ` T ) <-> A e. ( `' T " { 0 } ) ) )
10 ffn 
 |-  ( T : ~H --> CC -> T Fn ~H )
11 eleq1 
 |-  ( x = A -> ( x e. ( `' T " { 0 } ) <-> A e. ( `' T " { 0 } ) ) )
12 fveqeq2 
 |-  ( x = A -> ( ( T ` x ) = 0 <-> ( T ` A ) = 0 ) )
13 11 12 bibi12d 
 |-  ( x = A -> ( ( x e. ( `' T " { 0 } ) <-> ( T ` x ) = 0 ) <-> ( A e. ( `' T " { 0 } ) <-> ( T ` A ) = 0 ) ) )
14 13 imbi2d 
 |-  ( x = A -> ( ( T Fn ~H -> ( x e. ( `' T " { 0 } ) <-> ( T ` x ) = 0 ) ) <-> ( T Fn ~H -> ( A e. ( `' T " { 0 } ) <-> ( T ` A ) = 0 ) ) ) )
15 0cn 
 |-  0 e. CC
16 vex 
 |-  x e. _V
17 16 eliniseg 
 |-  ( 0 e. CC -> ( x e. ( `' T " { 0 } ) <-> x T 0 ) )
18 15 17 ax-mp 
 |-  ( x e. ( `' T " { 0 } ) <-> x T 0 )
19 fnbrfvb 
 |-  ( ( T Fn ~H /\ x e. ~H ) -> ( ( T ` x ) = 0 <-> x T 0 ) )
20 18 19 bitr4id 
 |-  ( ( T Fn ~H /\ x e. ~H ) -> ( x e. ( `' T " { 0 } ) <-> ( T ` x ) = 0 ) )
21 20 expcom 
 |-  ( x e. ~H -> ( T Fn ~H -> ( x e. ( `' T " { 0 } ) <-> ( T ` x ) = 0 ) ) )
22 14 21 vtoclga 
 |-  ( A e. ~H -> ( T Fn ~H -> ( A e. ( `' T " { 0 } ) <-> ( T ` A ) = 0 ) ) )
23 10 22 mpan9 
 |-  ( ( T : ~H --> CC /\ A e. ~H ) -> ( A e. ( `' T " { 0 } ) <-> ( T ` A ) = 0 ) )
24 9 23 bitrd 
 |-  ( ( T : ~H --> CC /\ A e. ~H ) -> ( A e. ( null ` T ) <-> ( T ` A ) = 0 ) )
25 24 pm5.32da 
 |-  ( T : ~H --> CC -> ( ( A e. ~H /\ A e. ( null ` T ) ) <-> ( A e. ~H /\ ( T ` A ) = 0 ) ) )
26 7 25 bitrd 
 |-  ( T : ~H --> CC -> ( A e. ( null ` T ) <-> ( A e. ~H /\ ( T ` A ) = 0 ) ) )