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 )