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

Definition df-nmop 29270
 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 28374 . 2 class normop
2 vt . . 3 setvar 𝑡
3 chba 28348 . . . 4 class
4 cmap 8140 . . . 4 class 𝑚
53, 3, 4co 6922 . . 3 class ( ℋ ↑𝑚 ℋ)
6 vz . . . . . . . . . 10 setvar 𝑧
76cv 1600 . . . . . . . . 9 class 𝑧
8 cno 28352 . . . . . . . . 9 class norm
97, 8cfv 6135 . . . . . . . 8 class (norm𝑧)
10 c1 10273 . . . . . . . 8 class 1
11 cle 10412 . . . . . . . 8 class
129, 10, 11wbr 4886 . . . . . . 7 wff (norm𝑧) ≤ 1
13 vx . . . . . . . . 9 setvar 𝑥
1413cv 1600 . . . . . . . 8 class 𝑥
152cv 1600 . . . . . . . . . 10 class 𝑡
167, 15cfv 6135 . . . . . . . . 9 class (𝑡𝑧)
1716, 8cfv 6135 . . . . . . . 8 class (norm‘(𝑡𝑧))
1814, 17wceq 1601 . . . . . . 7 wff 𝑥 = (norm‘(𝑡𝑧))
1912, 18wa 386 . . . . . 6 wff ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))
2019, 6, 3wrex 3091 . . . . 5 wff 𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))
2120, 13cab 2763 . . . 4 class {𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}
22 cxr 10410 . . . 4 class *
23 clt 10411 . . . 4 class <
2421, 22, 23csup 8634 . . 3 class sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}, ℝ*, < )
252, 5, 24cmpt 4965 . 2 class (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}, ℝ*, < ))
261, 25wceq 1601 1 wff normop = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}, ℝ*, < ))
 Colors of variables: wff setvar class This definition is referenced by:  nmopval  29287  hhnmoi  29332
 Copyright terms: Public domain W3C validator