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 class ContFn
1 vt setvar t
2 cc class ℂ
3 cmap class ↑ 𝑚
4 chba class ℋ
5 2 4 3 co class ℂ ℋ
6 vx setvar x
7 vy setvar y
8 crp class ℝ +
9 vz setvar z
10 vw setvar w
11 cno class norm ℎ
12 10 cv setvar w
13 cmv class - ℎ
14 6 cv setvar x
15 12 14 13 co class w - ℎ x
16 15 11 cfv class norm ℎ ⁡ w - ℎ x
17 clt class <
18 9 cv setvar z
19 16 18 17 wbr wff norm ℎ ⁡ w - ℎ x < z
20 cabs class abs
21 1 cv setvar t
22 12 21 cfv class t ⁡ w
23 cmin class −
24 14 21 cfv class t ⁡ x
25 22 24 23 co class t ⁡ w − t ⁡ x
26 25 20 cfv class t ⁡ w − t ⁡ x
27 7 cv setvar y
28 26 27 17 wbr wff t ⁡ w − t ⁡ x < y
29 19 28 wi wff norm ℎ ⁡ 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 class t ∈ ℂ ℋ | ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → t ⁡ w − t ⁡ x < y
35 0 34 wceq wff ContFn = t ∈ ℂ ℋ | ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → t ⁡ w − t ⁡ x < y