Definition df-ims

Description: Define the induced metric on a normed complex vector space. (Contributed by NM, 11-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Assertion	df-ims	$$⊢\mathrm{IndMet}=\left(u\in \mathrm{NrmCVec}⟼{norm}_{CV}\left(u\right)\circ {-}_v\left(u\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cims	$$class\mathrm{IndMet}$$
1		vu	$$setvaru$$
2		cnv	$$class\mathrm{NrmCVec}$$
3		cnmcv	$$class{norm}_{CV}$$
4	1	cv	$$setvaru$$
5	4 3	cfv	$$class{norm}_{CV}\left(u\right)$$
6		cnsb	$$class{-}_v$$
7	4 6	cfv	$$class{-}_v\left(u\right)$$
8	5 7	ccom	$$class\left({norm}_{CV}\left(u\right)\circ {-}_v\left(u\right)\right)$$
9	1 2 8	cmpt	$$class\left(u\in \mathrm{NrmCVec}⟼{norm}_{CV}\left(u\right)\circ {-}_v\left(u\right)\right)$$
10	0 9	wceq	$$wff\mathrm{IndMet}=\left(u\in \mathrm{NrmCVec}⟼{norm}_{CV}\left(u\right)\circ {-}_v\left(u\right)\right)$$