Theorem hilmet

Description: The Hilbert space norm determines a metric space. (Contributed by NM, 17-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hilmet.1	⊢ 𝐷 = ( normℎ ∘ −ℎ )
Assertion	hilmet	⊢ 𝐷 ∈ ( Met ‘ ℋ )

Proof

Step	Hyp	Ref	Expression
1		hilmet.1	⊢ 𝐷 = ( normℎ ∘ −ℎ )
2		eqid	⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
3	2 1	hhims	⊢ 𝐷 = ( IndMet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
4	2 3	hhmet	⊢ 𝐷 ∈ ( Met ‘ ℋ )