Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-cnop Structured version   Visualization version   GIF version

Definition df-cnop 29039
 Description: Define the set of continuous operators on Hilbert space. For every "epsilon" (𝑦) there is a "delta" (𝑧) such that... (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-cnop ContOp = {𝑡 ∈ ( ℋ ↑𝑚 ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ((norm‘(𝑤 𝑥)) < 𝑧 → (norm‘((𝑡𝑤) − (𝑡𝑥))) < 𝑦)}
Distinct variable group:   𝑤,𝑡,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-cnop
StepHypRef Expression
1 ccop 28143 . 2 class ContOp
2 vw . . . . . . . . . . . 12 setvar 𝑤
32cv 1630 . . . . . . . . . . 11 class 𝑤
4 vx . . . . . . . . . . . 12 setvar 𝑥
54cv 1630 . . . . . . . . . . 11 class 𝑥
6 cmv 28122 . . . . . . . . . . 11 class
73, 5, 6co 6793 . . . . . . . . . 10 class (𝑤 𝑥)
8 cno 28120 . . . . . . . . . 10 class norm
97, 8cfv 6031 . . . . . . . . 9 class (norm‘(𝑤 𝑥))
10 vz . . . . . . . . . 10 setvar 𝑧
1110cv 1630 . . . . . . . . 9 class 𝑧
12 clt 10276 . . . . . . . . 9 class <
139, 11, 12wbr 4786 . . . . . . . 8 wff (norm‘(𝑤 𝑥)) < 𝑧
14 vt . . . . . . . . . . . . 13 setvar 𝑡
1514cv 1630 . . . . . . . . . . . 12 class 𝑡
163, 15cfv 6031 . . . . . . . . . . 11 class (𝑡𝑤)
175, 15cfv 6031 . . . . . . . . . . 11 class (𝑡𝑥)
1816, 17, 6co 6793 . . . . . . . . . 10 class ((𝑡𝑤) − (𝑡𝑥))
1918, 8cfv 6031 . . . . . . . . 9 class (norm‘((𝑡𝑤) − (𝑡𝑥)))
20 vy . . . . . . . . . 10 setvar 𝑦
2120cv 1630 . . . . . . . . 9 class 𝑦
2219, 21, 12wbr 4786 . . . . . . . 8 wff (norm‘((𝑡𝑤) − (𝑡𝑥))) < 𝑦
2313, 22wi 4 . . . . . . 7 wff ((norm‘(𝑤 𝑥)) < 𝑧 → (norm‘((𝑡𝑤) − (𝑡𝑥))) < 𝑦)
24 chil 28116 . . . . . . 7 class
2523, 2, 24wral 3061 . . . . . 6 wff 𝑤 ∈ ℋ ((norm‘(𝑤 𝑥)) < 𝑧 → (norm‘((𝑡𝑤) − (𝑡𝑥))) < 𝑦)
26 crp 12035 . . . . . 6 class +
2725, 10, 26wrex 3062 . . . . 5 wff 𝑧 ∈ ℝ+𝑤 ∈ ℋ ((norm‘(𝑤 𝑥)) < 𝑧 → (norm‘((𝑡𝑤) − (𝑡𝑥))) < 𝑦)
2827, 20, 26wral 3061 . . . 4 wff 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ((norm‘(𝑤 𝑥)) < 𝑧 → (norm‘((𝑡𝑤) − (𝑡𝑥))) < 𝑦)
2928, 4, 24wral 3061 . . 3 wff 𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ((norm‘(𝑤 𝑥)) < 𝑧 → (norm‘((𝑡𝑤) − (𝑡𝑥))) < 𝑦)
30 cmap 8009 . . . 4 class 𝑚
3124, 24, 30co 6793 . . 3 class ( ℋ ↑𝑚 ℋ)
3229, 14, 31crab 3065 . 2 class {𝑡 ∈ ( ℋ ↑𝑚 ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ((norm‘(𝑤 𝑥)) < 𝑧 → (norm‘((𝑡𝑤) − (𝑡𝑥))) < 𝑦)}
331, 32wceq 1631 1 wff ContOp = {𝑡 ∈ ( ℋ ↑𝑚 ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ((norm‘(𝑤 𝑥)) < 𝑧 → (norm‘((𝑡𝑤) − (𝑡𝑥))) < 𝑦)}
 Colors of variables: wff setvar class This definition is referenced by:  elcnop  29056  hhcno  29103
 Copyright terms: Public domain W3C validator