Theorem hhxmet

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

	Ref	Expression
Hypotheses	hhnv.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
	hhims2.2	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
Assertion	hhxmet	⊢ 𝐷 ∈ ( ∞Met ‘ ℋ )

Proof

Step	Hyp	Ref	Expression
1		hhnv.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2		hhims2.2	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
3	1 2	hhmet	⊢ 𝐷 ∈ ( Met ‘ ℋ )
4		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ ℋ ) → 𝐷 ∈ ( ∞Met ‘ ℋ ) )
5	3 4	ax-mp	⊢ 𝐷 ∈ ( ∞Met ‘ ℋ )