Definition df-nmoo 30774

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‘𝑤) ↑m (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < )))

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

Detailed syntax breakdown of Definition df-nmoo

Step	Hyp	Ref	Expression
1		cnmoo 30770	. 2 class normOpOLD
2		vu	. . 3 setvar 𝑢
3		vw	. . 3 setvar 𝑤
4		cnv 30613	. . 3 class NrmCVec
5		vt	. . . 4 setvar 𝑡
6	3	cv 1536	. . . . . 6 class 𝑤
7		cba 30615	. . . . . 6 class BaseSet
8	6, 7	cfv 6563	. . . . 5 class (BaseSet‘𝑤)
9	2	cv 1536	. . . . . 6 class 𝑢
10	9, 7	cfv 6563	. . . . 5 class (BaseSet‘𝑢)
11		cmap 8865	. . . . 5 class ↑m
12	8, 10, 11	co 7431	. . . 4 class ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢))
13		vz	. . . . . . . . . . 11 setvar 𝑧
14	13	cv 1536	. . . . . . . . . 10 class 𝑧
15		cnmcv 30619	. . . . . . . . . . 11 class normCV
16	9, 15	cfv 6563	. . . . . . . . . 10 class (normCV‘𝑢)
17	14, 16	cfv 6563	. . . . . . . . 9 class ((normCV‘𝑢)‘𝑧)
18		c1 11154	. . . . . . . . 9 class 1
19		cle 11294	. . . . . . . . 9 class ≤
20	17, 18, 19	wbr 5148	. . . . . . . 8 wff ((normCV‘𝑢)‘𝑧) ≤ 1
21		vx	. . . . . . . . . 10 setvar 𝑥
22	21	cv 1536	. . . . . . . . 9 class 𝑥
23	5	cv 1536	. . . . . . . . . . 11 class 𝑡
24	14, 23	cfv 6563	. . . . . . . . . 10 class (𝑡‘𝑧)
25	6, 15	cfv 6563	. . . . . . . . . 10 class (normCV‘𝑤)
26	24, 25	cfv 6563	. . . . . . . . 9 class ((normCV‘𝑤)‘(𝑡‘𝑧))
27	22, 26	wceq 1537	. . . . . . . 8 wff 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧))
28	20, 27	wa 395	. . . . . . 7 wff (((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))
29	28, 13, 10	wrex 3068	. . . . . 6 wff ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))
30	29, 21	cab 2712	. . . . 5 class {𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}
31		cxr 11292	. . . . 5 class ℝ*
32		clt 11293	. . . . 5 class <
33	30, 31, 32	csup 9478	. . . 4 class sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < )
34	5, 12, 33	cmpt 5231	. . 3 class (𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < ))
35	2, 3, 4, 4, 34	cmpo 7433	. 2 class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < )))
36	1, 35	wceq 1537	1 wff normOpOLD = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < )))

This definition is referenced by:  nmoofval  30791