# Metamath Proof Explorer

## Theorem nvmtri

Description: Triangle inequality for the norm of a vector difference. (Contributed by NM, 27-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nvmtri.1 $⊢ X = BaseSet ⁡ U$
nvmtri.3 $⊢ M = - v ⁡ U$
nvmtri.6 $⊢ N = norm CV ⁡ U$
Assertion nvmtri $⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → N ⁡ A M B ≤ N ⁡ A + N ⁡ B$

### Proof

Step Hyp Ref Expression
1 nvmtri.1 $⊢ X = BaseSet ⁡ U$
2 nvmtri.3 $⊢ M = - v ⁡ U$
3 nvmtri.6 $⊢ N = norm CV ⁡ U$
4 neg1cn $⊢ − 1 ∈ ℂ$
5 eqid $⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U$
6 1 5 nvscl $⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ B ∈ X → -1 ⋅ 𝑠OLD ⁡ U B ∈ X$
7 4 6 mp3an2 $⊢ U ∈ NrmCVec ∧ B ∈ X → -1 ⋅ 𝑠OLD ⁡ U B ∈ X$
8 7 3adant2 $⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → -1 ⋅ 𝑠OLD ⁡ U B ∈ X$
9 eqid $⊢ + v ⁡ U = + v ⁡ U$
10 1 9 3 nvtri $⊢ U ∈ NrmCVec ∧ A ∈ X ∧ -1 ⋅ 𝑠OLD ⁡ U B ∈ X → N ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B ≤ N ⁡ A + N ⁡ -1 ⋅ 𝑠OLD ⁡ U B$
11 8 10 syld3an3 $⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → N ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B ≤ N ⁡ A + N ⁡ -1 ⋅ 𝑠OLD ⁡ U B$
12 1 9 5 2 nvmval $⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A M B = A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B$
13 12 fveq2d $⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → N ⁡ A M B = N ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B$
14 1 5 3 nvs $⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ B ∈ X → N ⁡ -1 ⋅ 𝑠OLD ⁡ U B = − 1 ⁢ N ⁡ B$
15 4 14 mp3an2 $⊢ U ∈ NrmCVec ∧ B ∈ X → N ⁡ -1 ⋅ 𝑠OLD ⁡ U B = − 1 ⁢ N ⁡ B$
16 ax-1cn $⊢ 1 ∈ ℂ$
17 16 absnegi $⊢ − 1 = 1$
18 abs1 $⊢ 1 = 1$
19 17 18 eqtri $⊢ − 1 = 1$
20 19 oveq1i $⊢ − 1 ⁢ N ⁡ B = 1 ⁢ N ⁡ B$
21 1 3 nvcl $⊢ U ∈ NrmCVec ∧ B ∈ X → N ⁡ B ∈ ℝ$
22 21 recnd $⊢ U ∈ NrmCVec ∧ B ∈ X → N ⁡ B ∈ ℂ$
23 22 mulid2d $⊢ U ∈ NrmCVec ∧ B ∈ X → 1 ⁢ N ⁡ B = N ⁡ B$
24 20 23 syl5eq $⊢ U ∈ NrmCVec ∧ B ∈ X → − 1 ⁢ N ⁡ B = N ⁡ B$
25 15 24 eqtr2d $⊢ U ∈ NrmCVec ∧ B ∈ X → N ⁡ B = N ⁡ -1 ⋅ 𝑠OLD ⁡ U B$
26 25 3adant2 $⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → N ⁡ B = N ⁡ -1 ⋅ 𝑠OLD ⁡ U B$
27 26 oveq2d $⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → N ⁡ A + N ⁡ B = N ⁡ A + N ⁡ -1 ⋅ 𝑠OLD ⁡ U B$
28 11 13 27 3brtr4d $⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → N ⁡ A M B ≤ N ⁡ A + N ⁡ B$