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 NrmCVec D ∞Met X


Step Hyp Ref Expression
1 imsmet.1 X = BaseSet U
2 imsmet.8 D = IndMet U
3 1 2 imsmet U NrmCVec D Met X
4 metxmet D Met X D ∞Met X
5 3 4 syl U NrmCVec D ∞Met X