Theorem cnopct 9837

Description: Basic continuity property of a continuous Hilbert space operator.

Assertion

Ref	Expression
cnopct	|- (((T e. ConOp /\ A e. H~) /\ (B e. RR /\ 0 < B)) -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < B)))

Distinct variable groups:   x,y,A   x,B,y   x,T,y

Proof of Theorem cnopct

Step	Hyp	Ref	Expression
1		elcnopt 9783	. . . 4 |- (T e. ConOp <-> (T:H~-->H~ /\ A.z e. H~ A.w e. RR (0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h z)) < x -> (normh` ((T` y) -h (T` z))) < w)))))
2	1	pm3.27bi 326	. . 3 |- (T e. ConOp -> A.z e. H~ A.w e. RR (0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h z)) < x -> (normh` ((T` y) -h (T` z))) < w))))
3		opreq2 3969	. . . . . . . . . . . . 13 |- (z = A -> (y -h z) = (y -h A))
4	3	fveq2d 3728	. . . . . . . . . . . 12 |- (z = A -> (normh` (y -h z)) = (normh` (y -h A)))
5	4	breq1d 2629	. . . . . . . . . . 11 |- (z = A -> ((normh` (y -h z)) < x <-> (normh` (y -h A)) < x))
6		fveq2 3724	. . . . . . . . . . . . . 14 |- (z = A -> (T` z) = (T` A))
7	6	opreq2d 3976	. . . . . . . . . . . . 13 |- (z = A -> ((T` y) -h (T` z)) = ((T` y) -h (T` A)))
8	7	fveq2d 3728	. . . . . . . . . . . 12 |- (z = A -> (normh` ((T` y) -h (T` z))) = (normh` ((T` y) -h (T` A))))
9	8	breq1d 2629	. . . . . . . . . . 11 |- (z = A -> ((normh` ((T` y) -h (T` z))) < w <-> (normh` ((T` y) -h (T` A))) < w))
10	5, 9	imbi12d 626	. . . . . . . . . 10 |- (z = A -> (((normh` (y -h z)) < x -> (normh` ((T` y) -h (T` z))) < w) <-> ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < w)))
11	10	ralbidv 1663	. . . . . . . . 9 |- (z = A -> (A.y e. H~ ((normh` (y -h z)) < x -> (normh` ((T` y) -h (T` z))) < w) <-> A.y e. H~ ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < w)))
12	11	anbi2d 616	. . . . . . . 8 |- (z = A -> ((0 < x /\ A.y e. H~ ((normh` (y -h z)) < x -> (normh` ((T` y) -h (T` z))) < w)) <-> (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < w))))
13	12	rexbidv 1664	. . . . . . 7 |- (z = A -> (E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h z)) < x -> (normh` ((T` y) -h (T` z))) < w)) <-> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < w))))
14	13	imbi2d 612	. . . . . 6 |- (z = A -> ((0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h z)) < x -> (normh` ((T` y) -h (T` z))) < w))) <-> (0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < w)))))
15	14	ralbidv 1663	. . . . 5 |- (z = A -> (A.w e. RR (0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h z)) < x -> (normh` ((T` y) -h (T` z))) < w))) <-> A.w e. RR (0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < w)))))
16	15	rcla4cv 1874	. . . 4 |- (A.z e. H~ A.w e. RR (0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h z)) < x -> (normh` ((T` y) -h (T` z))) < w))) -> (A e. H~ -> A.w e. RR (0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < w)))))
17		breq2 2623	. . . . . 6 |- (w = B -> (0 < w <-> 0 < B))
18		breq2 2623	. . . . . . . . . 10 |- (w = B -> ((normh` ((T` y) -h (T` A))) < w <-> (normh` ((T` y) -h (T` A))) < B))
19	18	imbi2d 612	. . . . . . . . 9 |- (w = B -> (((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < w) <-> ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < B)))
20	19	ralbidv 1663	. . . . . . . 8 |- (w = B -> (A.y e. H~ ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < w) <-> A.y e. H~ ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < B)))
21	20	anbi2d 616	. . . . . . 7 |- (w = B -> ((0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < w)) <-> (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < B))))
22	21	rexbidv 1664	. . . . . 6 |- (w = B -> (E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < w)) <-> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < B))))
23	17, 22	imbi12d 626	. . . . 5 |- (w = B -> ((0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < w))) <-> (0 < B -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < B)))))
24	23	rcla4cv 1874	. . . 4 |- (A.w e. RR (0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < w))) -> (B e. RR -> (0 < B -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < B)))))
25	16, 24	syl6 22	. . 3 |- (A.z e. H~ A.w e. RR (0 < w -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h z)) < x -> (normh` ((T` y) -h (T` z))) < w))) -> (A e. H~ -> (B e. RR -> (0 < B -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < B))))))
26	2, 25	syl 10	. 2 |- (T e. ConOp -> (A e. H~ -> (B e. RR -> (0 < B -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < B))))))
27	26	imp43 370	1 |- (((T e. ConOp /\ A e. H~) /\ (B e. RR /\ 0 < B)) -> E.x e. RR (0 < x /\ A.y e. H~ ((normh` (y -h A)) < x -> (normh` ((T` y) -h (T` A))) < B)))

Syntax hints:   -> wi 3   /\ wa 223   = wceq 956   e. wcel 958  A.wral 1645  E.wrex 1646   class class class wbr 2619  -->wf 3178  ` cfv 3182  (class class class)co 3963  RRcr 5233  0cc0 5234   < clt 5486  H~chil 8788   -h cmv 8792  normh