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

Proof

Step Hyp Ref Expression
1 isch2 ⊢ ( 𝐻 ∈ Cℋ ↔ ( 𝐻 ∈ Sℋ ∧ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ) )
2 ax-hcompl ⊢ ( 𝑓 ∈ Cauchy → ∃ 𝑥 ∈ ℋ 𝑓 ⇝𝑣 𝑥 )
3 rexex ⊢ ( ∃ 𝑥 ∈ ℋ 𝑓 ⇝𝑣 𝑥 → ∃ 𝑥 𝑓 ⇝𝑣 𝑥 )
4 2 3 syl ⊢ ( 𝑓 ∈ Cauchy → ∃ 𝑥 𝑓 ⇝𝑣 𝑥 )
5 19.29 ⊢ ( ( ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ ∃ 𝑥 𝑓 ⇝𝑣 𝑥 ) → ∃ 𝑥 ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ⇝𝑣 𝑥 ) )
6 4 5 sylan2 ⊢ ( ( ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ∈ Cauchy ) → ∃ 𝑥 ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ⇝𝑣 𝑥 ) )
7 id ⊢ ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) → ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) )
8 7 imp ⊢ ( ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) ) → 𝑥 ∈ 𝐻 )
9 8 an12s ⊢ ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ⇝𝑣 𝑥 ) ) → 𝑥 ∈ 𝐻 )
10 simprr ⊢ ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ⇝𝑣 𝑥 ) ) → 𝑓 ⇝𝑣 𝑥 )
11 9 10 jca ⊢ ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ⇝𝑣 𝑥 ) ) → ( 𝑥 ∈ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) )
12 11 ex ⊢ ( 𝑓 : ℕ ⟶ 𝐻 → ( ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → ( 𝑥 ∈ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) ) )
13 12 eximdv ⊢ ( 𝑓 : ℕ ⟶ 𝐻 → ( ∃ 𝑥 ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → ∃ 𝑥 ( 𝑥 ∈ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) ) )
14 13 com12 ⊢ ( ∃ 𝑥 ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ( 𝑥 ∈ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) ) )
15 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) )
16 14 15 syl6ibr ⊢ ( ∃ 𝑥 ( ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ⇝𝑣 𝑥 ) → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) )
17 6 16 syl ⊢ ( ( ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ∧ 𝑓 ∈ Cauchy ) → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) )
18 17 ex ⊢ ( ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) → ( 𝑓 ∈ Cauchy → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) )
19 nfv ⊢ Ⅎ 𝑥 𝑓 ∈ Cauchy
20 nfv ⊢ Ⅎ 𝑥 𝑓 : ℕ ⟶ 𝐻
21 nfre1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥
22 20 21 nfim ⊢ Ⅎ 𝑥 ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 )
23 19 22 nfim ⊢ Ⅎ 𝑥 ( 𝑓 ∈ Cauchy → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) )
24 bi2.04 ⊢ ( ( 𝑓 ∈ Cauchy → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) ↔ ( 𝑓 : ℕ ⟶ 𝐻 → ( 𝑓 ∈ Cauchy → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) )
25 hlimcaui ⊢ ( 𝑓 ⇝𝑣 𝑥 → 𝑓 ∈ Cauchy )
26 25 imim1i ⊢ ( ( 𝑓 ∈ Cauchy → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) → ( 𝑓 ⇝𝑣 𝑥 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) )
27 rexex ⊢ ( ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 → ∃ 𝑥 𝑓 ⇝𝑣 𝑥 )
28 hlimeui ⊢ ( ∃ 𝑥 𝑓 ⇝𝑣 𝑥 ↔ ∃! 𝑥 𝑓 ⇝𝑣 𝑥 )
29 27 28 sylib ⊢ ( ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 → ∃! 𝑥 𝑓 ⇝𝑣 𝑥 )
30 exancom ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) ↔ ∃ 𝑥 ( 𝑓 ⇝𝑣 𝑥 ∧ 𝑥 ∈ 𝐻 ) )
31 15 30 sylbb ⊢ ( ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 → ∃ 𝑥 ( 𝑓 ⇝𝑣 𝑥 ∧ 𝑥 ∈ 𝐻 ) )
32 eupick ⊢ ( ( ∃! 𝑥 𝑓 ⇝𝑣 𝑥 ∧ ∃ 𝑥 ( 𝑓 ⇝𝑣 𝑥 ∧ 𝑥 ∈ 𝐻 ) ) → ( 𝑓 ⇝𝑣 𝑥 → 𝑥 ∈ 𝐻 ) )
33 29 31 32 syl2anc ⊢ ( ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 → ( 𝑓 ⇝𝑣 𝑥 → 𝑥 ∈ 𝐻 ) )
34 26 33 syli ⊢ ( ( 𝑓 ∈ Cauchy → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) → ( 𝑓 ⇝𝑣 𝑥 → 𝑥 ∈ 𝐻 ) )
35 34 imim2i ⊢ ( ( 𝑓 : ℕ ⟶ 𝐻 → ( 𝑓 ∈ Cauchy → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) → ( 𝑓 : ℕ ⟶ 𝐻 → ( 𝑓 ⇝𝑣 𝑥 → 𝑥 ∈ 𝐻 ) ) )
36 24 35 sylbi ⊢ ( ( 𝑓 ∈ Cauchy → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) → ( 𝑓 : ℕ ⟶ 𝐻 → ( 𝑓 ⇝𝑣 𝑥 → 𝑥 ∈ 𝐻 ) ) )
37 36 impd ⊢ ( ( 𝑓 ∈ Cauchy → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) → ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) )
38 23 37 alrimi ⊢ ( ( 𝑓 ∈ Cauchy → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) → ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) )
39 18 38 impbii ⊢ ( ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ↔ ( 𝑓 ∈ Cauchy → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) )
40 39 albii ⊢ ( ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ↔ ∀ 𝑓 ( 𝑓 ∈ Cauchy → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) )
41 df-ral ⊢ ( ∀ 𝑓 ∈ Cauchy ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ↔ ∀ 𝑓 ( 𝑓 ∈ Cauchy → ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) )
42 40 41 bitr4i ⊢ ( ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ↔ ∀ 𝑓 ∈ Cauchy ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) )
43 42 anbi2i ⊢ ( ( 𝐻 ∈ Sℋ ∧ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ 𝐻 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝐻 ) ) ↔ ( 𝐻 ∈ Sℋ ∧ ∀ 𝑓 ∈ Cauchy ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) )
44 1 43 bitri ⊢ ( 𝐻 ∈ Cℋ ↔ ( 𝐻 ∈ Sℋ ∧ ∀ 𝑓 ∈ Cauchy ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥 ∈ 𝐻 𝑓 ⇝𝑣 𝑥 ) ) )