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