Metamath Proof Explorer

Theorem h2hlm

Description: The limit sequences of Hilbert space. (Contributed by NM, 6-Jun-2008) (Revised by Mario Carneiro, 13-May-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022) (New usage is discouraged.)

Ref Expression
Hypotheses h2hl.1 
|- U = <. <. +h , .h >. , normh >.
h2hl.2 
|- U e. NrmCVec
h2hl.3 
|- ~H = ( BaseSet ` U )
h2hl.4 
|- D = ( IndMet ` U )
h2hl.5 
|- J = ( MetOpen ` D )
Assertion h2hlm 
|- ~~>v = ( ( ~~>t ` J ) |` ( ~H ^m NN ) )

Proof

Step Hyp Ref Expression
1 h2hl.1 
 |-  U = <. <. +h , .h >. , normh >.
2 h2hl.2 
 |-  U e. NrmCVec
3 h2hl.3 
 |-  ~H = ( BaseSet ` U )
4 h2hl.4 
 |-  D = ( IndMet ` U )
5 h2hl.5 
 |-  J = ( MetOpen ` D )
6 df-hlim 
 |-  ~~>v = { <. f , x >. | ( ( f : NN --> ~H /\ x e. ~H ) /\ A. y e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` k ) -h x ) ) < y ) }
7 6 relopabiv 
 |-  Rel ~~>v
8 relres 
 |-  Rel ( ( ~~>t ` J ) |` ( ~H ^m NN ) )
9 6 eleq2i 
 |-  ( <. f , x >. e. ~~>v <-> <. f , x >. e. { <. f , x >. | ( ( f : NN --> ~H /\ x e. ~H ) /\ A. y e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` k ) -h x ) ) < y ) } )
10 opabidw 
 |-  ( <. f , x >. e. { <. f , x >. | ( ( f : NN --> ~H /\ x e. ~H ) /\ A. y e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` k ) -h x ) ) < y ) } <-> ( ( f : NN --> ~H /\ x e. ~H ) /\ A. y e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` k ) -h x ) ) < y ) )
11 3 hlex 
 |-  ~H e. _V
12 nnex 
 |-  NN e. _V
13 11 12 elmap 
 |-  ( f e. ( ~H ^m NN ) <-> f : NN --> ~H )
14 13 anbi1i 
 |-  ( ( f e. ( ~H ^m NN ) /\ <. f , x >. e. ( ~~>t ` J ) ) <-> ( f : NN --> ~H /\ <. f , x >. e. ( ~~>t ` J ) ) )
15 df-br 
 |-  ( f ( ~~>t ` J ) x <-> <. f , x >. e. ( ~~>t ` J ) )
16 3 4 imsxmet 
 |-  ( U e. NrmCVec -> D e. ( *Met ` ~H ) )
17 2 16 mp1i 
 |-  ( f : NN --> ~H -> D e. ( *Met ` ~H ) )
18 nnuz 
 |-  NN = ( ZZ>= ` 1 )
19 1zzd 
 |-  ( f : NN --> ~H -> 1 e. ZZ )
20 eqidd 
 |-  ( ( f : NN --> ~H /\ k e. NN ) -> ( f ` k ) = ( f ` k ) )
21 id 
 |-  ( f : NN --> ~H -> f : NN --> ~H )
22 5 17 18 19 20 21 lmmbrf 
 |-  ( f : NN --> ~H -> ( f ( ~~>t ` J ) x <-> ( x e. ~H /\ A. y e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( f ` k ) D x ) < y ) ) )
23 eluznn 
 |-  ( ( j e. NN /\ k e. ( ZZ>= ` j ) ) -> k e. NN )
24 ffvelrn 
 |-  ( ( f : NN --> ~H /\ k e. NN ) -> ( f ` k ) e. ~H )
25 1 2 3 4 h2hmetdval 
 |-  ( ( ( f ` k ) e. ~H /\ x e. ~H ) -> ( ( f ` k ) D x ) = ( normh ` ( ( f ` k ) -h x ) ) )
26 24 25 sylan 
 |-  ( ( ( f : NN --> ~H /\ k e. NN ) /\ x e. ~H ) -> ( ( f ` k ) D x ) = ( normh ` ( ( f ` k ) -h x ) ) )
