Definition df-cnop 10046

Description: Define the set of continuous operators on Hilbert space. For every "epsilon" (y) there is an "delta" (z) such that...

Assertion

Ref	Expression
df-cnop	|- ConOp = {t | (t:H~-->H~ /\ A.x e. H~ A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. H~ ((normh` (w -h x)) < z -> (normh` ((t` w) -h (t` x))) < y))))}

Distinct variable group:   w,t,x,y,z

Detailed syntax breakdown of Definition df-cnop

Step	Hyp	Ref	Expression
1		cco 9090	. 2 class ConOp
2		chil 9063	. . . . 5 class H~
3		vt	. . . . . 6 set t
4	3	cv 991	. . . . 5 class t
5	2, 2, 4	wf 3259	. . . 4 wff t:H~-->H~
6		cc0 5388	. . . . . . . 8 class 0
7		vy	. . . . . . . . 9 set y
8	7	cv 991	. . . . . . . 8 class y
9		clt 5640	. . . . . . . 8 class <
10	6, 8, 9	wbr 2692	. . . . . . 7 wff 0 < y
11		vz	. . . . . . . . . . 11 set z
12	11	cv 991	. . . . . . . . . 10 class z
13	6, 12, 9	wbr 2692	. . . . . . . . 9 wff 0 < z
14		vw	. . . . . . . . . . . . . . 15 set w
15	14	cv 991	. . . . . . . . . . . . . 14 class w
16		vx	. . . . . . . . . . . . . . 15 set x
17	16	cv 991	. . . . . . . . . . . . . 14 class x
18		cmv 9067	. . . . . . . . . . . . . 14 class -h
19	15, 17, 18	co 4021	. . . . . . . . . . . . 13 class (w -h x)
20		cno 9069	. . . . . . . . . . . . 13 class normh
21	19, 20	cfv 3263	. . . . . . . . . . . 12 class (normh` (w -h x))
22	21, 12, 9	wbr 2692	. . . . . . . . . . 11 wff (normh` (w -h x)) < z
23	15, 4	cfv 3263	. . . . . . . . . . . . . 14 class (t` w)
24	17, 4	cfv 3263	. . . . . . . . . . . . . 14 class (t` x)
25	23, 24, 18	co 4021	. . . . . . . . . . . . 13 class ((t` w) -h (t` x))
26	25, 20	cfv 3263	. . . . . . . . . . . 12 class (normh` ((t` w) -h (t` x)))
27	26, 8, 9	wbr 2692	. . . . . . . . . . 11 wff (normh` ((t` w) -h (t` x))) < y
28	22, 27	wi 3	. . . . . . . . . 10 wff ((normh` (w -h x)) < z -> (normh` ((t` w) -h (t` x))) < y)
29	28, 14, 2	wral 1691	. . . . . . . . 9 wff A.w e. H~ ((normh` (w -h x)) < z -> (normh` ((t` w) -h (t` x))) < y)
30	13, 29	wa 221	. . . . . . . 8 wff (0 < z /\ A.w e. H~ ((normh` (w -h x)) < z -> (normh` ((t` w) -h (t` x))) < y))
31		cr 5387	. . . . . . . 8 class RR
32	30, 11, 31	wrex 1692	. . . . . . 7 wff E.z e. RR (0 < z /\ A.w e. H~ ((normh` (w -h x)) < z -> (normh` ((t` w) -h (t` x))) < y))
33	10, 32	wi 3	. . . . . 6 wff (0 < y -> E.z e. RR (0 < z /\ A.w e. H~ ((normh` (w -h x)) < z -> (normh` ((t` w) -h (t` x))) < y)))
34	33, 7, 31	wral 1691	. . . . 5 wff A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. H~ ((normh` (w -h x)) < z -> (normh` ((t` w) -h (t` x))) < y)))
35	34, 16, 2	wral 1691	. . . 4 wff A.x e. H~ A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. H~ ((normh` (w -h x)) < z -> (normh` ((t` w) -h (t` x))) < y)))
36	5, 35	wa 221	. . 3 wff (t:H~-->H~ /\ A.x e. H~ A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. H~ ((normh` (w -h x)) < z -> (normh` ((t` w) -h (t` x))) < y))))
37	36, 3	cab 1505	. 2 class {t | (t:H~-->H~ /\ A.x e. H~ A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. H~ ((normh` (w -h x)) < z -> (normh` ((t` w) -h (t` x))) < y))))}
38	1, 37	wceq 992	1 wff ConOp = {t | (t:H~-->H~ /\ A.x e. H~ A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. H~ ((normh` (w -h x)) < z -> (normh` ((t` w) -h (t` x))) < y))))}

This definition is referenced by:  elcnop 10063

Copyright terms: Public domain