This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐻 ∈ Cℋ ∧ 𝐹 ∈ Cauchy ∧ 𝐹 : ℕ ⟶ 𝐻 ) → ∃ 𝑥 ∈ 𝐻 𝐹 ⇝𝑣 𝑥 )

Proof

Step Hyp Ref Expression
1 isch3 ⊢ ( 𝐻 ∈ Cℋ ↔ ( 𝐻 ∈ Sℋ ∧ ∀ 𝑓 ∈ Cauchy ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) )
2 1 simprbi ⊢ ( 𝐻 ∈ Cℋ → ∀ 𝑓 ∈ Cauchy ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) )
3 feq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 : ℕ ⟶ 𝐻 ↔ 𝐹 : ℕ ⟶ 𝐻 ) )
4 breq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ⇝𝑣 𝑥 ↔ 𝐹 ⇝𝑣 𝑥 ) )
5 4 rexbidv ⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ↔ ∃ 𝑥 ∈ 𝐻 𝐹 ⇝𝑣 𝑥 ) )
6 3 5 imbi12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ↔ ( 𝐹 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝐹 ⇝𝑣 𝑥 ) ) )
7 6 rspccv ⊢ ( ∀ 𝑓 ∈ Cauchy ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) → ( 𝐹 ∈ Cauchy → ( 𝐹 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝐹 ⇝𝑣 𝑥 ) ) )
8 2 7 syl ⊢ ( 𝐻 ∈ Cℋ → ( 𝐹 ∈ Cauchy → ( 𝐹 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝐹 ⇝𝑣 𝑥 ) ) )
9 8 3imp ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐹 ∈ Cauchy ∧ 𝐹 : ℕ ⟶ 𝐻 ) → ∃ 𝑥 ∈ 𝐻 𝐹 ⇝𝑣 𝑥 )