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

Metamath Proof Explorer

Theorem tmsds

Description: The metric of a constructed metric space. (Contributed by Mario Carneiro, 2-Sep-2015)

		Ref	Expression
	Hypothesis	tmsbas.k	$⊢ K = toMetSp (D)$
	Assertion	tmsds	$⊢ D \in ∞Met (X) \to D = dist (K)$

Step	Hyp	Ref	Expression
1		tmsbas.k	$⊢ K = toMetSp (D)$
2		eqid	$⊢ \{⟨{Base}_{ndx}, X⟩, ⟨dist (ndx), D⟩\} = \{⟨{Base}_{ndx}, X⟩, ⟨dist (ndx), D⟩\}$
3	2 1	tmslem	$⊢ D \in ∞Met (X) \to (X = {Base}_{K} \land D = dist (K) \land MetOpen (D) = TopOpen (K))$
4	3	simp2d	$⊢ D \in ∞Met (X) \to D = dist (K)$