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=\mathrm{BaseSet}\left(U\right)$$
	imsdfn.8	$$⊢D=\mathrm{IndMet}\left(U\right)$$
Assertion	imsdf	$$⊢U\in \mathrm{NrmCVec}\to D:X\times X⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		imsdfn.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		imsdfn.8	$$⊢D=\mathrm{IndMet}\left(U\right)$$
3		eqid	$$⊢{norm}_{CV}\left(U\right)={norm}_{CV}\left(U\right)$$
4	1 3	nvf	$$⊢U\in \mathrm{NrmCVec}\to {norm}_{CV}\left(U\right):X⟶ℝ$$
5		eqid	$$⊢{-}_v\left(U\right)={-}_v\left(U\right)$$
6	1 5	nvmf	$$⊢U\in \mathrm{NrmCVec}\to {-}_v\left(U\right):X\times X⟶X$$
7		fco	$$⊢\left({norm}_{CV}\left(U\right):X⟶ℝ\wedge {-}_v\left(U\right):X\times X⟶X\right)\to \left({norm}_{CV}\left(U\right)\circ {-}_v\left(U\right)\right):X\times X⟶ℝ$$
8	4 6 7	syl2anc	$$⊢U\in \mathrm{NrmCVec}\to \left({norm}_{CV}\left(U\right)\circ {-}_v\left(U\right)\right):X\times X⟶ℝ$$
9	5 3 2	imsval	$$⊢U\in \mathrm{NrmCVec}\to D={norm}_{CV}\left(U\right)\circ {-}_v\left(U\right)$$
10	9	feq1d	$$⊢U\in \mathrm{NrmCVec}\to \left(D:X\times X⟶ℝ\leftrightarrow \left({norm}_{CV}\left(U\right)\circ {-}_v\left(U\right)\right):X\times X⟶ℝ\right)$$
11	8 10	mpbird	$$⊢U\in \mathrm{NrmCVec}\to D:X\times X⟶ℝ$$