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 ⊢ 𝑋 = ( 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 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) )