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 ⊢ V = Base W
ncvsprp.n ⊢ N = norm ⁡ W
ncvsprp.s ⊢ · ˙ = ⋅ W
ncvsdif.p ⊢ + ˙ = + W
Assertion ncvsdif ⊢ W ∈ NrmVec ∩ ℂVec ∧ A ∈ V ∧ B ∈ V → N ⁡ A + ˙ -1 · ˙ B = N ⁡ B + ˙ -1 · ˙ A

Proof

Step Hyp Ref Expression
1 ncvsprp.v ⊢ V = Base W
2 ncvsprp.n ⊢ N = norm ⁡ W
3 ncvsprp.s ⊢ · ˙ = ⋅ W
4 ncvsdif.p ⊢ + ˙ = + W
5 elin ⊢ W ∈ NrmVec ∩ ℂVec ↔ W ∈ NrmVec ∧ W ∈ ℂVec
6 id ⊢ W ∈ ℂVec → W ∈ ℂVec
7 6 cvsclm ⊢ W ∈ ℂVec → W ∈ CMod
8 5 7 simplbiim ⊢ W ∈ NrmVec ∩ ℂVec → W ∈ CMod
9 eqid ⊢ - W = - W
10 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
11 1 4 9 10 3 clmvsubval ⊢ W ∈ CMod ∧ A ∈ V ∧ B ∈ V → A - W B = A + ˙ -1 · ˙ B
12 11 eqcomd ⊢ W ∈ CMod ∧ A ∈ V ∧ B ∈ V → A + ˙ -1 · ˙ B = A - W B
13 8 12 syl3an1 ⊢ W ∈ NrmVec ∩ ℂVec ∧ A ∈ V ∧ B ∈ V → A + ˙ -1 · ˙ B = A - W B
14 13 fveq2d ⊢ W ∈ NrmVec ∩ ℂVec ∧ A ∈ V ∧ B ∈ V → N ⁡ A + ˙ -1 · ˙ B = N ⁡ A - W B
15 nvcnlm ⊢ W ∈ NrmVec → W ∈ NrmMod
16 nlmngp ⊢ W ∈ NrmMod → W ∈ NrmGrp
17 15 16 syl ⊢ W ∈ NrmVec → W ∈ NrmGrp
18 17 adantr ⊢ W ∈ NrmVec ∧ W ∈ ℂVec → W ∈ NrmGrp
19 5 18 sylbi ⊢ W ∈ NrmVec ∩ ℂVec → W ∈ NrmGrp
20 1 2 9 nmsub ⊢ W ∈ NrmGrp ∧ A ∈ V ∧ B ∈ V → N ⁡ A - W B = N ⁡ B - W A
21 19 20 syl3an1 ⊢ W ∈ NrmVec ∩ ℂVec ∧ A ∈ V ∧ B ∈ V → N ⁡ A - W B = N ⁡ B - W A
22 8 3ad2ant1 ⊢ W ∈ NrmVec ∩ ℂVec ∧ A ∈ V ∧ B ∈ V → W ∈ CMod
23 simp3 ⊢ W ∈ NrmVec ∩ ℂVec ∧ A ∈ V ∧ B ∈ V → B ∈ V
24 simp2 ⊢ W ∈ NrmVec ∩ ℂVec ∧ A ∈ V ∧ B ∈ V → A ∈ V
25 1 4 9 10 3 clmvsubval ⊢ W ∈ CMod ∧ B ∈ V ∧ A ∈ V → B - W A = B + ˙ -1 · ˙ A
26 22 23 24 25 syl3anc ⊢ W ∈ NrmVec ∩ ℂVec ∧ A ∈ V ∧ B ∈ V → B - W A = B + ˙ -1 · ˙ A
27 26 fveq2d ⊢ W ∈ NrmVec ∩ ℂVec ∧ A ∈ V ∧ B ∈ V → N ⁡ B - W A = N ⁡ B + ˙ -1 · ˙ A
28 14 21 27 3eqtrd ⊢ W ∈ NrmVec ∩ ℂVec ∧ A ∈ V ∧ B ∈ V → N ⁡ A + ˙ -1 · ˙ B = N ⁡ B + ˙ -1 · ˙ A