Metamath Proof Explorer

Definition df-cnfn

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.)

Ref Expression
Assertion df-cnfn ⊢ContFn=t∈ℂℋ|∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→t⁡w−t⁡x<y

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccnfn classContFn
1 vt setvart
2 cc classℂ
3 cmap class↑𝑚
4 chba classℋ
5 2 4 3 co classℂℋ
6 vx setvarx
7 vy setvary
8 crp classℝ+
9 vz setvarz
10 vw setvarw
11 cno classnormℎ
12 10 cv setvarw
13 cmv class-ℎ
14 6 cv setvarx
15 12 14 13 co classw-ℎx
16 15 11 cfv classnormℎ⁡w-ℎx
17 clt class<
18 9 cv setvarz
19 16 18 17 wbr wffnormℎ⁡w-ℎx<z
20 cabs classabs
21 1 cv setvart
22 12 21 cfv classt⁡w
23 cmin class−
24 14 21 cfv classt⁡x
25 22 24 23 co classt⁡w−t⁡x
26 25 20 cfv classt⁡w−t⁡x
27 7 cv setvary
28 26 27 17 wbr wfft⁡w−t⁡x<y
29 19 28 wi wffnormℎ⁡w-ℎx<z→t⁡w−t⁡x<y
30 29 10 4 wral wff∀w∈ℋnormℎ⁡w-ℎx<z→t⁡w−t⁡x<y
31 30 9 8 wrex wff∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→t⁡w−t⁡x<y
32 31 7 8 wral wff∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→t⁡w−t⁡x<y
33 32 6 4 wral wff∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→t⁡w−t⁡x<y
34 33 1 5 crab classt∈ℂℋ|∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→t⁡w−t⁡x<y
35 0 34 wceq wffContFn=t∈ℂℋ|∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→t⁡w−t⁡x<y