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 ∈ C ℋ ∧ F ∈ Cauchy ∧ F : ℕ ⟶ H → ∃ x ∈ H F ⇝v x

Proof

Step Hyp Ref Expression
1 isch3 ⊢ H ∈ C ℋ ↔ H ∈ S ℋ ∧ ∀ f ∈ Cauchy f : ℕ ⟶ H → ∃ x ∈ H f ⇝v x
2 1 simprbi ⊢ H ∈ C ℋ → ∀ f ∈ Cauchy f : ℕ ⟶ H → ∃ x ∈ H f ⇝v x
3 feq1 ⊢ f = F → f : ℕ ⟶ H ↔ F : ℕ ⟶ H
4 breq1 ⊢ f = F → f ⇝v x ↔ F ⇝v x
5 4 rexbidv ⊢ f = F → ∃ x ∈ H f ⇝v x ↔ ∃ x ∈ H F ⇝v x
6 3 5 imbi12d ⊢ f = F → f : ℕ ⟶ H → ∃ x ∈ H f ⇝v x ↔ F : ℕ ⟶ H → ∃ x ∈ H F ⇝v x
7 6 rspccv ⊢ ∀ f ∈ Cauchy f : ℕ ⟶ H → ∃ x ∈ H f ⇝v x → F ∈ Cauchy → F : ℕ ⟶ H → ∃ x ∈ H F ⇝v x
8 2 7 syl ⊢ H ∈ C ℋ → F ∈ Cauchy → F : ℕ ⟶ H → ∃ x ∈ H F ⇝v x
9 8 3imp ⊢ H ∈ C ℋ ∧ F ∈ Cauchy ∧ F : ℕ ⟶ H → ∃ x ∈ H F ⇝v x