Metamath Proof Explorer

Theorem nvtri

Description: Triangle inequality for the norm of a normed complex vector space. (Contributed by NM, 11-Nov-2006) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nvtri.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nvtri.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
nvtri.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
Assertion nvtri ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 nvtri.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nvtri.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 nvtri.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
4 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
5 4 smfval ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( 2nd ‘ ( 1st ‘ 𝑈 ) )
6 5 eqcomi ⊢ ( 2nd ‘ ( 1st ‘ 𝑈 ) ) = ( ·𝑠OLD ‘ 𝑈 )
7 eqid ⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
8 1 2 6 7 3 nvi ⊢ ( 𝑈 ∈ NrmCVec → ( ⟨ 𝐺 , ( 2nd ‘ ( 1st ‘ 𝑈 ) ) ⟩ ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = ( 0vec ‘ 𝑈 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 ( 2nd ‘ ( 1st ‘ 𝑈 ) ) 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) )
9 8 simp3d ⊢ ( 𝑈 ∈ NrmCVec → ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = ( 0vec ‘ 𝑈 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 ( 2nd ‘ ( 1st ‘ 𝑈 ) ) 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) )
10 simp3 ⊢ ( ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = ( 0vec ‘ 𝑈 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 ( 2nd ‘ ( 1st ‘ 𝑈 ) ) 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) → ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) )
11 10 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = ( 0vec ‘ 𝑈 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 ( 2nd ‘ ( 1st ‘ 𝑈 ) ) 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) )
12 9 11 syl ⊢ ( 𝑈 ∈ NrmCVec → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) )
13 fvoveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 𝑦 ) ) )
14 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑁 ‘ 𝑥 ) = ( 𝑁 ‘ 𝐴 ) )
15 14 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) = ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ 𝑦 ) ) )
16 13 15 breq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ↔ ( 𝑁 ‘ ( 𝐴 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ 𝑦 ) ) ) )
17 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐺 𝑦 ) = ( 𝐴 𝐺 𝐵 ) )
18 17 fveq2d ⊢ ( 𝑦 = 𝐵 → ( 𝑁 ‘ ( 𝐴 𝐺 𝑦 ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) )
19 fveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝑁 ‘ 𝑦 ) = ( 𝑁 ‘ 𝐵 ) )
20 19 oveq2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ 𝑦 ) ) = ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ 𝐵 ) ) )
21 18 20 breq12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑁 ‘ ( 𝐴 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ 𝑦 ) ) ↔ ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ 𝐵 ) ) ) )
22 16 21 rspc2v ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) → ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ 𝐵 ) ) ) )
23 12 22 syl5 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑈 ∈ NrmCVec → ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ 𝐵 ) ) ) )
24 23 3impia ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝑈 ∈ NrmCVec ) → ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ 𝐵 ) ) )
25 24 3comr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ 𝐵 ) ) )