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 ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ≤ ( ( normℎ ‘ ( 𝐶 −ℎ 𝐴 ) ) + ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 norm3dif ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ≤ ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) + ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) ) )
2 normsub ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) = ( normℎ ‘ ( 𝐶 −ℎ 𝐴 ) ) )
3 2 3adant2 ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) = ( normℎ ‘ ( 𝐶 −ℎ 𝐴 ) ) )
4 3 oveq1d ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( normℎ ‘ ( 𝐴 −ℎ 𝐶 ) ) + ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) ) = ( ( normℎ ‘ ( 𝐶 −ℎ 𝐴 ) ) + ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) ) )
5 1 4 breqtrd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ≤ ( ( normℎ ‘ ( 𝐶 −ℎ 𝐴 ) ) + ( normℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) ) )