Definition df-cnfn 9773

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 8822	. 2 class ConFn
2		chil 8788	. . . . 5 class H~
3		cc 5232	. . . . 5 class CC
4		vt	. . . . . 6 set t
5	4	cv 955	. . . . 5 class t
6	2, 3, 5	wf 3178	. . . 4 wff t:H~-->CC
7		cc0 5234	. . . . . . . 8 class 0
8		vy	. . . . . . . . 9 set y
9	8	cv 955	. . . . . . . 8 class y
10		clt 5486	. . . . . . . 8 class <
11	7, 9, 10	wbr 2619	. . . . . . 7 wff 0 < y
12		vz	. . . . . . . . . . 11 set z
13	12	cv 955	. . . . . . . . . 10 class z
14	7, 13, 10	wbr 2619	. . . . . . . . 9 wff 0 < z
15		vw	. . . . . . . . . . . . . . 15 set w
16	15	cv 955	. . . . . . . . . . . . . 14 class w
17		vx	. . . . . . . . . . . . . . 15 set x
18	17	cv 955	. . . . . . . . . . . . . 14 class x
19		cmv 8792	. . . . . . . . . . . . . 14 class -h
20	16, 18, 19	co 3963	. . . . . . . . . . . . 13 class (w -h x)
21		cno 8794	. . . . . . . . . . . . 13 class normh
22	20, 21	cfv 3182	. . . . . . . . . . . 12 class (normh` (w -h x))
23	22, 13, 10	wbr 2619	. . . . . . . . . . 11 wff (normh` (w -h x)) < z
24	16, 5	cfv 3182	. . . . . . . . . . . . . 14 class (t` w)
25	18, 5	cfv 3182	. . . . . . . . . . . . . 14 class (t` x)
26		cmin 5292	. . . . . . . . . . . . . 14 class -
27	24, 25, 26	co 3963	. . . . . . . . . . . . 13 class ((t` w) - (t` x))
28		cabs 6750	. . . . . . . . . . . . 13 class abs
29	27, 28	cfv 3182	. . . . . . . . . . . 12 class (abs` ((t` w) - (t` x)))
30	29, 9, 10	wbr 2619	. . . . . . . . . . 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 1645	. . . . . . . . 9 wff A.w e. H~ ((normh` (w -h x)) < z -> (abs` ((t` w) - (t` x))) < y)
33	14, 32	wa 223	. . . . . . . 8 wff (0 < z /\ A.w e. H~ ((normh` (w -h x)) < z -> (abs` ((t` w) - (t` x))) < y))
34		cr 5233	. . . . . . . 8 class RR
35	33, 12, 34	wrex 1646	. . . . . . 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 1645	. . . . 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 1645	. . . 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 223	. . 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 1463	. 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 956	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:  elcnfnt 9809

Copyright terms: Public domain