Theorem hilmetdval

Description: Value of the distance function of the metric space of Hilbert space. (Contributed by NM, 17-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hilmet.1	⊢ 𝐷 = ( normℎ ∘ −ℎ )
Assertion	hilmetdval	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 𝐷 𝐵 ) = ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) )

Proof

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