Definition df-cnfn 9730

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

Assertion

Ref	Expression
df-cnfn	⊢ ConFn = {t∣(t: ℋ –→ℂ ⋀ ∀x ∈ ℋ ∀y ∈ ℝ (0 < y → ∃z ∈ ℝ (0 < z ⋀ ∀w ∈ ℋ ((normh ‘(w −h x)) < z → (abs ‘((t ‘w) − (t ‘x))) < y))))}

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

Detailed syntax breakdown of Definition df-cnfn

Step	Hyp	Ref	Expression
1		ccnf 8777	. 2 class ConFn
2		chil 8743	. . . . 5 class ℋ
3		cc 5215	. . . . 5 class ℂ
4		vt	. . . . . 6 set t
5	4	cv 954	. . . . 5 class t
6	2, 3, 5	wf 3174	. . . 4 wff t: ℋ –→ℂ
7		cc0 5217	. . . . . . . 8 class 0
8		vy	. . . . . . . . 9 set y
9	8	cv 954	. . . . . . . 8 class y
10		clt 5469	. . . . . . . 8 class <
11	7, 9, 10	wbr 2615	. . . . . . 7 wff 0 < y
12		vz	. . . . . . . . . . 11 set z
13	12	cv 954	. . . . . . . . . 10 class z
14	7, 13, 10	wbr 2615	. . . . . . . . 9 wff 0 < z
15		vw	. . . . . . . . . . . . . . 15 set w
16	15	cv 954	. . . . . . . . . . . . . 14 class w
17		vx	. . . . . . . . . . . . . . 15 set x
18	17	cv 954	. . . . . . . . . . . . . 14 class x
19		cmv 8747	. . . . . . . . . . . . . 14 class −h
20	16, 18, 19	co 3958	. . . . . . . . . . . . 13 class (w −h x)
21		cno 8749	. . . . . . . . . . . . 13 class normh
22	20, 21	cfv 3178	. . . . . . . . . . . 12 class (normh ‘(w −h x))
23	22, 13, 10	wbr 2615	. . . . . . . . . . 11 wff (normh ‘(w −h x)) < z
24	16, 5	cfv 3178	. . . . . . . . . . . . . 14 class (t ‘w)
25	18, 5	cfv 3178	. . . . . . . . . . . . . 14 class (t ‘x)
26		cmin 5275	. . . . . . . . . . . . . 14 class −
27	24, 25, 26	co 3958	. . . . . . . . . . . . 13 class ((t ‘w) − (t ‘x))
28		cabs 6696	. . . . . . . . . . . . 13 class abs
29	27, 28	cfv 3178	. . . . . . . . . . . 12 class (abs ‘((t ‘w) − (t ‘x)))
30	29, 9, 10	wbr 2615	. . . . . . . . . . 11 wff (abs ‘((t ‘w) − (t ‘x))) < y
31	23, 30	wi 3	. . . . . . . . . 10 wff ((normh ‘(w −h x)) < z → (abs ‘((t ‘w) − (t ‘x))) < y)
32	31, 15, 2	wral 1643	. . . . . . . . 9 wff ∀w ∈ ℋ ((normh ‘(w −h x)) < z → (abs ‘((t ‘w) − (t ‘x))) < y)
33	14, 32	wa 223	. . . . . . . 8 wff (0 < z ⋀ ∀w ∈ ℋ ((normh ‘(w −h x)) < z → (abs ‘((t ‘w) − (t ‘x))) < y))
34		cr 5216	. . . . . . . 8 class ℝ
35	33, 12, 34	wrex 1644	. . . . . . 7 wff ∃z ∈ ℝ (0 < z ⋀ ∀w ∈ ℋ ((normh ‘(w −h x)) < z → (abs ‘((t ‘w) − (t ‘x))) < y))
36	11, 35	wi 3	. . . . . 6 wff (0 < y → ∃z ∈ ℝ (0 < z ⋀ ∀w ∈ ℋ ((normh ‘(w −h x)) < z → (abs ‘((t ‘w) − (t ‘x))) < y)))
37	36, 8, 34	wral 1643	. . . . 5 wff ∀y ∈ ℝ (0 < y → ∃z ∈ ℝ (0 < z ⋀ ∀w ∈ ℋ ((normh ‘(w −h x)) < z → (abs ‘((t ‘w) − (t ‘x))) < y)))
38	37, 17, 2	wral 1643	. . . 4 wff ∀x ∈ ℋ ∀y ∈ ℝ (0 < y → ∃z ∈ ℝ (0 < z ⋀ ∀w ∈ ℋ ((normh ‘(w −h x)) < z → (abs ‘((t ‘w) − (t ‘x))) < y)))
39	6, 38	wa 223	. . 3 wff (t: ℋ –→ℂ ⋀ ∀x ∈ ℋ ∀y ∈ ℝ (0 < y → ∃z ∈ ℝ (0 < z ⋀ ∀w ∈ ℋ ((normh ‘(w −h x)) < z → (abs ‘((t ‘w) − (t ‘x))) < y))))
40	39, 4	cab 1462	. 2 class {t∣(t: ℋ –→ℂ ⋀ ∀x ∈ ℋ ∀y ∈ ℝ (0 < y → ∃z ∈ ℝ (0 < z ⋀ ∀w ∈ ℋ ((normh ‘(w −h x)) < z → (abs ‘((t ‘w) − (t ‘x))) < y))))}
41	1, 40	wceq 955	1 wff ConFn = {t∣(t: ℋ –→ℂ ⋀ ∀x ∈ ℋ ∀y ∈ ℝ (0 < y → ∃z ∈ ℝ (0 < z ⋀ ∀w ∈ ℋ ((normh ‘(w −h x)) < z → (abs ‘((t ‘w) − (t ‘x))) < y))))}

This definition is referenced by:  elcnfnt 9766

Copyright terms: Public domain