Metamath Proof Explorer

Theorem hlim0

Description: The zero sequence in Hilbert space converges to the zero vector. (Contributed by NM, 17-Aug-1999) (Proof shortened by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Assertion hlim0 
|- ( NN X. { 0h } ) ~~>v 0h

Proof

Step Hyp Ref Expression
1 ax-hv0cl 
 |-  0h e. ~H
2 1 fconst6 
 |-  ( NN X. { 0h } ) : NN --> ~H
3 ax-hilex 
 |-  ~H e. _V
4 nnex 
 |-  NN e. _V
5 3 4 elmap 
 |-  ( ( NN X. { 0h } ) e. ( ~H ^m NN ) <-> ( NN X. { 0h } ) : NN --> ~H )
6 2 5 mpbir 
 |-  ( NN X. { 0h } ) e. ( ~H ^m NN )
7 eqid 
 |-  <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.
8 eqid 
 |-  ( IndMet ` <. <. +h , .h >. , normh >. ) = ( IndMet ` <. <. +h , .h >. , normh >. )
9 7 8 hhxmet 
 |-  ( IndMet ` <. <. +h , .h >. , normh >. ) e. ( *Met ` ~H )
10 eqid 
 |-  ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) = ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) )
11 10 mopntopon 
 |-  ( ( IndMet ` <. <. +h , .h >. , normh >. ) e. ( *Met ` ~H ) -> ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) e. ( TopOn ` ~H ) )
12 9 11 ax-mp 
 |-  ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) e. ( TopOn ` ~H )
13 1z 
 |-  1 e. ZZ
14 nnuz 
 |-  NN = ( ZZ>= ` 1 )
15 14 lmconst 
 |-  ( ( ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) e. ( TopOn ` ~H ) /\ 0h e. ~H /\ 1 e. ZZ ) -> ( NN X. { 0h } ) ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) 0h )
16 12 1 13 15 mp3an 
 |-  ( NN X. { 0h } ) ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) 0h
17 7 8 10 hhlm 
 |-  ~~>v = ( ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) |` ( ~H ^m NN ) )
18 17 breqi 
 |-  ( ( NN X. { 0h } ) ~~>v 0h <-> ( NN X. { 0h } ) ( ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) |` ( ~H ^m NN ) ) 0h )
19 1 elexi 
 |-  0h e. _V
20 19 brresi 
 |-  ( ( NN X. { 0h } ) ( ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) |` ( ~H ^m NN ) ) 0h <-> ( ( NN X. { 0h } ) e. ( ~H ^m NN ) /\ ( NN X. { 0h } ) ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) 0h ) )
21 18 20 bitri 
 |-  ( ( NN X. { 0h } ) ~~>v 0h <-> ( ( NN X. { 0h } ) e. ( ~H ^m NN ) /\ ( NN X. { 0h } ) ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) 0h ) )
22 6 16 21 mpbir2an 
 |-  ( NN X. { 0h } ) ~~>v 0h