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 mullidd ⊢ U ∈ NrmCVec ∧ B ∈ X → 1 ⁢ N ⁡ B = N ⁡ B
24 20 23 eqtrid ⊢ 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