Definition df-cnfn 28706

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

Assertion

Ref	Expression
df-cnfn	|- ContFn = { t e. ( CC ^m ~H ) | A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( 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		ccnfn 27810	. 2 class ContFn
2		vw	. . . . . . . . . . . 12 setvar w
3	2	cv 1482	. . . . . . . . . . 11 class w
4		vx	. . . . . . . . . . . 12 setvar x
5	4	cv 1482	. . . . . . . . . . 11 class x
6		cmv 27782	. . . . . . . . . . 11 class -h
7	3, 5, 6	co 6650	. . . . . . . . . 10 class ( w -h x )
8		cno 27780	. . . . . . . . . 10 class normh
9	7, 8	cfv 5888	. . . . . . . . 9 class ( normh ` ( w -h x ) )
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1482	. . . . . . . . 9 class z
12		clt 10074	. . . . . . . . 9 class <
13	9, 11, 12	wbr 4653	. . . . . . . 8 wff ( normh ` ( w -h x ) ) < z
14		vt	. . . . . . . . . . . . 13 setvar t
15	14	cv 1482	. . . . . . . . . . . 12 class t
16	3, 15	cfv 5888	. . . . . . . . . . 11 class ( t ` w )
17	5, 15	cfv 5888	. . . . . . . . . . 11 class ( t ` x )
18		cmin 10266	. . . . . . . . . . 11 class -
19	16, 17, 18	co 6650	. . . . . . . . . 10 class ( ( t ` w ) - ( t ` x ) )
20		cabs 13974	. . . . . . . . . 10 class abs
21	19, 20	cfv 5888	. . . . . . . . 9 class ( abs ` ( ( t ` w ) - ( t ` x ) ) )
22		vy	. . . . . . . . . 10 setvar y
23	22	cv 1482	. . . . . . . . 9 class y
24	21, 23, 12	wbr 4653	. . . . . . . 8 wff ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y
25	13, 24	wi 4	. . . . . . 7 wff ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y )
26		chil 27776	. . . . . . 7 class ~H
27	25, 2, 26	wral 2912	. . . . . 6 wff A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y )
28		crp 11832	. . . . . 6 class RR+
29	27, 10, 28	wrex 2913	. . . . 5 wff E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y )
30	29, 22, 28	wral 2912	. . . 4 wff A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y )
31	30, 4, 26	wral 2912	. . 3 wff A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y )
32		cc 9934	. . . 4 class CC
33		cmap 7857	. . . 4 class ^m
34	32, 26, 33	co 6650	. . 3 class ( CC ^m ~H )
35	31, 14, 34	crab 2916	. 2 class { t e. ( CC ^m ~H ) | A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) }
36	1, 35	wceq 1483	1 wff ContFn = { t e. ( CC ^m ~H ) | A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) }

This definition is referenced by:  elcnfn  28741  hhcnf  28764