Definition df-ims 8220

Description: Define the induced metric on a normed complex vector space.

Assertion

Ref	Expression
df-ims	|- IndMet = {<.u, d>. | (u e. NrmCVec /\ d = ((norm` u) o. (-v` u)))}

Detailed syntax breakdown of Definition df-ims

Step	Hyp	Ref	Expression
1		cims 8210	. 2 class IndMet
2		vu	. . . . . 6 set u
3	2	cv 955	. . . . 5 class u
4		cnv 8203	. . . . 5 class NrmCVec
5	3, 4	wcel 958	. . . 4 wff u e. NrmCVec
6		vd	. . . . . 6 set d
7	6	cv 955	. . . . 5 class d
8		cnm 8209	. . . . . . 7 class norm
9	3, 8	cfv 3182	. . . . . 6 class (norm` u)
10		cnsb 8208	. . . . . . 7 class -v
11	3, 10	cfv 3182	. . . . . 6 class (-v` u)
12	9, 11	ccom 3174	. . . . 5 class ((norm` u) o. (-v` u))
13	7, 12	wceq 956	. . . 4 wff d = ((norm` u) o. (-v` u))
14	5, 13	wa 223	. . 3 wff (u e. NrmCVec /\ d = ((norm` u) o. (-v` u)))
15	14, 2, 6	copab 2666	. 2 class {<.u, d>. | (u e. NrmCVec /\ d = ((norm` u) o. (-v` u)))}
16	1, 15	wceq 956	1 wff IndMet = {<.u, d>. | (u e. NrmCVec /\ d = ((norm` u) o. (-v` u)))}

This definition is referenced by:  imsval 8316

Copyright terms: Public domain