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

Definition df-nmop 28826
 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 = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}, ℝ*, < ))
Distinct variable group:   𝑥,𝑡,𝑧

Detailed syntax breakdown of Definition df-nmop
StepHypRef Expression
1 cnop 27930 . 2 class normop
2 vt . . 3 setvar 𝑡
3 chil 27904 . . . 4 class
4 cmap 7899 . . . 4 class 𝑚
53, 3, 4co 6690 . . 3 class ( ℋ ↑𝑚 ℋ)
6 vz . . . . . . . . . 10 setvar 𝑧
76cv 1522 . . . . . . . . 9 class 𝑧
8 cno 27908 . . . . . . . . 9 class norm
97, 8cfv 5926 . . . . . . . 8 class (norm𝑧)
10 c1 9975 . . . . . . . 8 class 1
11 cle 10113 . . . . . . . 8 class
129, 10, 11wbr 4685 . . . . . . 7 wff (norm𝑧) ≤ 1
13 vx . . . . . . . . 9 setvar 𝑥
1413cv 1522 . . . . . . . 8 class 𝑥
152cv 1522 . . . . . . . . . 10 class 𝑡
167, 15cfv 5926 . . . . . . . . 9 class (𝑡𝑧)
1716, 8cfv 5926 . . . . . . . 8 class (norm‘(𝑡𝑧))
1814, 17wceq 1523 . . . . . . 7 wff 𝑥 = (norm‘(𝑡𝑧))
1912, 18wa 383 . . . . . 6 wff ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))
2019, 6, 3wrex 2942 . . . . 5 wff 𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))
2120, 13cab 2637 . . . 4 class {𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}
22 cxr 10111 . . . 4 class *
23 clt 10112 . . . 4 class <
2421, 22, 23csup 8387 . . 3 class sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}, ℝ*, < )
252, 5, 24cmpt 4762 . 2 class (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}, ℝ*, < ))
261, 25wceq 1523 1 wff normop = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}, ℝ*, < ))
 Colors of variables: wff setvar class This definition is referenced by:  nmopval  28843  hhnmoi  28888
 Copyright terms: Public domain W3C validator