Metamath Proof Explorer

Theorem hhcms

Description: The Hilbert space induced metric determines a complete metric space. (Contributed by NM, 10-Apr-2008) (Proof shortened by Mario Carneiro, 14-May-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022) (New usage is discouraged.)

Ref Expression
Hypotheses hhcms.1 ⊢ U = + ℎ ⋅ ℎ norm ℎ
hhcms.2 ⊢ D = IndMet ⁡ U
Assertion hhcms ⊢ D ∈ CMet ⁡ ℋ

Proof

Step Hyp Ref Expression
1 hhcms.1 ⊢ U = + ℎ ⋅ ℎ norm ℎ
2 hhcms.2 ⊢ D = IndMet ⁡ U
3 eqid ⊢ MetOpen ⁡ D = MetOpen ⁡ D
4 1 2 hhmet ⊢ D ∈ Met ⁡ ℋ
5 1 2 hhcau ⊢ Cauchy = Cau ⁡ D ∩ ℋ ℕ
6 5 eleq2i ⊢ f ∈ Cauchy ↔ f ∈ Cau ⁡ D ∩ ℋ ℕ
7 elin ⊢ f ∈ Cau ⁡ D ∩ ℋ ℕ ↔ f ∈ Cau ⁡ D ∧ f ∈ ℋ ℕ
8 ax-hilex ⊢ ℋ ∈ V
9 nnex ⊢ ℕ ∈ V
10 8 9 elmap ⊢ f ∈ ℋ ℕ ↔ f : ℕ ⟶ ℋ
11 10 anbi2i ⊢ f ∈ Cau ⁡ D ∧ f ∈ ℋ ℕ ↔ f ∈ Cau ⁡ D ∧ f : ℕ ⟶ ℋ
12 7 11 bitri ⊢ f ∈ Cau ⁡ D ∩ ℋ ℕ ↔ f ∈ Cau ⁡ D ∧ f : ℕ ⟶ ℋ
13 6 12 bitri ⊢ f ∈ Cauchy ↔ f ∈ Cau ⁡ D ∧ f : ℕ ⟶ ℋ
14 ax-hcompl ⊢ f ∈ Cauchy → ∃ x ∈ ℋ f ⇝v x
15 13 14 sylbir ⊢ f ∈ Cau ⁡ D ∧ f : ℕ ⟶ ℋ → ∃ x ∈ ℋ f ⇝v x
16 1 2 3 hhlm ⊢ ⇝v = ⇝t ⁡ MetOpen ⁡ D ↾ ℋ ℕ
17 16 breqi ⊢ f ⇝v x ↔ f ⇝t ⁡ MetOpen ⁡ D ↾ ℋ ℕ x
18 vex ⊢ x ∈ V
19 18 brresi ⊢ f ⇝t ⁡ MetOpen ⁡ D ↾ ℋ ℕ x ↔ f ∈ ℋ ℕ ∧ f ⇝t ⁡ MetOpen ⁡ D x
20 17 19 bitri ⊢ f ⇝v x ↔ f ∈ ℋ ℕ ∧ f ⇝t ⁡ MetOpen ⁡ D x
21 vex ⊢ f ∈ V
22 21 18 breldm ⊢ f ⇝t ⁡ MetOpen ⁡ D x → f ∈ dom ⁡ ⇝t ⁡ MetOpen ⁡ D
23 20 22 simplbiim ⊢ f ⇝v x → f ∈ dom ⁡ ⇝t ⁡ MetOpen ⁡ D
24 23 rexlimivw ⊢ ∃ x ∈ ℋ f ⇝v x → f ∈ dom ⁡ ⇝t ⁡ MetOpen ⁡ D
25 15 24 syl ⊢ f ∈ Cau ⁡ D ∧ f : ℕ ⟶ ℋ → f ∈ dom ⁡ ⇝t ⁡ MetOpen ⁡ D
26 3 4 25 iscmet3i ⊢ D ∈ CMet ⁡ ℋ