This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imsdf

Description: Mapping for the induced metric distance function of a normed complex vector space. (Contributed by NM, 29-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses imsdfn.1 
|- X = ( BaseSet ` U )
imsdfn.8 
|- D = ( IndMet ` U )
Assertion imsdf 
|- ( U e. NrmCVec -> D : ( X X. X ) --> RR )

Proof

Step Hyp Ref Expression
1 imsdfn.1 
 |-  X = ( BaseSet ` U )
2 imsdfn.8 
 |-  D = ( IndMet ` U )
3 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
4 1 3 nvf 
 |-  ( U e. NrmCVec -> ( normCV ` U ) : X --> RR )
5 eqid 
 |-  ( -v ` U ) = ( -v ` U )
6 1 5 nvmf 
 |-  ( U e. NrmCVec -> ( -v ` U ) : ( X X. X ) --> X )
7 fco 
 |-  ( ( ( normCV ` U ) : X --> RR /\ ( -v ` U ) : ( X X. X ) --> X ) -> ( ( normCV ` U ) o. ( -v ` U ) ) : ( X X. X ) --> RR )
8 4 6 7 syl2anc 
 |-  ( U e. NrmCVec -> ( ( normCV ` U ) o. ( -v ` U ) ) : ( X X. X ) --> RR )
9 5 3 2 imsval 
 |-  ( U e. NrmCVec -> D = ( ( normCV ` U ) o. ( -v ` U ) ) )
10 9 feq1d 
 |-  ( U e. NrmCVec -> ( D : ( X X. X ) --> RR <-> ( ( normCV ` U ) o. ( -v ` U ) ) : ( X X. X ) --> RR ) )
11 8 10 mpbird 
 |-  ( U e. NrmCVec -> D : ( X X. X ) --> RR )