Metamath Proof Explorer

Theorem nlelchi

Description: The null space of a continuous linear functional is a closed subspace. Remark 3.8 of Beran p. 103. (Contributed by NM, 11-Feb-2006) (Proof shortened by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses nlelch.1 
|- T e. LinFn
nlelch.2 
|- T e. ContFn
Assertion nlelchi 
|- ( null ` T ) e. CH

Proof

Step Hyp Ref Expression
1 nlelch.1 
 |-  T e. LinFn
2 nlelch.2 
 |-  T e. ContFn
3 1 nlelshi 
 |-  ( null ` T ) e. SH
4 vex 
 |-  x e. _V
5 4 hlimveci 
 |-  ( f ~~>v x -> x e. ~H )
6 5 adantl 
 |-  ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) -> x e. ~H )
7 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
8 7 cnfldhaus 
 |-  ( TopOpen ` CCfld ) e. Haus
9 8 a1i 
 |-  ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) -> ( TopOpen ` CCfld ) e. Haus )
10 eqid 
 |-  <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.
11 eqid 
 |-  ( normh o. -h ) = ( normh o. -h )
12 10 11 hhims 
 |-  ( normh o. -h ) = ( IndMet ` <. <. +h , .h >. , normh >. )
13 eqid 
 |-  ( MetOpen ` ( normh o. -h ) ) = ( MetOpen ` ( normh o. -h ) )
14 10 12 13 hhlm 
 |-  ~~>v = ( ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) |` ( ~H ^m NN ) )
15 resss 
 |-  ( ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) |` ( ~H ^m NN ) ) C_ ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) )
16 14 15 eqsstri 
 |-  ~~>v C_ ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) )
17 16 ssbri 
 |-  ( f ~~>v x -> f ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) x )
18 17 adantl 
 |-  ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) -> f ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) x )
19 11 13 7 hhcnf 
 |-  ContFn = ( ( MetOpen ` ( normh o. -h ) ) Cn ( TopOpen ` CCfld ) )
20 2 19 eleqtri 
 |-  T e. ( ( MetOpen ` ( normh o. -h ) ) Cn ( TopOpen ` CCfld ) )
21 20 a1i 
 |-  ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) -> T e. ( ( MetOpen ` ( normh o. -h ) ) Cn ( TopOpen ` CCfld ) ) )
22 18 21 lmcn 
 |-  ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) -> ( T o. f ) ( ~~>t ` ( TopOpen ` CCfld ) ) ( T ` x ) )
23 1 lnfnfi 
 |-  T : ~H --> CC
24 ffvelrn 
 |-  ( ( f : NN --> ( null ` T ) /\ n e. NN ) -> ( f ` n ) e. ( null ` T ) )
25 24 adantlr 
 |-  ( ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) /\ n e. NN ) -> ( f ` n ) e. ( null ` T ) )
26 elnlfn2 
 |-  ( ( T : ~H --> CC /\ ( f ` n ) e. ( null ` T ) ) -> ( T ` ( f ` n ) ) = 0 )
27 23 25 26 sylancr 
 |-  ( ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) /\ n e. NN ) -> ( T ` ( f ` n ) ) = 0 )
28 fvco3 
 |-  ( ( f : NN --> ( null ` T ) /\ n e. NN ) -> ( ( T o. f ) ` n ) = ( T ` ( f ` n ) ) )
29 28 adantlr 
 |-  ( ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) /\ n e. NN ) -> ( ( T o. f ) ` n ) = ( T ` ( f ` n ) ) )
30 c0ex 
 |-  0 e. _V
31 30 fvconst2 
 |-  ( n e. NN -> ( ( NN X. { 0 } ) ` n ) = 0 )
32 31 adantl 
 |-  ( ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) /\ n e. NN ) -> ( ( NN X. { 0 } ) ` n ) = 0 )
33 27 29 32 3eqtr4d 
 |-  ( ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) /\ n e. NN ) -> ( ( T o. f ) ` n ) = ( ( NN X. { 0 } ) ` n ) )
34 33 ralrimiva 
 |-  ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) -> A. n e. NN ( ( T o. f ) ` n ) = ( ( NN X. { 0 } ) ` n ) )
35 ffn 
 |-  ( T : ~H --> CC -> T Fn ~H )
36 23 35 ax-mp 
 |-  T Fn ~H
37 simpl 
 |-  ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) -> f : NN --> ( null ` T ) )
38 3 shssii 
 |-  ( null ` T ) C_ ~H
39 fss 
 |-  ( ( f : NN --> ( null ` T ) /\ ( null ` T ) C_ ~H ) -> f : NN --> ~H )
40 37 38 39 sylancl 
 |-  ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) -> f : NN --> ~H )
41 fnfco 
 |-  ( ( T Fn ~H /\ f : NN --> ~H ) -> ( T o. f ) Fn NN )
42 36 40 41 sylancr 
 |-  ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) -> ( T o. f ) Fn NN )
43 30 fconst 
 |-  ( NN X. { 0 } ) : NN --> { 0 }
44 ffn 
 |-  ( ( NN X. { 0 } ) : NN --> { 0 } -> ( NN X. { 0 } ) Fn NN )
45 43 44 ax-mp 
 |-  ( NN X. { 0 } ) Fn NN
46 eqfnfv 
 |-  ( ( ( T o. f ) Fn NN /\ ( NN X. { 0 } ) Fn NN ) -> ( ( T o. f ) = ( NN X. { 0 } ) <-> A. n e. NN ( ( T o. f ) ` n ) = ( ( NN X. { 0 } ) ` n ) ) )
47 42 45 46 sylancl 
 |-  ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) -> ( ( T o. f ) = ( NN X. { 0 } ) <-> A. n e. NN ( ( T o. f ) ` n ) = ( ( NN X. { 0 } ) ` n ) ) )
48 34 47 mpbird 
 |-  ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) -> ( T o. f ) = ( NN X. { 0 } ) )
49 7 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
50 49 a1i 
 |-  ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
51 0cnd 
 |-  ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) -> 0 e. CC )
52 1zzd 
 |-  ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) -> 1 e. ZZ )
53 nnuz 
 |-  NN = ( ZZ>= ` 1 )
54 53 lmconst 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ 0 e. CC /\ 1 e. ZZ ) -> ( NN X. { 0 } ) ( ~~>t ` ( TopOpen ` CCfld ) ) 0 )
55 50 51 52 54 syl3anc 
 |-  ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) -> ( NN X. { 0 } ) ( ~~>t ` ( TopOpen ` CCfld ) ) 0 )
56 48 55 eqbrtrd 
 |-  ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) -> ( T o. f ) ( ~~>t ` ( TopOpen ` CCfld ) ) 0 )
57 9 22 56 lmmo 
 |-  ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) -> ( T ` x ) = 0 )
58 elnlfn 
 |-  ( T : ~H --> CC -> ( x e. ( null ` T ) <-> ( x e. ~H /\ ( T ` x ) = 0 ) ) )
59 23 58 ax-mp 
 |-  ( x e. ( null ` T ) <-> ( x e. ~H /\ ( T ` x ) = 0 ) )
60 6 57 59 sylanbrc 
 |-  ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) -> x e. ( null ` T ) )
61 60 gen2 
 |-  A. f A. x ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) -> x e. ( null ` T ) )
62 isch2 
 |-  ( ( null ` T ) e. CH <-> ( ( null ` T ) e. SH /\ A. f A. x ( ( f : NN --> ( null ` T ) /\ f ~~>v x ) -> x e. ( null ` T ) ) ) )
63 3 61 62 mpbir2an 
 |-  ( null ` T ) e. CH