Description: Value of the induced metric of a normed complex vector space. (Contributed by NM, 11-Sep-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | imsval.3 | |
|
imsval.6 | |
||
imsval.8 | |
||
Assertion | imsval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imsval.3 | |
|
2 | imsval.6 | |
|
3 | imsval.8 | |
|
4 | fveq2 | |
|
5 | fveq2 | |
|
6 | 4 5 | coeq12d | |
7 | df-ims | |
|
8 | fvex | |
|
9 | fvex | |
|
10 | 8 9 | coex | |
11 | 6 7 10 | fvmpt | |
12 | 2 1 | coeq12i | |
13 | 11 3 12 | 3eqtr4g | |