27 26 breq1d 
 |-  ( ( ( f : NN --> ~H /\ k e. NN ) /\ x e. ~H ) -> ( ( ( f ` k ) D x ) < y <-> ( normh ` ( ( f ` k ) -h x ) ) < y ) )
28 27 an32s 
 |-  ( ( ( f : NN --> ~H /\ x e. ~H ) /\ k e. NN ) -> ( ( ( f ` k ) D x ) < y <-> ( normh ` ( ( f ` k ) -h x ) ) < y ) )
29 23 28 sylan2 
 |-  ( ( ( f : NN --> ~H /\ x e. ~H ) /\ ( j e. NN /\ k e. ( ZZ>= ` j ) ) ) -> ( ( ( f ` k ) D x ) < y <-> ( normh ` ( ( f ` k ) -h x ) ) < y ) )
30 29 anassrs 
 |-  ( ( ( ( f : NN --> ~H /\ x e. ~H ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( f ` k ) D x ) < y <-> ( normh ` ( ( f ` k ) -h x ) ) < y ) )
31 30 ralbidva 
 |-  ( ( ( f : NN --> ~H /\ x e. ~H ) /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( ( f ` k ) D x ) < y <-> A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` k ) -h x ) ) < y ) )
32 31 rexbidva 
 |-  ( ( f : NN --> ~H /\ x e. ~H ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( f ` k ) D x ) < y <-> E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` k ) -h x ) ) < y ) )
33 32 ralbidv 
 |-  ( ( f : NN --> ~H /\ x e. ~H ) -> ( A. y e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( f ` k ) D x ) < y <-> A. y e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` k ) -h x ) ) < y ) )
34 33 pm5.32da 
 |-  ( f : NN --> ~H -> ( ( x e. ~H /\ A. y e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( f ` k ) D x ) < y ) <-> ( x e. ~H /\ A. y e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` k ) -h x ) ) < y ) ) )
35 22 34 bitrd 
 |-  ( f : NN --> ~H -> ( f ( ~~>t ` J ) x <-> ( x e. ~H /\ A. y e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` k ) -h x ) ) < y ) ) )
36 15 35 bitr3id 
 |-  ( f : NN --> ~H -> ( <. f , x >. e. ( ~~>t ` J ) <-> ( x e. ~H /\ A. y e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` k ) -h x ) ) < y ) ) )
37 36 pm5.32i 
 |-  ( ( f : NN --> ~H /\ <. f , x >. e. ( ~~>t ` J ) ) <-> ( f : NN --> ~H /\ ( x e. ~H /\ A. y e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` k ) -h x ) ) < y ) ) )
38 14 37 bitr2i 
 |-  ( ( f : NN --> ~H /\ ( x e. ~H /\ A. y e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` k ) -h x ) ) < y ) ) <-> ( f e. ( ~H ^m NN ) /\ <. f , x >. e. ( ~~>t ` J ) ) )
39 anass 
 |-  ( ( ( f : NN --> ~H /\ x e. ~H ) /\ A. y e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` k ) -h x ) ) < y ) <-> ( f : NN --> ~H /\ ( x e. ~H /\ A. y e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` k ) -h x ) ) < y ) ) )
40 opelres 
 |-  ( x e. _V -> ( <. f , x >. e. ( ( ~~>t ` J ) |` ( ~H ^m NN ) ) <-> ( f e. ( ~H ^m NN ) /\ <. f , x >. e. ( ~~>t ` J ) ) ) )
41 40 elv 
 |-  ( <. f , x >. e. ( ( ~~>t ` J ) |` ( ~H ^m NN ) ) <-> ( f e. ( ~H ^m NN ) /\ <. f , x >. e. ( ~~>t ` J ) ) )
42 38 39 41 3bitr4i 
 |-  ( ( ( f : NN --> ~H /\ x e. ~H ) /\ A. y e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` k ) -h x ) ) < y ) <-> <. f , x >. e. ( ( ~~>t ` J ) |` ( ~H ^m NN ) ) )
43 9 10 42 3bitri 
 |-  ( <. f , x >. e. ~~>v <-> <. f , x >. e. ( ( ~~>t ` J ) |` ( ~H ^m NN ) ) )
44 7 8 43 eqrelriiv 
 |-  ~~>v = ( ( ~~>t ` J ) |` ( ~H ^m NN ) )