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

Metamath Proof Explorer

Theorem imsdval

Description: Value of the induced metric (distance function) of a normed complex vector space. Equation 1 of Kreyszig p. 59. (Contributed by NM, 11-Sep-2007) (Revised by Mario Carneiro, 27-Dec-2014) (New usage is discouraged.)

Ref Expression
Hypotheses imsdval.1 
|- X = ( BaseSet ` U )
imsdval.3 
|- M = ( -v ` U )
imsdval.6 
|- N = ( normCV ` U )
imsdval.8 
|- D = ( IndMet ` U )
Assertion imsdval 
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A D B ) = ( N ` ( A M B ) ) )

Proof

Step Hyp Ref Expression
1 imsdval.1 
 |-  X = ( BaseSet ` U )
2 imsdval.3 
 |-  M = ( -v ` U )
3 imsdval.6 
 |-  N = ( normCV ` U )
4 imsdval.8 
 |-  D = ( IndMet ` U )
5 2 3 4 imsval 
 |-  ( U e. NrmCVec -> D = ( N o. M ) )
6 5 3ad2ant1 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> D = ( N o. M ) )
7 6 fveq1d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( D ` <. A , B >. ) = ( ( N o. M ) ` <. A , B >. ) )
8 1 2 nvmf 
 |-  ( U e. NrmCVec -> M : ( X X. X ) --> X )
9 opelxpi 
 |-  ( ( A e. X /\ B e. X ) -> <. A , B >. e. ( X X. X ) )
10 fvco3 
 |-  ( ( M : ( X X. X ) --> X /\ <. A , B >. e. ( X X. X ) ) -> ( ( N o. M ) ` <. A , B >. ) = ( N ` ( M ` <. A , B >. ) ) )
11 8 9 10 syl2an 
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> ( ( N o. M ) ` <. A , B >. ) = ( N ` ( M ` <. A , B >. ) ) )
12 11 3impb 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N o. M ) ` <. A , B >. ) = ( N ` ( M ` <. A , B >. ) ) )
13 7 12 eqtrd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( D ` <. A , B >. ) = ( N ` ( M ` <. A , B >. ) ) )
14 df-ov 
 |-  ( A D B ) = ( D ` <. A , B >. )
15 df-ov 
 |-  ( A M B ) = ( M ` <. A , B >. )
16 15 fveq2i 
 |-  ( N ` ( A M B ) ) = ( N ` ( M ` <. A , B >. ) )
17 13 14 16 3eqtr4g 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A D B ) = ( N ` ( A M B ) ) )