Metamath Proof Explorer


Theorem h2hcau

Description: The Cauchy sequences of Hilbert space. (Contributed by NM, 6-Jun-2008) (Revised by Mario Carneiro, 13-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses h2hc.1 U = + norm
h2hc.2 U NrmCVec
h2hc.3 = BaseSet U
h2hc.4 D = IndMet U
Assertion h2hcau Cauchy = Cau D

Proof

Step Hyp Ref Expression
1 h2hc.1 U = + norm
2 h2hc.2 U NrmCVec
3 h2hc.3 = BaseSet U
4 h2hc.4 D = IndMet U
5 df-rab f | x + j k j norm f j - f k < x = f | f x + j k j norm f j - f k < x
6 df-hcau Cauchy = f | x + j k j norm f j - f k < x
7 elin f Cau D f Cau D f
8 ancom f Cau D f f f Cau D
9 3 hlex V
10 nnex V
11 9 10 elmap f f :
12 nnuz = 1
13 3 4 imsxmet U NrmCVec D ∞Met
14 2 13 mp1i f : D ∞Met
15 1zzd f : 1
16 eqidd f : k f k = f k
17 eqidd f : j f j = f j
18 id f : f :
19 12 14 15 16 17 18 iscauf f : f Cau D x + j k j f j D f k < x
20 ffvelrn f : j f j
21 20 adantr f : j k j f j
22 eluznn j k j k
23 ffvelrn f : k f k
24 22 23 sylan2 f : j k j f k
25 24 anassrs f : j k j f k
26 1 2 3 4 h2hmetdval f j f k f j D f k = norm f j - f k
27 21 25 26 syl2anc f : j k j f j D f k = norm f j - f k
28 27 breq1d f : j k j f j D f k < x norm f j - f k < x
29 28 ralbidva f : j k j f j D f k < x k j norm f j - f k < x
30 29 rexbidva f : j k j f j D f k < x j k j norm f j - f k < x
31 30 ralbidv f : x + j k j f j D f k < x x + j k j norm f j - f k < x
32 19 31 bitrd f : f Cau D x + j k j norm f j - f k < x
33 11 32 sylbi f f Cau D x + j k j norm f j - f k < x
34 33 pm5.32i f f Cau D f x + j k j norm f j - f k < x
35 7 8 34 3bitri f Cau D f x + j k j norm f j - f k < x
36 35 abbi2i Cau D = f | f x + j k j norm f j - f k < x
37 5 6 36 3eqtr4i Cauchy = Cau D