Theorem hhims2

Description: Hilbert space distance metric. (Contributed by NM, 10-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhnv.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
	hhims2.2	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
Assertion	hhims2	⊢ 𝐷 = ( normℎ ∘ −ℎ )

Proof

Step	Hyp	Ref	Expression
1		hhnv.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2		hhims2.2	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
3		eqid	⊢ ( normℎ ∘ −ℎ ) = ( normℎ ∘ −ℎ )
4	1 3	hhims	⊢ ( normℎ ∘ −ℎ ) = ( IndMet ‘ 𝑈 )
5	2 4	eqtr4i	⊢ 𝐷 = ( normℎ ∘ −ℎ )