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

Definition df-nmfn 28088
Description: Define the norm of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-nmfn normfn = (𝑡 ∈ (ℂ ↑𝑚 ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡𝑧)))}, ℝ*, < ))
Distinct variable group:   𝑥,𝑡,𝑧

Detailed syntax breakdown of Definition df-nmfn
StepHypRef Expression
1 cnmf 27192 . 2 class normfn
2 vt . . 3 setvar 𝑡
3 cc 9813 . . . 4 class
4 chil 27160 . . . 4 class
5 cmap 7744 . . . 4 class 𝑚
63, 4, 5co 6549 . . 3 class (ℂ ↑𝑚 ℋ)
7 vz . . . . . . . . . 10 setvar 𝑧
87cv 1474 . . . . . . . . 9 class 𝑧
9 cno 27164 . . . . . . . . 9 class norm
108, 9cfv 5804 . . . . . . . 8 class (norm𝑧)
11 c1 9816 . . . . . . . 8 class 1
12 cle 9954 . . . . . . . 8 class
1310, 11, 12wbr 4583 . . . . . . 7 wff (norm𝑧) ≤ 1
14 vx . . . . . . . . 9 setvar 𝑥
1514cv 1474 . . . . . . . 8 class 𝑥
162cv 1474 . . . . . . . . . 10 class 𝑡
178, 16cfv 5804 . . . . . . . . 9 class (𝑡𝑧)
18 cabs 13822 . . . . . . . . 9 class abs
1917, 18cfv 5804 . . . . . . . 8 class (abs‘(𝑡𝑧))
2015, 19wceq 1475 . . . . . . 7 wff 𝑥 = (abs‘(𝑡𝑧))
2113, 20wa 383 . . . . . 6 wff ((norm𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡𝑧)))
2221, 7, 4wrex 2897 . . . . 5 wff 𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡𝑧)))
2322, 14cab 2596 . . . 4 class {𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡𝑧)))}
24 cxr 9952 . . . 4 class *
25 clt 9953 . . . 4 class <
2623, 24, 25csup 8229 . . 3 class sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡𝑧)))}, ℝ*, < )
272, 6, 26cmpt 4643 . 2 class (𝑡 ∈ (ℂ ↑𝑚 ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡𝑧)))}, ℝ*, < ))
281, 27wceq 1475 1 wff normfn = (𝑡 ∈ (ℂ ↑𝑚 ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((norm𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡𝑧)))}, ℝ*, < ))
Colors of variables: wff setvar class
This definition is referenced by:  nmfnval  28119
  Copyright terms: Public domain W3C validator