Definition df-cnfn 11202

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:~H-->CC /\ A.x e. ~H A.y e. RR (0 < y -> E.z e. RR (0 < z /\ 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		ccnf 10246	. 2 class ConFn
2		chil 10212	. . . . 5 class ~H
3		cc 6180	. . . . 5 class CC
4		vt	. . . . . 6 set t
5	4	cv 1135	. . . . 5 class t
6	2, 3, 5	wf 3805	. . . 4 wff t:~H-->CC
7		cc0 6182	. . . . . . . 8 class 0
8		vy	. . . . . . . . 9 set y
9	8	cv 1135	. . . . . . . 8 class y
10		clt 6449	. . . . . . . 8 class <
11	7, 9, 10	wbr 3158	. . . . . . 7 wff 0 < y
12		vz	. . . . . . . . . . 11 set z
13	12	cv 1135	. . . . . . . . . 10 class z
14	7, 13, 10	wbr 3158	. . . . . . . . 9 wff 0 < z
15		vw	. . . . . . . . . . . . . . 15 set w
16	15	cv 1135	. . . . . . . . . . . . . 14 class w
17		vx	. . . . . . . . . . . . . . 15 set x
18	17	cv 1135	. . . . . . . . . . . . . 14 class x
19		cmv 10216	. . . . . . . . . . . . . 14 class -h
20	16, 18, 19	co 4695	. . . . . . . . . . . . 13 class (w -h x)
21		cno 10218	. . . . . . . . . . . . 13 class normh
22	20, 21	cfv 3809	. . . . . . . . . . . 12 class (normh` (w -h x))
23	22, 13, 10	wbr 3158	. . . . . . . . . . 11 wff (normh` (w -h x)) < z
24	16, 5	cfv 3809	. . . . . . . . . . . . . 14 class (t` w)
25	18, 5	cfv 3809	. . . . . . . . . . . . . 14 class (t` x)
26		cmin 6241	. . . . . . . . . . . . . 14 class -
27	24, 25, 26	co 4695	. . . . . . . . . . . . 13 class ((t` w) - (t` x))
28		cabs 7795	. . . . . . . . . . . . 13 class abs
29	27, 28	cfv 3809	. . . . . . . . . . . 12 class (abs` ((t` w) - (t` x)))
30	29, 9, 10	wbr 3158	. . . . . . . . . . 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 1939	. . . . . . . . 9 wff A.w e. ~H ((normh` (w -h x)) < z -> (abs` ((t` w) - (t` x))) < y)
33	14, 32	wa 239	. . . . . . . 8 wff (0 < z /\ A.w e. ~H ((normh` (w -h x)) < z -> (abs` ((t` w) - (t` x))) < y))
34		cr 6181	. . . . . . . 8 class RR
35	33, 12, 34	wrex 1940	. . . . . . 7 wff E.z e. RR (0 < z /\ A.w e. ~H ((normh` (w -h x)) < z -> (abs` ((t` w) - (t` x))) < y))
36	11, 35	wi 3	. . . . . 6 wff (0 < y -> E.z e. RR (0 < z /\ A.w e. ~H ((normh` (w -h x)) < z -> (abs` ((t` w) - (t` x))) < y)))
37	36, 8, 34	wral 1939	. . . . 5 wff A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. ~H ((normh` (w -h x)) < z -> (abs` ((t` w) - (t` x))) < y)))
38	37, 17, 2	wral 1939	. . . 4 wff A.x e. ~H A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. ~H ((normh` (w -h x)) < z -> (abs` ((t` w) - (t` x))) < y)))
39	6, 38	wa 239	. . 3 wff (t:~H-->CC /\ A.x e. ~H A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. ~H ((normh` (w -h x)) < z -> (abs` ((t` w) - (t` x))) < y))))
40	39, 4	cab 1708	. 2 class {t | (t:~H-->CC /\ A.x e. ~H A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. ~H ((normh` (w -h x)) < z -> (abs` ((t` w) - (t` x))) < y))))}
41	1, 40	wceq 1136	1 wff ConFn = {t | (t:~H-->CC /\ A.x e. ~H A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. ~H ((normh` (w -h x)) < z -> (abs` ((t` w) - (t` x))) < y))))}

This definition is referenced by:  elcnfn 11238

Copyright terms: Public domain