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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nvnd.5 ⊢ 𝑍 = ( 0vec ‘ 𝑈 )
nvnd.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
nvnd.8 ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
Assertion nvnd ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) = ( 𝐴 𝐷 𝑍 ) )

Proof

Step Hyp Ref Expression
1 nvnd.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nvnd.5 ⊢ 𝑍 = ( 0vec ‘ 𝑈 )
3 nvnd.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
4 nvnd.8 ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
5 1 2 nvzcl ⊢ ( 𝑈 ∈ NrmCVec → 𝑍 ∈ 𝑋 )
6 5 adantr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → 𝑍 ∈ 𝑋 )
7 eqid ⊢ ( −𝑣 ‘ 𝑈 ) = ( −𝑣 ‘ 𝑈 )
8 1 7 3 4 imsdval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ) → ( 𝐴 𝐷 𝑍 ) = ( 𝑁 ‘ ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝑍 ) ) )
9 6 8 mpd3an3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐷 𝑍 ) = ( 𝑁 ‘ ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝑍 ) ) )
10 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
11 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
12 1 10 11 7 nvmval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ) → ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝑍 ) = ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) )
13 6 12 mpd3an3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝑍 ) = ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) )
14 neg1cn ⊢ - 1 ∈ ℂ
15 11 2 nvsz ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ) → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) = 𝑍 )
16 14 15 mpan2 ⊢ ( 𝑈 ∈ NrmCVec → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) = 𝑍 )
17 16 oveq2d ⊢ ( 𝑈 ∈ NrmCVec → ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) = ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝑍 ) )
18 17 adantr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑍 ) ) = ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝑍 ) )
19 1 10 2 nv0rid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝑍 ) = 𝐴 )
20 13 18 19 3eqtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝑍 ) = 𝐴 )
21 20 fveq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝑍 ) ) = ( 𝑁 ‘ 𝐴 ) )
22 9 21 eqtr2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) = ( 𝐴 𝐷 𝑍 ) )