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