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

Definition df-nmop 29628
 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 28734 . 2 class normop
2 vt . . 3 setvar 𝑡
3 chba 28708 . . . 4 class
4 cmap 8402 . . . 4 class m
53, 3, 4co 7149 . . 3 class ( ℋ ↑m ℋ)
6 vz . . . . . . . . . 10 setvar 𝑧
76cv 1537 . . . . . . . . 9 class 𝑧
8 cno 28712 . . . . . . . . 9 class norm
97, 8cfv 6343 . . . . . . . 8 class (norm𝑧)
10 c1 10536 . . . . . . . 8 class 1
11 cle 10674 . . . . . . . 8 class
129, 10, 11wbr 5052 . . . . . . 7 wff (norm𝑧) ≤ 1
13 vx . . . . . . . . 9 setvar 𝑥
1413cv 1537 . . . . . . . 8 class 𝑥
152cv 1537 . . . . . . . . . 10 class 𝑡
167, 15cfv 6343 . . . . . . . . 9 class (𝑡𝑧)
1716, 8cfv 6343 . . . . . . . 8 class (norm‘(𝑡𝑧))
1814, 17wceq 1538 . . . . . . 7 wff 𝑥 = (norm‘(𝑡𝑧))
1912, 18wa 399 . . . . . 6 wff ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))
2019, 6, 3wrex 3134 . . . . 5 wff 𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))
2120, 13cab 2802 . . . 4 class {𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}
22 cxr 10672 . . . 4 class *
23 clt 10673 . . . 4 class <
2421, 22, 23csup 8901 . . 3 class sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}, ℝ*, < )
252, 5, 24cmpt 5132 . 2 class (𝑡 ∈ ( ℋ ↑m ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}, ℝ*, < ))
261, 25wceq 1538 1 wff normop = (𝑡 ∈ ( ℋ ↑m ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (norm‘(𝑡𝑧)))}, ℝ*, < ))
 Colors of variables: wff setvar class This definition is referenced by:  nmopval  29645  hhnmoi  29690
 Copyright terms: Public domain W3C validator