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

Definition df-nmop 31087
Description: Define the norm of a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-nmop normop = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}, ℝ*, < ))
Distinct variable group:   𝑥,𝑡,𝑧

Detailed syntax breakdown of Definition df-nmop
StepHypRef Expression
1 cnop 30193 . 2 class normop
2 vt . . 3 setvar 𝑡
3 chba 30167 . . . 4 class
4 cmap 8819 . . . 4 class m
53, 3, 4co 7408 . . 3 class ( ℋ ↑m ℋ)
6 vz . . . . . . . . . 10 setvar 𝑧
76cv 1540 . . . . . . . . 9 class 𝑧
8 cno 30171 . . . . . . . . 9 class norm
97, 8cfv 6543 . . . . . . . 8 class (norm𝑧)
10 c1 11110 . . . . . . . 8 class 1
11 cle 11248 . . . . . . . 8 class
129, 10, 11wbr 5148 . . . . . . 7 wff (norm𝑧) ≤ 1
13 vx . . . . . . . . 9 setvar 𝑥
1413cv 1540 . . . . . . . 8 class 𝑥
152cv 1540 . . . . . . . . . 10 class 𝑡
167, 15cfv 6543 . . . . . . . . 9 class (𝑡𝑧)
1716, 8cfv 6543 . . . . . . . 8 class (norm‘(𝑡𝑧))
1814, 17wceq 1541 . . . . . . 7 wff 𝑥 = (norm‘(𝑡𝑧))
1912, 18wa 396 . . . . . 6 wff ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))
2019, 6, 3wrex 3070 . . . . 5 wff 𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))
2120, 13cab 2709 . . . 4 class {𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}
22 cxr 11246 . . . 4 class *
23 clt 11247 . . . 4 class <
2421, 22, 23csup 9434 . . 3 class sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}, ℝ*, < )
252, 5, 24cmpt 5231 . 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}, ℝ*, < ))
261, 25wceq 1541 1 wff normop = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}, ℝ*, < ))
Colors of variables: wff setvar class
This definition is referenced by:  nmopval  31104  hhnmoi  31149
  Copyright terms: Public domain W3C validator