Definition df-ims 9552

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 9542	. 2 class IndMet
2		vu	. . . . . 6 set u
3	2	cv 1297	. . . . 5 class u
4		cnv 9535	. . . . 5 class NrmCVec
5	3, 4	wcel 1300	. . . 4 wff u e. NrmCVec
6		vd	. . . . . 6 set d
7	6	cv 1297	. . . . 5 class d
8		cnm 9541	. . . . . . 7 class norm
9	3, 8	cfv 3998	. . . . . 6 class (norm` u)
10		cnsb 9540	. . . . . . 7 class -v
11	3, 10	cfv 3998	. . . . . 6 class (-v` u)
12	9, 11	ccom 3990	. . . . 5 class ((norm` u) o. (-v` u))
13	7, 12	wceq 1298	. . . 4 wff d = ((norm` u) o. (-v` u))
14	5, 13	wa 240	. . 3 wff (u e. NrmCVec /\ d = ((norm` u) o. (-v` u)))
15	14, 2, 6	copab 3395	. 2 class {<.u, d>. | (u e. NrmCVec /\ d = ((norm` u) o. (-v` u)))}
16	1, 15	wceq 1298	1 wff IndMet = {<.u, d>. | (u e. NrmCVec /\ d = ((norm` u) o. (-v` u)))}

This definition is referenced by:  imsval 9648

Copyright terms: Public domain