Definition df-cnop 28083

Description: Define the set of continuous operators on Hilbert space. For every "epsilon" (𝑦) there is a "delta" (𝑧) such that... (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.)

Assertion

Ref	Expression
df-cnop	⊢ ConOp = {𝑡 ∈ ( ℋ ↑𝑚 ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦)}

Distinct variable group:   𝑤,𝑡,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-cnop

Step	Hyp	Ref	Expression
1		ccop 27187	. 2 class ConOp
2		vw	. . . . . . . . . . . 12 setvar 𝑤
3	2	cv 1474	. . . . . . . . . . 11 class 𝑤
4		vx	. . . . . . . . . . . 12 setvar 𝑥
5	4	cv 1474	. . . . . . . . . . 11 class 𝑥
6		cmv 27166	. . . . . . . . . . 11 class −ℎ
7	3, 5, 6	co 6549	. . . . . . . . . 10 class (𝑤 −ℎ 𝑥)
8		cno 27164	. . . . . . . . . 10 class normℎ
9	7, 8	cfv 5804	. . . . . . . . 9 class (normℎ‘(𝑤 −ℎ 𝑥))
10		vz	. . . . . . . . . 10 setvar 𝑧
11	10	cv 1474	. . . . . . . . 9 class 𝑧
12		clt 9953	. . . . . . . . 9 class <
13	9, 11, 12	wbr 4583	. . . . . . . 8 wff (normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧
14		vt	. . . . . . . . . . . . 13 setvar 𝑡
15	14	cv 1474	. . . . . . . . . . . 12 class 𝑡
16	3, 15	cfv 5804	. . . . . . . . . . 11 class (𝑡‘𝑤)
17	5, 15	cfv 5804	. . . . . . . . . . 11 class (𝑡‘𝑥)
18	16, 17, 6	co 6549	. . . . . . . . . 10 class ((𝑡‘𝑤) −ℎ (𝑡‘𝑥))
19	18, 8	cfv 5804	. . . . . . . . 9 class (normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥)))
20		vy	. . . . . . . . . 10 setvar 𝑦
21	20	cv 1474	. . . . . . . . 9 class 𝑦
22	19, 21, 12	wbr 4583	. . . . . . . 8 wff (normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦
23	13, 22	wi 4	. . . . . . 7 wff ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦)
24		chil 27160	. . . . . . 7 class ℋ
25	23, 2, 24	wral 2896	. . . . . 6 wff ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦)
26		crp 11708	. . . . . 6 class ℝ+
27	25, 10, 26	wrex 2897	. . . . 5 wff ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦)
28	27, 20, 26	wral 2896	. . . 4 wff ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦)
29	28, 4, 24	wral 2896	. . 3 wff ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦)
30		cmap 7744	. . . 4 class ↑𝑚
31	24, 24, 30	co 6549	. . 3 class ( ℋ ↑𝑚 ℋ)
32	29, 14, 31	crab 2900	. 2 class {𝑡 ∈ ( ℋ ↑𝑚 ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦)}
33	1, 32	wceq 1475	1 wff ConOp = {𝑡 ∈ ( ℋ ↑𝑚 ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (normℎ‘((𝑡‘𝑤) −ℎ (𝑡‘𝑥))) < 𝑦)}

This definition is referenced by:  elcnop  28100  hhcno  28147