# Metamath Proof Explorer

## Theorem imsmet

Description: The induced metric of a normed complex vector space is a metric space. Part of Definition 2.2-1 of Kreyszig p. 58. (Contributed by NM, 4-Dec-2006) (Revised by Mario Carneiro, 10-Sep-2015) (New usage is discouraged.)

Ref Expression
Hypotheses imsmet.1
`|- X = ( BaseSet ` U )`
imsmet.8
`|- D = ( IndMet ` U )`
Assertion imsmet
`|- ( 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 fveq2
` |-  ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> ( IndMet ` U ) = ( IndMet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) )`
4 fveq2
` |-  ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> ( BaseSet ` U ) = ( BaseSet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) )`
5 1 4 syl5eq
` |-  ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> X = ( BaseSet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) )`
6 5 fveq2d
` |-  ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> ( Met ` X ) = ( Met ` ( BaseSet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) ) )`
7 3 6 eleq12d
` |-  ( U = if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) -> ( ( IndMet ` U ) e. ( Met ` X ) <-> ( IndMet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) e. ( Met ` ( BaseSet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) ) ) )`
8 eqid
` |-  ( BaseSet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) = ( BaseSet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) )`
9 eqid
` |-  ( +v ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) = ( +v ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) )`
10 eqid
` |-  ( inv ` ( +v ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) ) = ( inv ` ( +v ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) )`
11 eqid
` |-  ( .sOLD ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) = ( .sOLD ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) )`
12 eqid
` |-  ( 0vec ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) = ( 0vec ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) )`
13 eqid
` |-  ( normCV ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) = ( normCV ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) )`
14 eqid
` |-  ( IndMet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) = ( IndMet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) )`
15 elimnvu
` |-  if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) e. NrmCVec`
16 8 9 10 11 12 13 14 15 imsmetlem
` |-  ( IndMet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) e. ( Met ` ( BaseSet ` if ( U e. NrmCVec , U , <. <. + , x. >. , abs >. ) ) )`
17 7 16 dedth
` |-  ( U e. NrmCVec -> ( IndMet ` U ) e. ( Met ` X ) )`
18 2 17 eqeltrid
` |-  ( U e. NrmCVec -> D e. ( Met ` X ) )`