This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ D = {norm}_{ℎ} \circ -_{ℎ}$
	Assertion	hilmetdval	$⊢ (A \in ℋ \land B \in ℋ) \to A D B = {norm}_{ℎ} (A -_{ℎ} B)$

Step	Hyp	Ref	Expression
1		hilmet.1	$⊢ D = {norm}_{ℎ} \circ -_{ℎ}$
2		eqid	$⊢ ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩ = ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
3	2 1	hhims	$⊢ D = IndMet (⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩)$
4	2 3	hhmetdval	$⊢ (A \in ℋ \land B \in ℋ) \to A D B = {norm}_{ℎ} (A -_{ℎ} B)$