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 27870
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 26974 . 2 class normop
2 vt . . 3 setvar 𝑡
3 chil 26948 . . . 4 class
4 cmap 7620 . . . 4 class 𝑚
53, 3, 4co 6426 . . 3 class ( ℋ ↑𝑚 ℋ)
6 vz . . . . . . . . . 10 setvar 𝑧
76cv 1473 . . . . . . . . 9 class 𝑧
8 cno 26952 . . . . . . . . 9 class norm
97, 8cfv 5689 . . . . . . . 8 class (norm𝑧)
10 c1 9692 . . . . . . . 8 class 1
11 cle 9830 . . . . . . . 8 class
129, 10, 11wbr 4481 . . . . . . 7 wff (norm𝑧) ≤ 1
13 vx . . . . . . . . 9 setvar 𝑥
1413cv 1473 . . . . . . . 8 class 𝑥
152cv 1473 . . . . . . . . . 10 class 𝑡
167, 15cfv 5689 . . . . . . . . 9 class (𝑡𝑧)
1716, 8cfv 5689 . . . . . . . 8 class (norm‘(𝑡𝑧))
1814, 17wceq 1474 . . . . . . 7 wff 𝑥 = (norm‘(𝑡𝑧))
1912, 18wa 382 . . . . . 6 wff ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))
2019, 6, 3wrex 2801 . . . . 5 wff 𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))
2120, 13cab 2500 . . . 4 class {𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}
22 cxr 9828 . . . 4 class *
23 clt 9829 . . . 4 class <
2421, 22, 23csup 8105 . . 3 class sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}, ℝ*, < )
252, 5, 24cmpt 4541 . 2 class (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}, ℝ*, < ))
261, 25wceq 1474 1 wff normop = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}, ℝ*, < ))
Colors of variables: wff setvar class
This definition is referenced by:  nmopval  27887  hhnmoi  27932
  Copyright terms: Public domain W3C validator