Metamath Proof Explorer


Theorem imsval

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 M=-vU
imsval.6 N=normCVU
imsval.8 D=IndMetU
Assertion imsval UNrmCVecD=NM

Proof

Step Hyp Ref Expression
1 imsval.3 M=-vU
2 imsval.6 N=normCVU
3 imsval.8 D=IndMetU
4 fveq2 u=UnormCVu=normCVU
5 fveq2 u=U-vu=-vU
6 4 5 coeq12d u=UnormCVu-vu=normCVU-vU
7 df-ims IndMet=uNrmCVecnormCVu-vu
8 fvex normCVUV
9 fvex -vUV
10 8 9 coex normCVU-vUV
11 6 7 10 fvmpt UNrmCVecIndMetU=normCVU-vU
12 2 1 coeq12i NM=normCVU-vU
13 11 3 12 3eqtr4g UNrmCVecD=NM