Metamath Proof Explorer

Definition df-ims

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cims 
 |-  IndMet
1 vu 
 |-  u
2 cnv 
 |-  NrmCVec
3 cnmcv 
 |-  normCV
4 1 cv 
 |-  u
5 4 3 cfv 
 |-  ( normCV ` u )
6 cnsb 
 |-  -v
7 4 6 cfv 
 |-  ( -v ` u )
8 5 7 ccom 
 |-  ( ( normCV ` u ) o. ( -v ` u ) )
9 1 2 8 cmpt 
 |-  ( u e. NrmCVec |-> ( ( normCV ` u ) o. ( -v ` u ) ) )
10 0 9 wceq 
 |-  IndMet = ( u e. NrmCVec |-> ( ( normCV ` u ) o. ( -v ` u ) ) )