Definition df-nmfn 29293

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

Step	Hyp	Ref	Expression
1		cnmf 28397	. 2 class normfn
2		vt	. . 3 setvar 𝑡
3		cc 10272	. . . 4 class ℂ
4		chba 28365	. . . 4 class ℋ
5		cmap 8142	. . . 4 class ↑𝑚
6	3, 4, 5	co 6924	. . 3 class (ℂ ↑𝑚 ℋ)
7		vz	. . . . . . . . . 10 setvar 𝑧
8	7	cv 1600	. . . . . . . . 9 class 𝑧
9		cno 28369	. . . . . . . . 9 class normℎ
10	8, 9	cfv 6137	. . . . . . . 8 class (normℎ‘𝑧)
11		c1 10275	. . . . . . . 8 class 1
12		cle 10414	. . . . . . . 8 class ≤
13	10, 11, 12	wbr 4888	. . . . . . 7 wff (normℎ‘𝑧) ≤ 1
14		vx	. . . . . . . . 9 setvar 𝑥
15	14	cv 1600	. . . . . . . 8 class 𝑥
16	2	cv 1600	. . . . . . . . . 10 class 𝑡
17	8, 16	cfv 6137	. . . . . . . . 9 class (𝑡‘𝑧)
18		cabs 14387	. . . . . . . . 9 class abs
19	17, 18	cfv 6137	. . . . . . . 8 class (abs‘(𝑡‘𝑧))
20	15, 19	wceq 1601	. . . . . . 7 wff 𝑥 = (abs‘(𝑡‘𝑧))
21	13, 20	wa 386	. . . . . 6 wff ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡‘𝑧)))
22	21, 7, 4	wrex 3091	. . . . 5 wff ∃𝑧 ∈ ℋ ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡‘𝑧)))
23	22, 14	cab 2763	. . . 4 class {𝑥 ∣ ∃𝑧 ∈ ℋ ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡‘𝑧)))}
24		cxr 10412	. . . 4 class ℝ*
25		clt 10413	. . . 4 class <
26	23, 24, 25	csup 8636	. . 3 class sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡‘𝑧)))}, ℝ*, < )
27	2, 6, 26	cmpt 4967	. 2 class (𝑡 ∈ (ℂ ↑𝑚 ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡‘𝑧)))}, ℝ*, < ))
28	1, 27	wceq 1601	1 wff normfn = (𝑡 ∈ (ℂ ↑𝑚 ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (abs‘(𝑡‘𝑧)))}, ℝ*, < ))

This definition is referenced by:  nmfnval  29324