Metamath Proof Explorer

Theorem chcompl

Description: Completeness of a closed subspace of Hilbert space. (Contributed by NM, 4-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion chcompl 
|- ( ( H e. CH /\ F e. Cauchy /\ F : NN --> H ) -> E. x e. H F ~~>v x )

Proof

Step Hyp Ref Expression
1 isch3 
 |-  ( H e. CH <-> ( H e. SH /\ A. f e. Cauchy ( f : NN --> H -> E. x e. H f ~~>v x ) ) )
2 1 simprbi 
 |-  ( H e. CH -> A. f e. Cauchy ( f : NN --> H -> E. x e. H f ~~>v x ) )
3 feq1 
 |-  ( f = F -> ( f : NN --> H <-> F : NN --> H ) )
4 breq1 
 |-  ( f = F -> ( f ~~>v x <-> F ~~>v x ) )
5 4 rexbidv 
 |-  ( f = F -> ( E. x e. H f ~~>v x <-> E. x e. H F ~~>v x ) )
6 3 5 imbi12d 
 |-  ( f = F -> ( ( f : NN --> H -> E. x e. H f ~~>v x ) <-> ( F : NN --> H -> E. x e. H F ~~>v x ) ) )
7 6 rspccv 
 |-  ( A. f e. Cauchy ( f : NN --> H -> E. x e. H f ~~>v x ) -> ( F e. Cauchy -> ( F : NN --> H -> E. x e. H F ~~>v x ) ) )
8 2 7 syl 
 |-  ( H e. CH -> ( F e. Cauchy -> ( F : NN --> H -> E. x e. H F ~~>v x ) ) )
9 8 3imp 
 |-  ( ( H e. CH /\ F e. Cauchy /\ F : NN --> H ) -> E. x e. H F ~~>v x )