Metamath Proof Explorer

Definition df-cnop

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccop class ContOp
1 vt setvar t
2 chba class ℋ
3 cmap class ↑ 𝑚
4 2 2 3 co class ℋ ℋ
5 vx setvar x
6 vy setvar y
7 crp class ℝ +
8 vz setvar z
9 vw setvar w
10 cno class norm ℎ
11 9 cv setvar w
12 cmv class - ℎ
13 5 cv setvar x
14 11 13 12 co class w - ℎ x
15 14 10 cfv class norm ℎ ⁡ w - ℎ x
16 clt class <
17 8 cv setvar z
18 15 17 16 wbr wff norm ℎ ⁡ w - ℎ x < z
19 1 cv setvar t
20 11 19 cfv class t ⁡ w
21 13 19 cfv class t ⁡ x
22 20 21 12 co class t ⁡ w - ℎ t ⁡ x
23 22 10 cfv class norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x
24 6 cv setvar y
25 23 24 16 wbr wff norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y
26 18 25 wi wff norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y
27 26 9 2 wral wff ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y
28 27 8 7 wrex wff ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y
29 28 6 7 wral wff ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y
30 29 5 2 wral wff ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y
31 30 1 4 crab class t ∈ ℋ ℋ | ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y
32 0 31 wceq wff ContOp = t ∈ ℋ ℋ | ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y