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=normCV⁡U
Assertion nvmtri ⊢U∈NrmCVec∧A∈X∧B∈X→N⁡AMB≤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=normCV⁡U
4 neg1cn ⊢−1∈ℂ
5 eqid ⊢⋅𝑠OLD⁡U=⋅𝑠OLD⁡U
6 1 5 nvscl ⊢U∈NrmCVec∧−1∈ℂ∧B∈X→-1⋅𝑠OLD⁡UB∈X
7 4 6 mp3an2 ⊢U∈NrmCVec∧B∈X→-1⋅𝑠OLD⁡UB∈X
8 7 3adant2 ⊢U∈NrmCVec∧A∈X∧B∈X→-1⋅𝑠OLD⁡UB∈X
9 eqid ⊢+v⁡U=+v⁡U
10 1 9 3 nvtri ⊢U∈NrmCVec∧A∈X∧-1⋅𝑠OLD⁡UB∈X→N⁡A+v⁡U-1⋅𝑠OLD⁡UB≤N⁡A+N⁡-1⋅𝑠OLD⁡UB
11 8 10 syld3an3 ⊢U∈NrmCVec∧A∈X∧B∈X→N⁡A+v⁡U-1⋅𝑠OLD⁡UB≤N⁡A+N⁡-1⋅𝑠OLD⁡UB
12 1 9 5 2 nvmval ⊢U∈NrmCVec∧A∈X∧B∈X→AMB=A+v⁡U-1⋅𝑠OLD⁡UB
13 12 fveq2d ⊢U∈NrmCVec∧A∈X∧B∈X→N⁡AMB=N⁡A+v⁡U-1⋅𝑠OLD⁡UB
14 1 5 3 nvs ⊢U∈NrmCVec∧−1∈ℂ∧B∈X→N⁡-1⋅𝑠OLD⁡UB=−1⁢N⁡B
15 4 14 mp3an2 ⊢U∈NrmCVec∧B∈X→N⁡-1⋅𝑠OLD⁡UB=−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⁡UB
26 25 3adant2 ⊢U∈NrmCVec∧A∈X∧B∈X→N⁡B=N⁡-1⋅𝑠OLD⁡UB
27 26 oveq2d ⊢U∈NrmCVec∧A∈X∧B∈X→N⁡A+N⁡B=N⁡A+N⁡-1⋅𝑠OLD⁡UB
28 11 13 27 3brtr4d ⊢U∈NrmCVec∧A∈X∧B∈X→N⁡AMB≤N⁡A+N⁡B