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 )