This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem norm3lem

Description: Lemma involving norm of differences in Hilbert space. (Contributed by NM, 18-Aug-1999) (New usage is discouraged.)

Ref Expression
Hypotheses norm3dif.1 
|- A e. ~H
norm3dif.2 
|- B e. ~H
norm3dif.3 
|- C e. ~H
norm3lem.4 
|- D e. RR
Assertion norm3lem 
|- ( ( ( normh ` ( A -h C ) ) < ( D / 2 ) /\ ( normh ` ( C -h B ) ) < ( D / 2 ) ) -> ( normh ` ( A -h B ) ) < D )

Proof

Step Hyp Ref Expression
1 norm3dif.1 
 |-  A e. ~H
2 norm3dif.2 
 |-  B e. ~H
3 norm3dif.3 
 |-  C e. ~H
4 norm3lem.4 
 |-  D e. RR
5 1 2 3 norm3difi 
 |-  ( normh ` ( A -h B ) ) <_ ( ( normh ` ( A -h C ) ) + ( normh ` ( C -h B ) ) )
6 1 3 hvsubcli 
 |-  ( A -h C ) e. ~H
7 6 normcli 
 |-  ( normh ` ( A -h C ) ) e. RR
8 3 2 hvsubcli 
 |-  ( C -h B ) e. ~H
9 8 normcli 
 |-  ( normh ` ( C -h B ) ) e. RR
10 4 rehalfcli 
 |-  ( D / 2 ) e. RR
11 7 9 10 10 lt2addi 
 |-  ( ( ( normh ` ( A -h C ) ) < ( D / 2 ) /\ ( normh ` ( C -h B ) ) < ( D / 2 ) ) -> ( ( normh ` ( A -h C ) ) + ( normh ` ( C -h B ) ) ) < ( ( D / 2 ) + ( D / 2 ) ) )
12 1 2 hvsubcli 
 |-  ( A -h B ) e. ~H
13 12 normcli 
 |-  ( normh ` ( A -h B ) ) e. RR
14 7 9 readdcli 
 |-  ( ( normh ` ( A -h C ) ) + ( normh ` ( C -h B ) ) ) e. RR
15 10 10 readdcli 
 |-  ( ( D / 2 ) + ( D / 2 ) ) e. RR
16 13 14 15 lelttri 
 |-  ( ( ( normh ` ( A -h B ) ) <_ ( ( normh ` ( A -h C ) ) + ( normh ` ( C -h B ) ) ) /\ ( ( normh ` ( A -h C ) ) + ( normh ` ( C -h B ) ) ) < ( ( D / 2 ) + ( D / 2 ) ) ) -> ( normh ` ( A -h B ) ) < ( ( D / 2 ) + ( D / 2 ) ) )
17 5 11 16 sylancr 
 |-  ( ( ( normh ` ( A -h C ) ) < ( D / 2 ) /\ ( normh ` ( C -h B ) ) < ( D / 2 ) ) -> ( normh ` ( A -h B ) ) < ( ( D / 2 ) + ( D / 2 ) ) )
18 10 recni 
 |-  ( D / 2 ) e. CC
19 18 2timesi 
 |-  ( 2 x. ( D / 2 ) ) = ( ( D / 2 ) + ( D / 2 ) )
20 4 recni 
 |-  D e. CC
21 2cn 
 |-  2 e. CC
22 2ne0 
 |-  2 =/= 0
23 20 21 22 divcan2i 
 |-  ( 2 x. ( D / 2 ) ) = D
24 19 23 eqtr3i 
 |-  ( ( D / 2 ) + ( D / 2 ) ) = D
25 17 24 breqtrdi 
 |-  ( ( ( normh ` ( A -h C ) ) < ( D / 2 ) /\ ( normh ` ( C -h B ) ) < ( D / 2 ) ) -> ( normh ` ( A -h B ) ) < D )