Definition df-cnfn 32442

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

Assertion

Ref	Expression
df-cnfn	⊢ ContFn = {𝑡 ∈ (ℂ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (abs‘((𝑡‘𝑤) − (𝑡‘𝑥))) < 𝑦)}

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

Detailed syntax breakdown of Definition df-cnfn

Step	Hyp	Ref	Expression
1		ccnfn 31548	. 2 class ContFn
2		vw	. . . . . . . . . . . 12 setvar 𝑤
3	2	cv 1569	. . . . . . . . . . 11 class 𝑤
4		vx	. . . . . . . . . . . 12 setvar 𝑥
5	4	cv 1569	. . . . . . . . . . 11 class 𝑥
6		cmv 31520	. . . . . . . . . . 11 class −ℎ
7	3, 5, 6	co 7418	. . . . . . . . . 10 class (𝑤 −ℎ 𝑥)
8		cno 31518	. . . . . . . . . 10 class normℎ
9	7, 8	cfv 6537	. . . . . . . . 9 class (normℎ‘(𝑤 −ℎ 𝑥))
10		vz	. . . . . . . . . 10 setvar 𝑧
11	10	cv 1569	. . . . . . . . 9 class 𝑧
12		clt 11336	. . . . . . . . 9 class <
13	9, 11, 12	wbr 5103	. . . . . . . 8 wff (normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧
14		vt	. . . . . . . . . . . . 13 setvar 𝑡
15	14	cv 1569	. . . . . . . . . . . 12 class 𝑡
16	3, 15	cfv 6537	. . . . . . . . . . 11 class (𝑡‘𝑤)
17	5, 15	cfv 6537	. . . . . . . . . . 11 class (𝑡‘𝑥)
18		cmin 11534	. . . . . . . . . . 11 class −
19	16, 17, 18	co 7418	. . . . . . . . . 10 class ((𝑡‘𝑤) − (𝑡‘𝑥))
20		cabs 15394	. . . . . . . . . 10 class abs
21	19, 20	cfv 6537	. . . . . . . . 9 class (abs‘((𝑡‘𝑤) − (𝑡‘𝑥)))
22		vy	. . . . . . . . . 10 setvar 𝑦
23	22	cv 1569	. . . . . . . . 9 class 𝑦
24	21, 23, 12	wbr 5103	. . . . . . . 8 wff (abs‘((𝑡‘𝑤) − (𝑡‘𝑥))) < 𝑦
25	13, 24	wi 4	. . . . . . 7 wff ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (abs‘((𝑡‘𝑤) − (𝑡‘𝑥))) < 𝑦)
26		chba 31514	. . . . . . 7 class ℋ
27	25, 2, 26	wral 3077	. . . . . 6 wff ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (abs‘((𝑡‘𝑤) − (𝑡‘𝑥))) < 𝑦)
28		crp 13113	. . . . . 6 class ℝ+
29	27, 10, 28	wrex 3087	. . . . 5 wff ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (abs‘((𝑡‘𝑤) − (𝑡‘𝑥))) < 𝑦)
30	29, 22, 28	wral 3077	. . . 4 wff ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (abs‘((𝑡‘𝑤) − (𝑡‘𝑥))) < 𝑦)
31	30, 4, 26	wral 3077	. . 3 wff ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (abs‘((𝑡‘𝑤) − (𝑡‘𝑥))) < 𝑦)
32		cc 11191	. . . 4 class ℂ
33		cmap 8840	. . . 4 class ↑m
34	32, 26, 33	co 7418	. . 3 class (ℂ ↑m ℋ)
35	31, 14, 34	crab 3413	. 2 class {𝑡 ∈ (ℂ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (abs‘((𝑡‘𝑤) − (𝑡‘𝑥))) < 𝑦)}
36	1, 35	wceq 1570	1 wff ContFn = {𝑡 ∈ (ℂ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ ℋ ((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑧 → (abs‘((𝑡‘𝑤) − (𝑡‘𝑥))) < 𝑦)}

This definition is used by:  elcnfn  32477  hhcnf  32500