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 e. ~H /\ B e. ~H /\ C e. ~H ) -> ( normh ` ( A -h B ) ) <_ ( ( normh ` ( C -h A ) ) + ( normh ` ( C -h B ) ) ) )

Proof

Step Hyp Ref Expression
1 norm3dif 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( normh ` ( A -h B ) ) <_ ( ( normh ` ( A -h C ) ) + ( normh ` ( C -h B ) ) ) )
2 normsub 
 |-  ( ( A e. ~H /\ C e. ~H ) -> ( normh ` ( A -h C ) ) = ( normh ` ( C -h A ) ) )
3 2 3adant2 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( normh ` ( A -h C ) ) = ( normh ` ( C -h A ) ) )
4 3 oveq1d 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( normh ` ( A -h C ) ) + ( normh ` ( C -h B ) ) ) = ( ( normh ` ( C -h A ) ) + ( normh ` ( C -h B ) ) ) )
5 1 4 breqtrd 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( normh ` ( A -h B ) ) <_ ( ( normh ` ( C -h A ) ) + ( normh ` ( C -h B ) ) ) )