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 classContOp
1 vt setvart
2 chba classℋ
3 cmap class↑𝑚
4 2 2 3 co classℋℋ
5 vx setvarx
6 vy setvary
7 crp classℝ+
8 vz setvarz
9 vw setvarw
10 cno classnormℎ
11 9 cv setvarw
12 cmv class-ℎ
13 5 cv setvarx
14 11 13 12 co classw-ℎx
15 14 10 cfv classnormℎ⁡w-ℎx
16 clt class<
17 8 cv setvarz
18 15 17 16 wbr wffnormℎ⁡w-ℎx<z
19 1 cv setvart
20 11 19 cfv classt⁡w
21 13 19 cfv classt⁡x
22 20 21 12 co classt⁡w-ℎt⁡x
23 22 10 cfv classnormℎ⁡t⁡w-ℎt⁡x
24 6 cv setvary
25 23 24 16 wbr wffnormℎ⁡t⁡w-ℎt⁡x<y
26 18 25 wi wffnormℎ⁡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 classt∈ℋℋ|∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡t⁡w-ℎt⁡x<y
32 0 31 wceq wffContOp=t∈ℋℋ|∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→normℎ⁡t⁡w-ℎt⁡x<y