Theorem norm3lemt 9019

Description: Lemma involving norm of differences in Hilbert space.

Assertion

Ref	Expression
norm3lemt	|- (((A e. H~ /\ B e. H~) /\ (C e. H~ /\ D e. RR)) -> (((normh` (A -h C)) < (D / 2) /\ (normh` (C -h B)) < (D / 2)) -> (normh` (A -h B)) < D))

Proof of Theorem norm3lemt

Step	Hyp	Ref	Expression
1		opreq1 3968	. . . . . 6 |- (A = if(A e. H~, A, 0h) -> (A -h C) = (if(A e. H~, A, 0h) -h C))
2	1	fveq2d 3728	. . . . 5 |- (A = if(A e. H~, A, 0h) -> (normh` (A -h C)) = (normh` (if(A e. H~, A, 0h) -h C)))
3	2	breq1d 2629	. . . 4 |- (A = if(A e. H~, A, 0h) -> ((normh` (A -h C)) < (D / 2) <-> (normh` (if(A e. H~, A, 0h) -h C)) < (D / 2)))
4	3	anbi1d 617	. . 3 |- (A = if(A e. H~, A, 0h) -> (((normh` (A -h C)) < (D / 2) /\ (normh` (C -h B)) < (D / 2)) <-> ((normh` (if(A e. H~, A, 0h) -h C)) < (D / 2) /\ (normh` (C -h B)) < (D / 2))))
5		opreq1 3968	. . . . 5 |- (A = if(A e. H~, A, 0h) -> (A -h B) = (if(A e. H~, A, 0h) -h B))
6	5	fveq2d 3728	. . . 4 |- (A = if(A e. H~, A, 0h) -> (normh` (A -h B)) = (normh` (if(A e. H~, A, 0h) -h B)))
7	6	breq1d 2629	. . 3 |- (A = if(A e. H~, A, 0h) -> ((normh` (A -h B)) < D <-> (normh` (if(A e. H~, A, 0h) -h B)) < D))
8	4, 7	imbi12d 626	. 2 |- (A = if(A e. H~, A, 0h) -> ((((normh` (A -h C)) < (D / 2) /\ (normh` (C -h B)) < (D / 2)) -> (normh` (A -h B)) < D) <-> (((normh` (if(A e. H~, A, 0h) -h C)) < (D / 2) /\ (normh` (C -h B)) < (D / 2)) -> (normh` (if(A e. H~, A, 0h) -h B)) < D)))
9		opreq2 3969	. . . . . 6 |- (B = if(B e. H~, B, 0h) -> (C -h B) = (C -h if(B e. H~, B, 0h)))
10	9	fveq2d 3728	. . . . 5 |- (B = if(B e. H~, B, 0h) -> (normh` (C -h B)) = (normh` (C -h if(B e. H~, B, 0h))))
11	10	breq1d 2629	. . . 4 |- (B = if(B e. H~, B, 0h) -> ((normh` (C -h B)) < (D / 2) <-> (normh` (C -h if(B e. H~, B, 0h))) < (D / 2)))
12	11	anbi2d 616	. . 3 |- (B = if(B e. H~, B, 0h) -> (((normh` (if(A e. H~, A, 0h) -h C)) < (D / 2) /\ (normh` (C -h B)) < (D / 2)) <-> ((normh` (if(A e. H~, A, 0h) -h C)) < (D / 2) /\ (normh` (C -h if(B e. H~, B, 0h))) < (D / 2))))
13		opreq2 3969	. . . . 5 |- (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)))
14	13	fveq2d 3728	. . . 4 |- (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))))
15	14	breq1d 2629	. . 3 |- (B = if(B e. H~, B, 0h) -> ((normh` (if(A e. H~, A, 0h) -h B)) < D <-> (normh` (if(A e. H~, A, 0h) -h if(B e. H~, B, 0h))) < D))
16	12, 15	imbi12d 626	. 2 |- (B = if(B e. H~, B, 0h) -> ((((normh` (if(A e. H~, A, 0h) -h C)) < (D / 2) /\ (normh` (C -h B)) < (D / 2)) -> (normh` (if(A e. H~, A, 0h) -h B)) < D) <-> (((normh` (if(A e. H~, A, 0h) -h C)) < (D / 2) /\ (normh` (C -h if(B e. H~, B, 0h))) < (D / 2)) -> (normh` (if(A e. H~, A, 0h) -h if(B e. H~, B, 0h))) < D)))
17		opreq2 3969	. . . . . 6 |- (C = if(C e. H~, C, 0h) -> (if(A e. H~, A, 0h) -h C) = (if(A e. H~, A, 0h) -h if(C e. H~, C, 0h)))
18	17	fveq2d 3728	. . . . 5 |- (C = if(C e. H~, C, 0h) -> (normh` (if(A e. H~, A, 0h) -h C)) = (normh` (if(A e. H~, A, 0h) -h if(C e. H~, C, 0h))))
19	18	breq1d 2629	. . . 4 |- (C = if(C e. H~, C, 0h) -> ((normh` (if(A e. H~, A, 0h) -h C)) < (D / 2) <-> (normh` (if(A e. H~, A, 0h) -h if(C e. H~, C, 0h))) < (D / 2)))
20		opreq1 3968	. . . . . 6 |- (C = if(C e. H~, C, 0h) -> (C -h if(B e. H~, B, 0h)) = (if(C e. H~, C, 0h) -h if(B e. H~, B, 0h)))
21	20	fveq2d 3728	. . . . 5 |- (C = if(C e. H~, C, 0h) -> (normh` (C -h if(B e. H~, B, 0h))) = (normh` (if(C e. H~, C, 0h) -h if(B e. H~, B, 0h))))
22	21	breq1d 2629	. . . 4 |- (C = if(C e. H~, C, 0h) -> ((normh` (C -h if(B e. H~, B, 0h))) < (D / 2) <-> (normh` (if(C e. H~, C, 0h) -h if(B e. H~, B, 0h))) < (D / 2)))
23	19, 22	anbi12d 628	. . 3 |- (C = if(C e. H~, C, 0h) -> (((normh` (if(A e. H~, A, 0h) -h C)) < (D / 2) /\ (normh` (C -h if(B e. H~, B, 0h))) < (D / 2)) <-> ((normh` (if(A e. H~, A, 0h) -h if(C e. H~, C, 0h))) < (D / 2) /\ (normh` (if(C e. H~, C, 0h) -h if(B e. H~, B, 0h))) < (D / 2))))
24	23	imbi1d 613	. 2 |- (C = if(C e. H~, C, 0h) -> ((((normh` (if(A e. H~, A, 0h) -h C)) < (D / 2) /\ (normh` (C -h if(B e. H~, B, 0h))) < (D / 2)) -> (normh` (if(A e. H~, A, 0h) -h if(B e. H~, B, 0h))) < D) <-> (((normh` (if(A e. H~, A, 0h) -h if(C e. H~, C, 0h))) < (D / 2) /\ (normh` (if(C e. H~, C, 0h) -h if(B e. H~, B, 0h))) < (D / 2)) -> (normh` (if(A e. H~, A, 0h) -h if(B e. H~, B, 0h))) < D)))
25		opreq1 3968	. . . . 5 |- (D = if(D e. RR, D, 2) -> (D / 2) = (if(D e. RR, D, 2) / 2))
26	25	breq2d 2630	. . . 4 |- (D = if(D e. RR, D, 2) -> ((normh` (if(A e. H~, A, 0h) -h if(C e. H~, C, 0h))) < (D / 2) <-> (normh` (if(A e. H~, A, 0h) -h if(C e. H~, C, 0h))) < (if(D e. RR, D, 2) / 2)))
27	25	breq2d 2630	. . . 4 |- (D = if(D e. RR, D, 2) -> ((normh` (if(C e. H~, C, 0h) -h if(B e. H~, B, 0h))) < (D / 2) <-> (normh` (if(C e. H~, C, 0h) -h if(B e. H~, B, 0h))) < (if(D e. RR, D, 2) / 2)))
28	26, 27	anbi12d 628	. . 3 |- (D = if(D e. RR, D, 2) -> (((normh` (if(A e. H~, A, 0h) -h if