Definition df-nmoo 28151

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 28147	. 2 class normOpOLD
2		vu	. . 3 setvar 𝑢
3		vw	. . 3 setvar 𝑤
4		cnv 27990	. . 3 class NrmCVec
5		vt	. . . 4 setvar 𝑡
6	3	cv 1655	. . . . . 6 class 𝑤
7		cba 27992	. . . . . 6 class BaseSet
8	6, 7	cfv 6127	. . . . 5 class (BaseSet‘𝑤)
9	2	cv 1655	. . . . . 6 class 𝑢
10	9, 7	cfv 6127	. . . . 5 class (BaseSet‘𝑢)
11		cmap 8127	. . . . 5 class ↑𝑚
12	8, 10, 11	co 6910	. . . 4 class ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢))
13		vz	. . . . . . . . . . 11 setvar 𝑧
14	13	cv 1655	. . . . . . . . . 10 class 𝑧
15		cnmcv 27996	. . . . . . . . . . 11 class normCV
16	9, 15	cfv 6127	. . . . . . . . . 10 class (normCV‘𝑢)
17	14, 16	cfv 6127	. . . . . . . . 9 class ((normCV‘𝑢)‘𝑧)
18		c1 10260	. . . . . . . . 9 class 1
19		cle 10399	. . . . . . . . 9 class ≤
20	17, 18, 19	wbr 4875	. . . . . . . 8 wff ((normCV‘𝑢)‘𝑧) ≤ 1
21		vx	. . . . . . . . . 10 setvar 𝑥
22	21	cv 1655	. . . . . . . . 9 class 𝑥
23	5	cv 1655	. . . . . . . . . . 11 class 𝑡
24	14, 23	cfv 6127	. . . . . . . . . 10 class (𝑡‘𝑧)
25	6, 15	cfv 6127	. . . . . . . . . 10 class (normCV‘𝑤)
26	24, 25	cfv 6127	. . . . . . . . 9 class ((normCV‘𝑤)‘(𝑡‘𝑧))
27	22, 26	wceq 1656	. . . . . . . 8 wff 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧))
28	20, 27	wa 386	. . . . . . 7 wff (((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))
29	28, 13, 10	wrex 3118	. . . . . 6 wff ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))
30	29, 21	cab 2811	. . . . 5 class {𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}
31		cxr 10397	. . . . 5 class ℝ*
32		clt 10398	. . . . 5 class <
33	30, 31, 32	csup 8621	. . . 4 class sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < )
34	5, 12, 33	cmpt 4954	. . 3 class (𝑡 ∈ ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < ))
35	2, 3, 4, 4, 34	cmpt2 6912	. 2 class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < )))
36	1, 35	wceq 1656	1 wff normOpOLD = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < )))

This definition is referenced by:  nmoofval  28168