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 = + norm
h2hl.2 U NrmCVec
h2hl.3 = BaseSet U
h2hl.4 D = IndMet U
h2hl.5 J = MetOpen D
Assertion h2hlm v = t J

Proof

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