Metamath Proof Explorer

Theorem ncvsdif

Description: The norm of the difference between two vectors. (Contributed by NM, 1-Dec-2006) (Revised by AV, 8-Oct-2021)

Ref Expression
Hypotheses ncvsprp.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
ncvsprp.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
ncvsprp.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
ncvsdif.p ⊢ + = ( +g ‘ 𝑊 )
Assertion ncvsdif ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐵 + ( - 1 · 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 ncvsprp.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 ncvsprp.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
3 ncvsprp.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
4 ncvsdif.p ⊢ + = ( +g ‘ 𝑊 )
5 elin ⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ↔ ( 𝑊 ∈ NrmVec ∧ 𝑊 ∈ ℂVec ) )
6 id ⊢ ( 𝑊 ∈ ℂVec → 𝑊 ∈ ℂVec )
7 6 cvsclm ⊢ ( 𝑊 ∈ ℂVec → 𝑊 ∈ ℂMod )
8 5 7 simplbiim ⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) → 𝑊 ∈ ℂMod )
9 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
10 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
11 1 4 9 10 3 clmvsubval ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) = ( 𝐴 + ( - 1 · 𝐵 ) ) )
12 11 eqcomd ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 + ( - 1 · 𝐵 ) ) = ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) )
13 8 12 syl3an1 ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 + ( - 1 · 𝐵 ) ) = ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) )
14 13 fveq2d ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) )
15 nvcnlm ⊢ ( 𝑊 ∈ NrmVec → 𝑊 ∈ NrmMod )
16 nlmngp ⊢ ( 𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp )
17 15 16 syl ⊢ ( 𝑊 ∈ NrmVec → 𝑊 ∈ NrmGrp )
18 17 adantr ⊢ ( ( 𝑊 ∈ NrmVec ∧ 𝑊 ∈ ℂVec ) → 𝑊 ∈ NrmGrp )
19 5 18 sylbi ⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) → 𝑊 ∈ NrmGrp )
20 1 2 9 nmsub ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) = ( 𝑁 ‘ ( 𝐵 ( -g ‘ 𝑊 ) 𝐴 ) ) )
21 19 20 syl3an1 ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) = ( 𝑁 ‘ ( 𝐵 ( -g ‘ 𝑊 ) 𝐴 ) ) )
22 8 3ad2ant1 ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝑊 ∈ ℂMod )
23 simp3 ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ 𝑉 )
24 simp2 ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
25 1 4 9 10 3 clmvsubval ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐵 ( -g ‘ 𝑊 ) 𝐴 ) = ( 𝐵 + ( - 1 · 𝐴 ) ) )
26 22 23 24 25 syl3anc ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐵 ( -g ‘ 𝑊 ) 𝐴 ) = ( 𝐵 + ( - 1 · 𝐴 ) ) )
27 26 fveq2d ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐵 ( -g ‘ 𝑊 ) 𝐴 ) ) = ( 𝑁 ‘ ( 𝐵 + ( - 1 · 𝐴 ) ) ) )
28 14 21 27 3eqtrd ⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐵 + ( - 1 · 𝐴 ) ) ) )