Metamath Proof Explorer

Theorem norm3adifii

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

Ref Expression
Hypotheses norm3dif.1 
|- A e. ~H
norm3dif.2 
|- B e. ~H
norm3dif.3 
|- C e. ~H
Assertion norm3adifii 
|- ( abs ` ( ( normh ` ( A -h C ) ) - ( normh ` ( B -h C ) ) ) ) <_ ( normh ` ( A -h B ) )

Proof

Step Hyp Ref Expression
1 norm3dif.1 
 |-  A e. ~H
2 norm3dif.2 
 |-  B e. ~H
3 norm3dif.3 
 |-  C e. ~H
4 1 3 hvsubcli 
 |-  ( A -h C ) e. ~H
5 4 normcli 
 |-  ( normh ` ( A -h C ) ) e. RR
6 5 recni 
 |-  ( normh ` ( A -h C ) ) e. CC
7 2 3 hvsubcli 
 |-  ( B -h C ) e. ~H
8 7 normcli 
 |-  ( normh ` ( B -h C ) ) e. RR
9 8 recni 
 |-  ( normh ` ( B -h C ) ) e. CC
10 6 9 negsubdi2i 
 |-  -u ( ( normh ` ( A -h C ) ) - ( normh ` ( B -h C ) ) ) = ( ( normh ` ( B -h C ) ) - ( normh ` ( A -h C ) ) )
11 2 3 1 norm3difi 
 |-  ( normh ` ( B -h C ) ) <_ ( ( normh ` ( B -h A ) ) + ( normh ` ( A -h C ) ) )
12 2 1 normsubi 
 |-  ( normh ` ( B -h A ) ) = ( normh ` ( A -h B ) )
13 12 oveq1i 
 |-  ( ( normh ` ( B -h A ) ) + ( normh ` ( A -h C ) ) ) = ( ( normh ` ( A -h B ) ) + ( normh ` ( A -h C ) ) )
14 11 13 breqtri 
 |-  ( normh ` ( B -h C ) ) <_ ( ( normh ` ( A -h B ) ) + ( normh ` ( A -h C ) ) )
15 1 2 hvsubcli 
 |-  ( A -h B ) e. ~H
16 15 normcli 
 |-  ( normh ` ( A -h B ) ) e. RR
17 8 5 16 lesubaddi 
 |-  ( ( ( normh ` ( B -h C ) ) - ( normh ` ( A -h C ) ) ) <_ ( normh ` ( A -h B ) ) <-> ( normh ` ( B -h C ) ) <_ ( ( normh ` ( A -h B ) ) + ( normh ` ( A -h C ) ) ) )
18 14 17 mpbir 
 |-  ( ( normh ` ( B -h C ) ) - ( normh ` ( A -h C ) ) ) <_ ( normh ` ( A -h B ) )
19 10 18 eqbrtri 
 |-  -u ( ( normh ` ( A -h C ) ) - ( normh ` ( B -h C ) ) ) <_ ( normh ` ( A -h B ) )
20 5 8 resubcli 
 |-  ( ( normh ` ( A -h C ) ) - ( normh ` ( B -h C ) ) ) e. RR
21 20 16 lenegcon1i 
 |-  ( -u ( ( normh ` ( A -h C ) ) - ( normh ` ( B -h C ) ) ) <_ ( normh ` ( A -h B ) ) <-> -u ( normh ` ( A -h B ) ) <_ ( ( normh ` ( A -h C ) ) - ( normh ` ( B -h C ) ) ) )
22 19 21 mpbi 
 |-  -u ( normh ` ( A -h B ) ) <_ ( ( normh ` ( A -h C ) ) - ( normh ` ( B -h C ) ) )
23 1 3 2 norm3difi 
 |-  ( normh ` ( A -h C ) ) <_ ( ( normh ` ( A -h B ) ) + ( normh ` ( B -h C ) ) )
24 5 8 16 lesubaddi 
 |-  ( ( ( normh ` ( A -h C ) ) - ( normh ` ( B -h C ) ) ) <_ ( normh ` ( A -h B ) ) <-> ( normh ` ( A -h C ) ) <_ ( ( normh ` ( A -h B ) ) + ( normh ` ( B -h C ) ) ) )
25 23 24 mpbir 
 |-  ( ( normh ` ( A -h C ) ) - ( normh ` ( B -h C ) ) ) <_ ( normh ` ( A -h B ) )
26 20 16 abslei 
 |-  ( ( abs ` ( ( normh ` ( A -h C ) ) - ( normh ` ( B -h C ) ) ) ) <_ ( normh ` ( A -h B ) ) <-> ( -u ( normh ` ( A -h B ) ) <_ ( ( normh ` ( A -h C ) ) - ( normh ` ( B -h C ) ) ) /\ ( ( normh ` ( A -h C ) ) - ( normh ` ( B -h C ) ) ) <_ ( normh ` ( A -h B ) ) ) )
27 22 25 26 mpbir2an 
 |-  ( abs ` ( ( normh ` ( A -h C ) ) - ( normh ` ( B -h C ) ) ) ) <_ ( normh ` ( A -h B ) )