Definition df-ims 27456

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

Assertion

Ref	Expression
df-ims	|- IndMet = ( u e. NrmCVec |-> ( ( normCV ` u ) o. ( -v ` u ) ) )

Detailed syntax breakdown of Definition df-ims

Step	Hyp	Ref	Expression
1		cims 27446	. 2 class IndMet
2		vu	. . 3 setvar u
3		cnv 27439	. . 3 class NrmCVec
4	2	cv 1482	. . . . 5 class u
5		cnmcv 27445	. . . . 5 class normCV
6	4, 5	cfv 5888	. . . 4 class ( normCV ` u )
7		cnsb 27444	. . . . 5 class -v
8	4, 7	cfv 5888	. . . 4 class ( -v ` u )
9	6, 8	ccom 5118	. . 3 class ( ( normCV ` u ) o. ( -v ` u ) )
10	2, 3, 9	cmpt 4729	. 2 class ( u e. NrmCVec |-> ( ( normCV ` u ) o. ( -v ` u ) ) )
11	1, 10	wceq 1483	1 wff IndMet = ( u e. NrmCVec |-> ( ( normCV ` u ) o. ( -v ` u ) ) )

This definition is referenced by:  imsval  27540