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

Metamath Proof Explorer

Theorem imsxmet

Description: The induced metric of a normed complex vector space is an extended metric space. (Contributed by Mario Carneiro, 10-Sep-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	imsmet.1	$⊢ X = BaseSet (U)$
	imsmet.8	$⊢ D = IndMet (U)$
Assertion	imsxmet	$⊢ U \in NrmCVec \to D \in ∞Met (X)$

Proof

Step	Hyp	Ref	Expression
1		imsmet.1	$⊢ X = BaseSet (U)$
2		imsmet.8	$⊢ D = IndMet (U)$
3	1 2	imsmet	$⊢ U \in NrmCVec \to D \in Met (X)$
4		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
5	3 4	syl	$⊢ U \in NrmCVec \to D \in ∞Met (X)$