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 ( 𝑓 : ℕ ⟶ 𝐻 → ∃ 𝑥𝐻 𝑓𝑣 𝑥 ) ) )