# 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 ) )`
` |-  ( ( 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 ) ) )`