Metamath Proof Explorer

Theorem ncvspds

Description: Value of the distance function in terms of the norm of a normed subcomplex vector space. Equation 1 of Kreyszig p. 59. (Contributed by NM, 28-Nov-2006) (Revised by AV, 13-Oct-2021)

Ref Expression
Hypotheses ncvspds.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
ncvspds.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
ncvspds.p ⊢ + = ( +g ‘ 𝐺 )
ncvspds.d ⊢ 𝐷 = ( dist ‘ 𝐺 )
ncvspds.s ⊢ · = ( ·𝑠 ‘ 𝐺 )
Assertion ncvspds ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 ncvspds.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
2 ncvspds.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
3 ncvspds.p ⊢ + = ( +g ‘ 𝐺 )
4 ncvspds.d ⊢ 𝐷 = ( dist ‘ 𝐺 )
5 ncvspds.s ⊢ · = ( ·𝑠 ‘ 𝐺 )
6 elin ⊢ ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ↔ ( 𝐺 ∈ NrmVec ∧ 𝐺 ∈ ℂVec ) )
7 nvcnlm ⊢ ( 𝐺 ∈ NrmVec → 𝐺 ∈ NrmMod )
8 nlmngp ⊢ ( 𝐺 ∈ NrmMod → 𝐺 ∈ NrmGrp )
9 7 8 syl ⊢ ( 𝐺 ∈ NrmVec → 𝐺 ∈ NrmGrp )
10 9 adantr ⊢ ( ( 𝐺 ∈ NrmVec ∧ 𝐺 ∈ ℂVec ) → 𝐺 ∈ NrmGrp )
11 6 10 sylbi ⊢ ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) → 𝐺 ∈ NrmGrp )
12 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
13 1 2 12 4 ngpds ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝐺 ) 𝐵 ) ) )
14 11 13 syl3an1 ⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝐺 ) 𝐵 ) ) )
15 id ⊢ ( 𝐺 ∈ ℂVec → 𝐺 ∈ ℂVec )
16 15 cvsclm ⊢ ( 𝐺 ∈ ℂVec → 𝐺 ∈ ℂMod )
17 6 16 simplbiim ⊢ ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) → 𝐺 ∈ ℂMod )
18 eqid ⊢ ( Scalar ‘ 𝐺 ) = ( Scalar ‘ 𝐺 )
19 2 3 12 18 5 clmvsubval ⊢ ( ( 𝐺 ∈ ℂMod ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( -g ‘ 𝐺 ) 𝐵 ) = ( 𝐴 + ( - 1 · 𝐵 ) ) )
20 17 19 syl3an1 ⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( -g ‘ 𝐺 ) 𝐵 ) = ( 𝐴 + ( - 1 · 𝐵 ) ) )
21 20 fveq2d ⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝐺 ) 𝐵 ) ) = ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) )
22 14 21 eqtrd ⊢ ( ( 𝐺 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) )