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 ‘ ℋ )