Metamath Proof Explorer

Theorem nvnd

Description: The norm of a normed complex vector space expressed in terms of the distance function of its induced metric. Problem 1 of Kreyszig p. 63. (Contributed by NM, 4-Dec-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nvnd.1 ⊢ X = BaseSet ⁡ U
nvnd.5 ⊢ Z = 0 vec ⁡ U
nvnd.6 ⊢ N = norm CV ⁡ U
nvnd.8 ⊢ D = IndMet ⁡ U
Assertion nvnd ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A = A D Z

Proof

Step Hyp Ref Expression
1 nvnd.1 ⊢ X = BaseSet ⁡ U
2 nvnd.5 ⊢ Z = 0 vec ⁡ U
3 nvnd.6 ⊢ N = norm CV ⁡ U
4 nvnd.8 ⊢ D = IndMet ⁡ U
5 1 2 nvzcl ⊢ U ∈ NrmCVec → Z ∈ X
6 5 adantr ⊢ U ∈ NrmCVec ∧ A ∈ X → Z ∈ X
7 eqid ⊢ - v ⁡ U = - v ⁡ U
8 1 7 3 4 imsdval ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ Z ∈ X → A D Z = N ⁡ A - v ⁡ U Z
9 6 8 mpd3an3 ⊢ U ∈ NrmCVec ∧ A ∈ X → A D Z = N ⁡ A - v ⁡ U Z
10 eqid ⊢ + v ⁡ U = + v ⁡ U
11 eqid ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U
12 1 10 11 7 nvmval ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ Z ∈ X → A - v ⁡ U Z = A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U Z
13 6 12 mpd3an3 ⊢ U ∈ NrmCVec ∧ A ∈ X → A - v ⁡ U Z = A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U Z
14 neg1cn ⊢ − 1 ∈ ℂ
15 11 2 nvsz ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ → -1 ⋅ 𝑠OLD ⁡ U Z = Z
16 14 15 mpan2 ⊢ U ∈ NrmCVec → -1 ⋅ 𝑠OLD ⁡ U Z = Z
17 16 oveq2d ⊢ U ∈ NrmCVec → A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U Z = A + v ⁡ U Z
18 17 adantr ⊢ U ∈ NrmCVec ∧ A ∈ X → A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U Z = A + v ⁡ U Z
19 1 10 2 nv0rid ⊢ U ∈ NrmCVec ∧ A ∈ X → A + v ⁡ U Z = A
20 13 18 19 3eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X → A - v ⁡ U Z = A
21 20 fveq2d ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A - v ⁡ U Z = N ⁡ A
22 9 21 eqtr2d ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A = A D Z