Definition df-nmop 28082

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

Step	Hyp	Ref	Expression
1		cnop 27186	. 2 class normop
2		vt	. . 3 setvar 𝑡
3		chil 27160	. . . 4 class ℋ
4		cmap 7744	. . . 4 class ↑𝑚
5	3, 3, 4	co 6549	. . 3 class ( ℋ ↑𝑚 ℋ)
6		vz	. . . . . . . . . 10 setvar 𝑧
7	6	cv 1474	. . . . . . . . 9 class 𝑧
8		cno 27164	. . . . . . . . 9 class normℎ
9	7, 8	cfv 5804	. . . . . . . 8 class (normℎ‘𝑧)
10		c1 9816	. . . . . . . 8 class 1
11		cle 9954	. . . . . . . 8 class ≤
12	9, 10, 11	wbr 4583	. . . . . . 7 wff (normℎ‘𝑧) ≤ 1
13		vx	. . . . . . . . 9 setvar 𝑥
14	13	cv 1474	. . . . . . . 8 class 𝑥
15	2	cv 1474	. . . . . . . . . 10 class 𝑡
16	7, 15	cfv 5804	. . . . . . . . 9 class (𝑡‘𝑧)
17	16, 8	cfv 5804	. . . . . . . 8 class (normℎ‘(𝑡‘𝑧))
18	14, 17	wceq 1475	. . . . . . 7 wff 𝑥 = (normℎ‘(𝑡‘𝑧))
19	12, 18	wa 383	. . . . . 6 wff ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑡‘𝑧)))
20	19, 6, 3	wrex 2897	. . . . 5 wff ∃𝑧 ∈ ℋ ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑡‘𝑧)))
21	20, 13	cab 2596	. . . 4 class {𝑥 ∣ ∃𝑧 ∈ ℋ ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑡‘𝑧)))}
22		cxr 9952	. . . 4 class ℝ*
23		clt 9953	. . . 4 class <
24	21, 22, 23	csup 8229	. . 3 class sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑡‘𝑧)))}, ℝ*, < )
25	2, 5, 24	cmpt 4643	. 2 class (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑡‘𝑧)))}, ℝ*, < ))
26	1, 25	wceq 1475	1 wff normop = (𝑡 ∈ ( ℋ ↑𝑚 ℋ) ↦ sup({𝑥 ∣ ∃𝑧 ∈ ℋ ((normℎ‘𝑧) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑡‘𝑧)))}, ℝ*, < ))

This definition is referenced by:  nmopval  28099  hhnmoi  28144