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 ) )