Theorem hilxmet

Description: The Hilbert space norm determines a metric space. (Contributed by Mario Carneiro, 10-Sep-2015) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		hilmet.1	⊢ 𝐷 = ( normℎ ∘ −ℎ )
2	1	hilmet	⊢ 𝐷 ∈ ( Met ‘ ℋ )
3		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ ℋ ) → 𝐷 ∈ ( ∞Met ‘ ℋ ) )
4	2 3	ax-mp	⊢ 𝐷 ∈ ( ∞Met ‘ ℋ )