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

Metamath Proof Explorer

Theorem imsdval2

Description: Value of the distance function of the induced metric of a normed complex vector space. Equation 1 of Kreyszig p. 59. (Contributed by NM, 28-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses imsdval2.1 ⊢ X = BaseSet ⁡ U
imsdval2.2 ⊢ G = + v ⁡ U
imsdval2.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
imsdval2.6 ⊢ N = norm CV ⁡ U
imsdval2.8 ⊢ D = IndMet ⁡ U
Assertion imsdval2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A D B = N ⁡ A G -1 S B

Proof

Step Hyp Ref Expression
1 imsdval2.1 ⊢ X = BaseSet ⁡ U
2 imsdval2.2 ⊢ G = + v ⁡ U
3 imsdval2.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
4 imsdval2.6 ⊢ N = norm CV ⁡ U
5 imsdval2.8 ⊢ D = IndMet ⁡ U
6 eqid ⊢ - v ⁡ U = - v ⁡ U
7 1 6 4 5 imsdval ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A D B = N ⁡ A - v ⁡ U B
8 1 2 3 6 nvmval ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A - v ⁡ U B = A G -1 S B
9 8 fveq2d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → N ⁡ A - v ⁡ U B = N ⁡ A G -1 S B
10 7 9 eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A D B = N ⁡ A G -1 S B