Definition df-cnop 11195

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 10239	. 2 class ConOp
2		chil 10212	. . . . 5 class ~H
3		vt	. . . . . 6 set t
4	3	cv 1135	. . . . 5 class t
5	2, 2, 4	wf 3805	. . . 4 wff t:~H-->~H
6		cc0 6182	. . . . . . . 8 class 0
7		vy	. . . . . . . . 9 set y
8	7	cv 1135	. . . . . . . 8 class y
9		clt 6449	. . . . . . . 8 class <
10	6, 8, 9	wbr 3158	. . . . . . 7 wff 0 < y
11		vz	. . . . . . . . . . 11 set z
12	11	cv 1135	. . . . . . . . . 10 class z
13	6, 12, 9	wbr 3158	. . . . . . . . 9 wff 0 < z
14		vw	. . . . . . . . . . . . . . 15 set w
15	14	cv 1135	. . . . . . . . . . . . . 14 class w
16		vx	. . . . . . . . . . . . . . 15 set x
17	16	cv 1135	. . . . . . . . . . . . . 14 class x
18		cmv 10216	. . . . . . . . . . . . . 14 class -h
19	15, 17, 18	co 4695	. . . . . . . . . . . . 13 class (w -h x)
20		cno 10218	. . . . . . . . . . . . 13 class normh
21	19, 20	cfv 3809	. . . . . . . . . . . 12 class (normh` (w -h x))
22	21, 12, 9	wbr 3158	. . . . . . . . . . 11 wff (normh` (w -h x)) < z
23	15, 4	cfv 3809	. . . . . . . . . . . . . 14 class (t` w)
24	17, 4	cfv 3809	. . . . . . . . . . . . . 14 class (t` x)
25	23, 24, 18	co 4695	. . . . . . . . . . . . 13 class ((t` w) -h (t` x))
26	25, 20	cfv 3809	. . . . . . . . . . . 12 class (normh` ((t` w) -h (t` x)))
27	26, 8, 9	wbr 3158	. . . . . . . . . . 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 1939	. . . . . . . . 9 wff A.w e. ~H ((normh` (w -h x)) < z -> (normh` ((t` w) -h (t` x))) < y)
30	13, 29	wa 239	. . . . . . . 8 wff (0 < z /\ A.w e. ~H ((normh` (w -h x)) < z -> (normh` ((t` w) -h (t` x))) < y))
31		cr 6181	. . . . . . . 8 class RR
32	30, 11, 31	wrex 1940	. . . . . . 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 1939	. . . . 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 1939	. . . 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 239	. . 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 1708	. 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 1136	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 11212

Copyright terms: Public domain