Theorem h2hmetdval

Description: Value of the distance function of the metric space of Hilbert space. (Contributed by NM, 6-Jun-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	h2h.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
	h2h.2	⊢ 𝑈 ∈ NrmCVec
	h2hm.4	⊢ ℋ = ( BaseSet ‘ 𝑈 )
	h2hm.5	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
Assertion	h2hmetdval	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 𝐷 𝐵 ) = ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		h2h.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2		h2h.2	⊢ 𝑈 ∈ NrmCVec
3		h2hm.4	⊢ ℋ = ( BaseSet ‘ 𝑈 )
4		h2hm.5	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
5	1 2 3	h2hvs	⊢ −ℎ = ( −𝑣 ‘ 𝑈 )
6	1 2	h2hnm	⊢ normℎ = ( normCV ‘ 𝑈 )
7	3 5 6 4	imsdval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 𝐷 𝐵 ) = ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) )
8	2 7	mp3an1	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 𝐷 𝐵 ) = ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) )