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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nvmtri.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
nvmtri.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
Assertion nvmtri ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 nvmtri.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nvmtri.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
3 nvmtri.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
4 neg1cn ⊢ - 1 ∈ ℂ
5 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
6 1 5 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 )
7 4 6 mp3an2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 )
8 7 3adant2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 )
9 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
10 1 9 3 nvtri ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) )
11 8 10 syld3an3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) )
12 1 9 5 2 nvmval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐵 ) = ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) )
13 12 fveq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) = ( 𝑁 ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) )
14 1 5 3 nvs ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) = ( ( abs ‘ - 1 ) · ( 𝑁 ‘ 𝐵 ) ) )
15 4 14 mp3an2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) = ( ( abs ‘ - 1 ) · ( 𝑁 ‘ 𝐵 ) ) )
16 ax-1cn ⊢ 1 ∈ ℂ
17 16 absnegi ⊢ ( abs ‘ - 1 ) = ( abs ‘ 1 )
18 abs1 ⊢ ( abs ‘ 1 ) = 1
19 17 18 eqtri ⊢ ( abs ‘ - 1 ) = 1
20 19 oveq1i ⊢ ( ( abs ‘ - 1 ) · ( 𝑁 ‘ 𝐵 ) ) = ( 1 · ( 𝑁 ‘ 𝐵 ) )
21 1 3 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐵 ) ∈ ℝ )
22 21 recnd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐵 ) ∈ ℂ )
23 22 mulid2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( 1 · ( 𝑁 ‘ 𝐵 ) ) = ( 𝑁 ‘ 𝐵 ) )
24 20 23 syl5eq ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( ( abs ‘ - 1 ) · ( 𝑁 ‘ 𝐵 ) ) = ( 𝑁 ‘ 𝐵 ) )
25 15 24 eqtr2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐵 ) = ( 𝑁 ‘ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) )
26 25 3adant2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐵 ) = ( 𝑁 ‘ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) )
27 26 oveq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ 𝐵 ) ) = ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐵 ) ) ) )
28 11 13 27 3brtr4d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ 𝐵 ) ) )