This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem norm3dif2

Description: Norm of differences around common element. (Contributed by NM, 18-Apr-2007) (New usage is discouraged.)

Ref Expression
Assertion norm3dif2 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → norm ℎ ⁡ A - ℎ B ≤ norm ℎ ⁡ C - ℎ A + norm ℎ ⁡ C - ℎ B

Proof

Step Hyp Ref Expression
1 norm3dif ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → norm ℎ ⁡ A - ℎ B ≤ norm ℎ ⁡ A - ℎ C + norm ℎ ⁡ C - ℎ B
2 normsub ⊢ A ∈ ℋ ∧ C ∈ ℋ → norm ℎ ⁡ A - ℎ C = norm ℎ ⁡ C - ℎ A
3 2 3adant2 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → norm ℎ ⁡ A - ℎ C = norm ℎ ⁡ C - ℎ A
4 3 oveq1d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → norm ℎ ⁡ A - ℎ C + norm ℎ ⁡ C - ℎ B = norm ℎ ⁡ C - ℎ A + norm ℎ ⁡ C - ℎ B
5 1 4 breqtrd ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → norm ℎ ⁡ A - ℎ B ≤ norm ℎ ⁡ C - ℎ A + norm ℎ ⁡ C - ℎ B