Definition df-cnfn 9690

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 8761	. 2 class ConFn
2		chil 8727	. . . . 5 class ℋ
3		cc 5204	. . . . 5 class ℂ
4		vt	. . . . . 6 set t
5	4	cv 952	. . . . 5 class t
6	2, 3, 5	wf 3168	. . . 4 wff t: ℋ –→ℂ
7		cc0 5206	. . . . . . . 8 class 0
8		vy	. . . . . . . . 9 set y
9	8	cv 952	. . . . . . . 8 class y
10		clt 5458	. . . . . . . 8 class <
11	7, 9, 10	wbr 2609	. . . . . . 7 wff 0 < y
12		vz	. . . . . . . . . . 11 set z
13	12	cv 952	. . . . . . . . . 10 class z
14	7, 13, 10	wbr 2609	. . . . . . . . 9 wff 0 < z
15		vw	. . . . . . . . . . . . . . 15 set w
16	15	cv 952	. . . . . . . . . . . . . 14 class w
17		vx	. . . . . . . . . . . . . . 15 set x
18	17	cv 952	. . . . . . . . . . . . . 14 class x
19		cmv 8731	. . . . . . . . . . . . . 14 class −h
20	16, 18, 19	co 3948	. . . . . . . . . . . . 13 class (w −h x)
21		cno 8733	. . . . . . . . . . . . 13 class normh
22	20, 21	cfv 3172	. . . . . . . . . . . 12 class (normh ‘(w −h x))
23	22, 13, 10	wbr 2609	. . . . . . . . . . 11 wff (normh ‘(w −h x)) < z
24	16, 5	cfv 3172	. . . . . . . . . . . . . 14 class (t ‘w)
25	18, 5	cfv 3172	. . . . . . . . . . . . . 14 class (t ‘x)
26		cmin 5264	. . . . . . . . . . . . . 14 class −
27	24, 25, 26	co 3948	. . . . . . . . . . . . 13 class ((t ‘w) − (t ‘x))
28		cabs 6681	. . . . . . . . . . . . 13 class abs
29	27, 28	cfv 3172	. . . . . . . . . . . 12 class (abs ‘((t ‘w) − (t ‘x)))
30	29, 9, 10	wbr 2609	. . . . . . . . . . 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 1637	. . . . . . . . 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 5205	. . . . . . . 8 class ℝ
35	33, 12, 34	wrex 1638	. . . . . . 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 1637	. . . . 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 1637	. . . 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 1456	. 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 953	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 9726

Copyright terms: Public domain