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 = norm CV ⁡ U
imsdval.8 ⊢ D = IndMet ⁡ U
Assertion imsdval ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ 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 = norm CV ⁡ U
4 imsdval.8 ⊢ D = IndMet ⁡ U
5 2 3 4 imsval ⊢ U ∈ NrmCVec → D = N ∘ M
6 5 3ad2ant1 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → D = N ∘ M
7 6 fveq1d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → D ⁡ A B = N ∘ M ⁡ A B
8 1 2 nvmf ⊢ U ∈ NrmCVec → M : X × X ⟶ X
9 opelxpi ⊢ A ∈ X ∧ B ∈ X → A B ∈ X × X
10 fvco3 ⊢ M : X × X ⟶ X ∧ A B ∈ X × X → N ∘ M ⁡ A B = N ⁡ M ⁡ A B
11 8 9 10 syl2an ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → N ∘ M ⁡ A B = N ⁡ M ⁡ A B
12 11 3impb ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → N ∘ M ⁡ A B = N ⁡ M ⁡ A B
13 7 12 eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ 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 ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A D B = N ⁡ A M B