Theorem norm3adifi

Description: Norm of differences around common element. Part of Lemma 3.6 of Beran p. 101. (Contributed by NM, 3-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypothesis	norm3adift.1	|- C e. ~H
Assertion	norm3adifi	|- ( ( A e. ~H /\ B e. ~H ) -> ( abs ` ( ( normh ` ( A -h C ) ) - ( normh ` ( B -h C ) ) ) ) <_ ( normh ` ( A -h B ) ) )

Proof

Step	Hyp	Ref	Expression
1		norm3adift.1	|- C e. ~H
2		fvoveq1	|- ( A = if ( A e. ~H , A , 0h ) -> ( normh ` ( A -h C ) ) = ( normh ` ( if ( A e. ~H , A , 0h ) -h C ) ) )
3	2	fvoveq1d	|- ( A = if ( A e. ~H , A , 0h ) -> ( abs ` ( ( normh ` ( A -h C ) ) - ( normh ` ( B -h C ) ) ) ) = ( abs ` ( ( normh ` ( if ( A e. ~H , A , 0h ) -h C ) ) - ( normh ` ( B -h C ) ) ) ) )
4		fvoveq1	|- ( A = if ( A e. ~H , A , 0h ) -> ( normh ` ( A -h B ) ) = ( normh ` ( if ( A e. ~H , A , 0h ) -h B ) ) )
5	3 4	breq12d	|- ( A = if ( A e. ~H , A , 0h ) -> ( ( abs ` ( ( normh ` ( A -h C ) ) - ( normh ` ( B -h C ) ) ) ) <_ ( normh ` ( A -h B ) ) <-> ( abs ` ( ( normh ` ( if ( A e. ~H , A , 0h ) -h C ) ) - ( normh ` ( B -h C ) ) ) ) <_ ( normh ` ( if ( A e. ~H , A , 0h ) -h B ) ) ) )
6		fvoveq1	|- ( B = if ( B e. ~H , B , 0h ) -> ( normh ` ( B -h C ) ) = ( normh ` ( if ( B e. ~H , B , 0h ) -h C ) ) )
7	6	oveq2d	|- ( B = if ( B e. ~H , B , 0h ) -> ( ( normh ` ( if ( A e. ~H , A , 0h ) -h C ) ) - ( normh ` ( B -h C ) ) ) = ( ( normh ` ( if ( A e. ~H , A , 0h ) -h C ) ) - ( normh ` ( if ( B e. ~H , B , 0h ) -h C ) ) ) )
8	7	fveq2d	|- ( B = if ( B e. ~H , B , 0h ) -> ( abs ` ( ( normh ` ( if ( A e. ~H , A , 0h ) -h C ) ) - ( normh ` ( B -h C ) ) ) ) = ( abs ` ( ( normh ` ( if ( A e. ~H , A , 0h ) -h C ) ) - ( normh ` ( if ( B e. ~H , B , 0h ) -h C ) ) ) ) )
9		oveq2	|- ( B = if ( B e. ~H , B , 0h ) -> ( if ( A e. ~H , A , 0h ) -h B ) = ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) )
10	9	fveq2d	|- ( B = if ( B e. ~H , B , 0h ) -> ( normh ` ( if ( A e. ~H , A , 0h ) -h B ) ) = ( normh ` ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) ) )
11	8 10	breq12d	|- ( B = if ( B e. ~H , B , 0h ) -> ( ( abs ` ( ( normh ` ( if ( A e. ~H , A , 0h ) -h C ) ) - ( normh ` ( B -h C ) ) ) ) <_ ( normh ` ( if ( A e. ~H , A , 0h ) -h B ) ) <-> ( abs ` ( ( normh ` ( if ( A e. ~H , A , 0h ) -h C ) ) - ( normh ` ( if ( B e. ~H , B , 0h ) -h C ) ) ) ) <_ ( normh ` ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) ) ) )
12		ifhvhv0	|- if ( A e. ~H , A , 0h ) e. ~H
13		ifhvhv0	|- if ( B e. ~H , B , 0h ) e. ~H
14	12 13 1	norm3adifii	|- ( abs ` ( ( normh ` ( if ( A e. ~H , A , 0h ) -h C ) ) - ( normh ` ( if ( B e. ~H , B , 0h ) -h C ) ) ) ) <_ ( normh ` ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) )
15	5 11 14	dedth2h	|- ( ( A e. ~H /\ B e. ~H ) -> ( abs ` ( ( normh ` ( A -h C ) ) - ( normh ` ( B -h C ) ) ) ) <_ ( normh ` ( A -h B ) ) )