This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( -v ` U )
imsval.6 
|- N = ( normCV ` U )
imsval.8 
|- D = ( IndMet ` U )
Assertion imsval 
|- ( U e. NrmCVec -> D = ( N o. M ) )

Proof

Step Hyp Ref Expression
1 imsval.3 
 |-  M = ( -v ` U )
2 imsval.6 
 |-  N = ( normCV ` U )
3 imsval.8 
 |-  D = ( IndMet ` U )
4 fveq2 
 |-  ( u = U -> ( normCV ` u ) = ( normCV ` U ) )
5 fveq2 
 |-  ( u = U -> ( -v ` u ) = ( -v ` U ) )
6 4 5 coeq12d 
 |-  ( u = U -> ( ( normCV ` u ) o. ( -v ` u ) ) = ( ( normCV ` U ) o. ( -v ` U ) ) )
7 df-ims 
 |-  IndMet = ( u e. NrmCVec |-> ( ( normCV ` u ) o. ( -v ` u ) ) )
8 fvex 
 |-  ( normCV ` U ) e. _V
9 fvex 
 |-  ( -v ` U ) e. _V
10 8 9 coex 
 |-  ( ( normCV ` U ) o. ( -v ` U ) ) e. _V
11 6 7 10 fvmpt 
 |-  ( U e. NrmCVec -> ( IndMet ` U ) = ( ( normCV ` U ) o. ( -v ` U ) ) )
12 2 1 coeq12i 
 |-  ( N o. M ) = ( ( normCV ` U ) o. ( -v ` U ) )
13 11 3 12 3eqtr4g 
 |-  ( U e. NrmCVec -> D = ( N o. M ) )