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 UNrmCVec
h2hl.3 =BaseSetU
h2hl.4 D=IndMetU
h2hl.5 J=MetOpenD
Assertion h2hlm v=tJ

Proof

Step Hyp Ref Expression
1 h2hl.1 U=+norm
2 h2hl.2 UNrmCVec
3 h2hl.3 =BaseSetU
4 h2hl.4 D=IndMetU
5 h2hl.5 J=MetOpenD
6 df-hlim v=fx|f:xy+jkjnormfk-x<y
7 6 relopabiv Relv
8 relres ReltJ
9 6 eleq2i fxvfxfx|f:xy+jkjnormfk-x<y
10 opabidw fxfx|f:xy+jkjnormfk-x<yf:xy+jkjnormfk-x<y
11 3 hlex V
12 nnex V
13 11 12 elmap ff:
14 13 anbi1i ffxtJf:fxtJ
15 df-br ftJxfxtJ
16 3 4 imsxmet UNrmCVecD∞Met
17 2 16 mp1i f:D∞Met
18 nnuz =1
19 1zzd f:1
20 eqidd f:kfk=fk
21 id f:f:
22 5 17 18 19 20 21 lmmbrf f:ftJxxy+jkjfkDx<y
23 eluznn jkjk
24 ffvelrn f:kfk
25 1 2 3 4 h2hmetdval fkxfkDx=normfk-x
26 24 25 sylan f:kxfkDx=normfk-x
27 26 breq1d f:kxfkDx<ynormfk-x<y
28 27 an32s f:xkfkDx<ynormfk-x<y
29 23 28 sylan2 f:xjkjfkDx<ynormfk-x<y
30 29 anassrs f:xjkjfkDx<ynormfk-x<y
31 30 ralbidva f:xjkjfkDx<ykjnormfk-x<y
32 31 rexbidva f:xjkjfkDx<yjkjnormfk-x<y
33 32 ralbidv f:xy+jkjfkDx<yy+jkjnormfk-x<y
34 33 pm5.32da f:xy+jkjfkDx<yxy+jkjnormfk-x<y
35 22 34 bitrd f:ftJxxy+jkjnormfk-x<y
36 15 35 bitr3id f:fxtJxy+jkjnormfk-x<y
37 36 pm5.32i f:fxtJf:xy+jkjnormfk-x<y
38 14 37 bitr2i f:xy+jkjnormfk-x<yffxtJ
39 anass f:xy+jkjnormfk-x<yf:xy+jkjnormfk-x<y
40 opelres xVfxtJffxtJ
41 40 elv fxtJffxtJ
42 38 39 41 3bitr4i f:xy+jkjnormfk-x<yfxtJ
43 9 10 42 3bitri fxvfxtJ
44 7 8 43 eqrelriiv v=tJ