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 e. NrmCVec -> D e. ( *Met ` X ) )

Proof

Step Hyp Ref Expression
1 imsmet.1
 |-  X = ( BaseSet ` U )
2 imsmet.8
 |-  D = ( IndMet ` U )
3 1 2 imsmet
 |-  ( U e. NrmCVec -> D e. ( Met ` X ) )
4 metxmet
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
5 3 4 syl
 |-  ( U e. NrmCVec -> D e. ( *Met ` X ) )