Metamath Proof Explorer

Theorem isch3

Description: A Hilbert subspace is closed iff it is complete. A complete subspace is one in which every Cauchy sequence of vectors in the subspace converges to a member of the subspace (Definition of complete subspace in Beran p. 96). Remark 3.12 of Beran p. 107. (Contributed by NM, 24-Dec-2001) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Assertion isch3 
|- ( H e. CH <-> ( H e. SH /\ A. f e. Cauchy ( f : NN --> H -> E. x e. H f ~~>v x ) ) )

Proof

Step Hyp Ref Expression
1 isch2 
 |-  ( H e. CH <-> ( H e. SH /\ A. f A. x ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) ) )
2 ax-hcompl 
 |-  ( f e. Cauchy -> E. x e. ~H f ~~>v x )
3 rexex 
 |-  ( E. x e. ~H f ~~>v x -> E. x f ~~>v x )
4 2 3 syl 
 |-  ( f e. Cauchy -> E. x f ~~>v x )
5 19.29 
 |-  ( ( A. x ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) /\ E. x f ~~>v x ) -> E. x ( ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) /\ f ~~>v x ) )
6 4 5 sylan2 
 |-  ( ( A. x ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) /\ f e. Cauchy ) -> E. x ( ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) /\ f ~~>v x ) )
7 id 
 |-  ( ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) -> ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) )
8 7 imp 
 |-  ( ( ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) /\ ( f : NN --> H /\ f ~~>v x ) ) -> x e. H )
9 8 an12s 
 |-  ( ( f : NN --> H /\ ( ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) /\ f ~~>v x ) ) -> x e. H )
10 simprr 
 |-  ( ( f : NN --> H /\ ( ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) /\ f ~~>v x ) ) -> f ~~>v x )
11 9 10 jca 
 |-  ( ( f : NN --> H /\ ( ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) /\ f ~~>v x ) ) -> ( x e. H /\ f ~~>v x ) )
12 11 ex 
 |-  ( f : NN --> H -> ( ( ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) /\ f ~~>v x ) -> ( x e. H /\ f ~~>v x ) ) )
13 12 eximdv 
 |-  ( f : NN --> H -> ( E. x ( ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) /\ f ~~>v x ) -> E. x ( x e. H /\ f ~~>v x ) ) )
14 13 com12 
 |-  ( E. x ( ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) /\ f ~~>v x ) -> ( f : NN --> H -> E. x ( x e. H /\ f ~~>v x ) ) )
15 df-rex 
 |-  ( E. x e. H f ~~>v x <-> E. x ( x e. H /\ f ~~>v x ) )
16 14 15 imbitrrdi 
 |-  ( E. x ( ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) /\ f ~~>v x ) -> ( f : NN --> H -> E. x e. H f ~~>v x ) )
17 6 16 syl 
 |-  ( ( A. x ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) /\ f e. Cauchy ) -> ( f : NN --> H -> E. x e. H f ~~>v x ) )
18 17 ex 
 |-  ( A. x ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) -> ( f e. Cauchy -> ( f : NN --> H -> E. x e. H f ~~>v x ) ) )
19 nfv 
 |-  F/ x f e. Cauchy
20 nfv 
 |-  F/ x f : NN --> H
21 nfre1 
 |-  F/ x E. x e. H f ~~>v x
22 20 21 nfim 
 |-  F/ x ( f : NN --> H -> E. x e. H f ~~>v x )
23 19 22 nfim 
 |-  F/ x ( f e. Cauchy -> ( f : NN --> H -> E. x e. H f ~~>v x ) )
24 bi2.04 
 |-  ( ( f e. Cauchy -> ( f : NN --> H -> E. x e. H f ~~>v x ) ) <-> ( f : NN --> H -> ( f e. Cauchy -> E. x e. H f ~~>v x ) ) )
25 hlimcaui 
 |-  ( f ~~>v x -> f e. Cauchy )
26 25 imim1i 
 |-  ( ( f e. Cauchy -> E. x e. H f ~~>v x ) -> ( f ~~>v x -> E. x e. H f ~~>v x ) )
27 rexex 
 |-  ( E. x e. H f ~~>v x -> E. x f ~~>v x )
28 hlimeui 
 |-  ( E. x f ~~>v x <-> E! x f ~~>v x )
29 27 28 sylib 
 |-  ( E. x e. H f ~~>v x -> E! x f ~~>v x )
30 exancom 
 |-  ( E. x ( x e. H /\ f ~~>v x ) <-> E. x ( f ~~>v x /\ x e. H ) )
31 15 30 sylbb 
 |-  ( E. x e. H f ~~>v x -> E. x ( f ~~>v x /\ x e. H ) )
32 eupick 
 |-  ( ( E! x f ~~>v x /\ E. x ( f ~~>v x /\ x e. H ) ) -> ( f ~~>v x -> x e. H ) )
33 29 31 32 syl2anc 
 |-  ( E. x e. H f ~~>v x -> ( f ~~>v x -> x e. H ) )
34 26 33 syli 
 |-  ( ( f e. Cauchy -> E. x e. H f ~~>v x ) -> ( f ~~>v x -> x e. H ) )
35 34 imim2i 
 |-  ( ( f : NN --> H -> ( f e. Cauchy -> E. x e. H f ~~>v x ) ) -> ( f : NN --> H -> ( f ~~>v x -> x e. H ) ) )
36 24 35 sylbi 
 |-  ( ( f e. Cauchy -> ( f : NN --> H -> E. x e. H f ~~>v x ) ) -> ( f : NN --> H -> ( f ~~>v x -> x e. H ) ) )
37 36 impd 
 |-  ( ( f e. Cauchy -> ( f : NN --> H -> E. x e. H f ~~>v x ) ) -> ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) )
38 23 37 alrimi 
 |-  ( ( f e. Cauchy -> ( f : NN --> H -> E. x e. H f ~~>v x ) ) -> A. x ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) )
39 18 38 impbii 
 |-  ( A. x ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) <-> ( f e. Cauchy -> ( f : NN --> H -> E. x e. H f ~~>v x ) ) )
40 39 albii 
 |-  ( A. f A. x ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) <-> A. f ( f e. Cauchy -> ( f : NN --> H -> E. x e. H f ~~>v x ) ) )
41 df-ral 
 |-  ( A. f e. Cauchy ( f : NN --> H -> E. x e. H f ~~>v x ) <-> A. f ( f e. Cauchy -> ( f : NN --> H -> E. x e. H f ~~>v x ) ) )
42 40 41 bitr4i 
 |-  ( A. f A. x ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) <-> A. f e. Cauchy ( f : NN --> H -> E. x e. H f ~~>v x ) )
43 42 anbi2i 
 |-  ( ( H e. SH /\ A. f A. x ( ( f : NN --> H /\ f ~~>v x ) -> x e. H ) ) <-> ( H e. SH /\ A. f e. Cauchy ( f : NN --> H -> E. x e. H f ~~>v x ) ) )
44 1 43 bitri 
 |-  ( H e. CH <-> ( H e. SH /\ A. f e. Cauchy ( f : NN --> H -> E. x e. H f ~~>v x ) ) )