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⇝vx
15 13 14 sylbir ⊢f∈Cau⁡D∧f:ℕ⟶ℋ→∃x∈ℋf⇝vx
16 1 2 3 hhlm ⊢⇝v=⇝t⁡MetOpen⁡D↾ℋℕ
17 16 breqi ⊢f⇝vx↔f⇝t⁡MetOpen⁡D↾ℋℕx
18 vex ⊢x∈V
19 18 brresi ⊢f⇝t⁡MetOpen⁡D↾ℋℕx↔f∈ℋℕ∧f⇝t⁡MetOpen⁡Dx
20 17 19 bitri ⊢f⇝vx↔f∈ℋℕ∧f⇝t⁡MetOpen⁡Dx
21 vex ⊢f∈V
22 21 18 breldm ⊢f⇝t⁡MetOpen⁡Dx→f∈dom⁡⇝t⁡MetOpen⁡D
23 20 22 simplbiim ⊢f⇝vx→f∈dom⁡⇝t⁡MetOpen⁡D
24 23 rexlimivw ⊢∃x∈ℋf⇝vx→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⁡ℋ