# 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 𝑋 = ( BaseSet ‘ 𝑈 )
imsdval.3 𝑀 = ( −𝑣𝑈 )
imsdval.6 𝑁 = ( normCV𝑈 )
imsdval.8 𝐷 = ( IndMet ‘ 𝑈 )
Assertion imsdval ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) )

### Proof

Step Hyp Ref Expression
1 imsdval.1 𝑋 = ( BaseSet ‘ 𝑈 )
2 imsdval.3 𝑀 = ( −𝑣𝑈 )
3 imsdval.6 𝑁 = ( normCV𝑈 )
4 imsdval.8 𝐷 = ( IndMet ‘ 𝑈 )
5 2 3 4 imsval ( 𝑈 ∈ NrmCVec → 𝐷 = ( 𝑁𝑀 ) )
6 5 3ad2ant1 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → 𝐷 = ( 𝑁𝑀 ) )
7 6 fveq1d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐷 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( 𝑁𝑀 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
8 1 2 nvmf ( 𝑈 ∈ NrmCVec → 𝑀 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
9 opelxpi ( ( 𝐴𝑋𝐵𝑋 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑋 ) )
10 fvco3 ( ( 𝑀 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑋 ) ) → ( ( 𝑁𝑀 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝑁 ‘ ( 𝑀 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
11 8 9 10 syl2an ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴𝑋𝐵𝑋 ) ) → ( ( 𝑁𝑀 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝑁 ‘ ( 𝑀 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
12 11 3impb ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( ( 𝑁𝑀 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝑁 ‘ ( 𝑀 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
13 7 12 eqtrd ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐷 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝑁 ‘ ( 𝑀 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
14 df-ov ( 𝐴 𝐷 𝐵 ) = ( 𝐷 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
15 df-ov ( 𝐴 𝑀 𝐵 ) = ( 𝑀 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
16 15 fveq2i ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) = ( 𝑁 ‘ ( 𝑀 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
17 13 14 16 3eqtr4g ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) )