Definition df-nmoo 27600

Description: Define the norm of an operator between two normed complex vector spaces. This definition produces an operator norm function for each pair of vector spaces ⟨𝑢, 𝑤⟩. Based on definition of linear operator norm in [AkhiezerGlazman] p. 39, although we define it for all operators for convenience. It isn't necessarily meaningful for nonlinear operators, since it doesn't take into account operator values at vectors with norm greater than 1. See Equation 2 of [Kreyszig] p. 92 for a definition that does (although it ignores the value at the zero vector). However, operator norms are rarely if ever used for nonlinear operators. (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.)

Assertion

Ref	Expression
df-nmoo	⊢ normOpOLD = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < )))

Distinct variable group:   𝑢,𝑡,𝑤,𝑥,𝑧

Detailed syntax breakdown of Definition df-nmoo

Step	Hyp	Ref	Expression
1		cnmoo 27596	. 2 class normOpOLD
2		vu	. . 3 setvar 𝑢
3		vw	. . 3 setvar 𝑤
4		cnv 27439	. . 3 class NrmCVec
5		vt	. . . 4 setvar 𝑡
6	3	cv 1482	. . . . . 6 class 𝑤
7		cba 27441	. . . . . 6 class BaseSet
8	6, 7	cfv 5888	. . . . 5 class (BaseSet‘𝑤)
9	2	cv 1482	. . . . . 6 class 𝑢
10	9, 7	cfv 5888	. . . . 5 class (BaseSet‘𝑢)
11		cmap 7857	. . . . 5 class ↑𝑚
12	8, 10, 11	co 6650	. . . 4 class ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢))
13		vz	. . . . . . . . . . 11 setvar 𝑧
14	13	cv 1482	. . . . . . . . . 10 class 𝑧
15		cnmcv 27445	. . . . . . . . . . 11 class normCV
16	9, 15	cfv 5888	. . . . . . . . . 10 class (normCV‘𝑢)
17	14, 16	cfv 5888	. . . . . . . . 9 class ((normCV‘𝑢)‘𝑧)
18		c1 9937	. . . . . . . . 9 class 1
19		cle 10075	. . . . . . . . 9 class ≤
20	17, 18, 19	wbr 4653	. . . . . . . 8 wff ((normCV‘𝑢)‘𝑧) ≤ 1
21		vx	. . . . . . . . . 10 setvar 𝑥
22	21	cv 1482	. . . . . . . . 9 class 𝑥
23	5	cv 1482	. . . . . . . . . . 11 class 𝑡
24	14, 23	cfv 5888	. . . . . . . . . 10 class (𝑡‘𝑧)
25	6, 15	cfv 5888	. . . . . . . . . 10 class (normCV‘𝑤)
26	24, 25	cfv 5888	. . . . . . . . 9 class ((normCV‘𝑤)‘(𝑡‘𝑧))
27	22, 26	wceq 1483	. . . . . . . 8 wff 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧))
28	20, 27	wa 384	. . . . . . 7 wff (((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))
29	28, 13, 10	wrex 2913	. . . . . 6 wff ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))
30	29, 21	cab 2608	. . . . 5 class {𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}
31		cxr 10073	. . . . 5 class ℝ*
32		clt 10074	. . . . 5 class <
33	30, 31, 32	csup 8346	. . . 4 class sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < )
34	5, 12, 33	cmpt 4729	. . 3 class (𝑡 ∈ ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < ))
35	2, 3, 4, 4, 34	cmpt2 6652	. 2 class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < )))
36	1, 35	wceq 1483	1 wff normOpOLD = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < )))

This definition is referenced by:  nmoofval  27617