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

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 ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
hhcms.2 ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
Assertion hhcms 𝐷 ∈ ( CMet ‘ ℋ )

Proof

Step Hyp Ref Expression
1 hhcms.1 ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2 hhcms.2 ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
3 eqid ⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
4 1 2 hhmet ⊢ 𝐷 ∈ ( Met ‘ ℋ )
5 1 2 hhcau ⊢ Cauchy = ( ( Cau ‘ 𝐷 ) ∩ ( ℋ ↑m ℕ ) )
6 5 eleq2i ⊢ ( 𝑓 ∈ Cauchy ↔ 𝑓 ∈ ( ( Cau ‘ 𝐷 ) ∩ ( ℋ ↑m ℕ ) ) )
7 elin ⊢ ( 𝑓 ∈ ( ( Cau ‘ 𝐷 ) ∩ ( ℋ ↑m ℕ ) ) ↔ ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 ∈ ( ℋ ↑m ℕ ) ) )
8 ax-hilex ⊢ ℋ ∈ V
9 nnex ⊢ ℕ ∈ V
10 8 9 elmap ⊢ ( 𝑓 ∈ ( ℋ ↑m ℕ ) ↔ 𝑓 : ℕ ⟶ ℋ )
11 10 anbi2i ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 ∈ ( ℋ ↑m ℕ ) ) ↔ ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ ℋ ) )
12 7 11 bitri ⊢ ( 𝑓 ∈ ( ( Cau ‘ 𝐷 ) ∩ ( ℋ ↑m ℕ ) ) ↔ ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ ℋ ) )
13 6 12 bitri ⊢ ( 𝑓 ∈ Cauchy ↔ ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ ℋ ) )
14 ax-hcompl ⊢ ( 𝑓 ∈ Cauchy → ∃ 𝑥 ∈ ℋ 𝑓 ⇝𝑣 𝑥 )
15 13 14 sylbir ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ ℋ ) → ∃ 𝑥 ∈ ℋ 𝑓 ⇝𝑣 𝑥 )
16 1 2 3 hhlm ⊢ ⇝𝑣 = ( ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ↾ ( ℋ ↑m ℕ ) )
17 16 breqi ⊢ ( 𝑓 ⇝𝑣 𝑥 ↔ 𝑓 ( ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ↾ ( ℋ ↑m ℕ ) ) 𝑥 )
18 vex ⊢ 𝑥 ∈ V
19 18 brresi ⊢ ( 𝑓 ( ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) ↾ ( ℋ ↑m ℕ ) ) 𝑥 ↔ ( 𝑓 ∈ ( ℋ ↑m ℕ ) ∧ 𝑓 ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) 𝑥 ) )
20 17 19 bitri ⊢ ( 𝑓 ⇝𝑣 𝑥 ↔ ( 𝑓 ∈ ( ℋ ↑m ℕ ) ∧ 𝑓 ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) 𝑥 ) )
21 vex ⊢ 𝑓 ∈ V
22 21 18 breldm ⊢ ( 𝑓 ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) 𝑥 → 𝑓 ∈ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) )
23 20 22 simplbiim ⊢ ( 𝑓 ⇝𝑣 𝑥 → 𝑓 ∈ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) )
24 23 rexlimivw ⊢ ( ∃ 𝑥 ∈ ℋ 𝑓 ⇝𝑣 𝑥 → 𝑓 ∈ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) )
25 15 24 syl ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ ℋ ) → 𝑓 ∈ dom ( ⇝𝑡 ‘ ( MetOpen ‘ 𝐷 ) ) )
26 3 4 25 iscmet3i ⊢ 𝐷 ∈ ( CMet ‘ ℋ )