Definition df-cnop 9706

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: ℋ –→ ℋ ⋀ ∀x ∈ ℋ ∀y ∈ ℝ (0 < y → ∃z ∈ ℝ (0 < z ⋀ ∀w ∈ ℋ ((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 8754	. 2 class ConOp
2		chil 8727	. . . . 5 class ℋ
3		vt	. . . . . 6 set t
4	3	cv 953	. . . . 5 class t
5	2, 2, 4	wf 3173	. . . 4 wff t: ℋ –→ ℋ
6		cc0 5214	. . . . . . . 8 class 0
7		vy	. . . . . . . . 9 set y
8	7	cv 953	. . . . . . . 8 class y
9		clt 5466	. . . . . . . 8 class <
10	6, 8, 9	wbr 2614	. . . . . . 7 wff 0 < y
11		vz	. . . . . . . . . . 11 set z
12	11	cv 953	. . . . . . . . . 10 class z
13	6, 12, 9	wbr 2614	. . . . . . . . 9 wff 0 < z
14		vw	. . . . . . . . . . . . . . 15 set w
15	14	cv 953	. . . . . . . . . . . . . 14 class w
16		vx	. . . . . . . . . . . . . . 15 set x
17	16	cv 953	. . . . . . . . . . . . . 14 class x
18		cmv 8731	. . . . . . . . . . . . . 14 class −h
19	15, 17, 18	co 3954	. . . . . . . . . . . . 13 class (w −h x)
20		cno 8733	. . . . . . . . . . . . 13 class normh
21	19, 20	cfv 3177	. . . . . . . . . . . 12 class (normh ‘(w −h x))
22	21, 12, 9	wbr 2614	. . . . . . . . . . 11 wff (normh ‘(w −h x)) < z
23	15, 4	cfv 3177	. . . . . . . . . . . . . 14 class (t ‘w)
24	17, 4	cfv 3177	. . . . . . . . . . . . . 14 class (t ‘x)
25	23, 24, 18	co 3954	. . . . . . . . . . . . 13 class ((t ‘w) −h (t ‘x))
26	25, 20	cfv 3177	. . . . . . . . . . . 12 class (normh ‘((t ‘w) −h (t ‘x)))
27	26, 8, 9	wbr 2614	. . . . . . . . . . 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 1642	. . . . . . . . 9 wff ∀w ∈ ℋ ((normh ‘(w −h x)) < z → (normh ‘((t ‘w) −h (t ‘x))) < y)
30	13, 29	wa 223	. . . . . . . 8 wff (0 < z ⋀ ∀w ∈ ℋ ((normh ‘(w −h x)) < z → (normh ‘((t ‘w) −h (t ‘x))) < y))
31		cr 5213	. . . . . . . 8 class ℝ
32	30, 11, 31	wrex 1643	. . . . . . 7 wff ∃z ∈ ℝ (0 < z ⋀ ∀w ∈ ℋ ((normh ‘(w −h x)) < z → (normh ‘((t ‘w) −h (t ‘x))) < y))
33	10, 32	wi 3	. . . . . 6 wff (0 < y → ∃z ∈ ℝ (0 < z ⋀ ∀w ∈ ℋ ((normh ‘(w −h x)) < z → (normh ‘((t ‘w) −h (t ‘x))) < y)))
34	33, 7, 31	wral 1642	. . . . 5 wff ∀y ∈ ℝ (0 < y → ∃z ∈ ℝ (0 < z ⋀ ∀w ∈ ℋ ((normh ‘(w −h x)) < z → (normh ‘((t ‘w) −h (t ‘x))) < y)))
35	34, 16, 2	wral 1642	. . . 4 wff ∀x ∈ ℋ ∀y ∈ ℝ (0 < y → ∃z ∈ ℝ (0 < z ⋀ ∀w ∈ ℋ ((normh ‘(w −h x)) < z → (normh ‘((t ‘w) −h (t ‘x))) < y)))
36	5, 35	wa 223	. . 3 wff (t: ℋ –→ ℋ ⋀ ∀x ∈ ℋ ∀y ∈ ℝ (0 < y → ∃z ∈ ℝ (0 < z ⋀ ∀w ∈ ℋ ((normh ‘(w −h x)) < z → (normh ‘((t ‘w) −h (t ‘x))) < y))))
37	36, 3	cab 1461	. 2 class {t∣(t: ℋ –→ ℋ ⋀ ∀x ∈ ℋ ∀y ∈ ℝ (0 < y → ∃z ∈ ℝ (0 < z ⋀ ∀w ∈ ℋ ((normh ‘(w −h x)) < z → (normh ‘((t ‘w) −h (t ‘x))) < y))))}
38	1, 37	wceq 954	1 wff ConOp = {t∣(t: ℋ –→ ℋ ⋀ ∀x ∈ ℋ ∀y ∈ ℝ (0 < y → ∃z ∈ ℝ (0 < z ⋀ ∀w ∈ ℋ ((normh ‘(w −h x)) < z → (normh ‘((t ‘w) −h (t ‘x))) < y))))}

This definition is referenced by:  elcnopt 9723

Copyright terms: Public domain