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ℎ ‘ ( 𝐶 −ℎ 𝐵 ) ) ) )