Definition df-nmoo 31362

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 31358	. 2 class normOpOLD
2		vu	. . 3 setvar 𝑢
3		vw	. . 3 setvar 𝑤
4		cnv 31201	. . 3 class NrmCVec
5		vt	. . . 4 setvar 𝑡
6	3	cv 1568	. . . . . 6 class 𝑤
7		cba 31203	. . . . . 6 class BaseSet
8	6, 7	cfv 6547	. . . . 5 class (BaseSet‘𝑤)
9	2	cv 1568	. . . . . 6 class 𝑢
10	9, 7	cfv 6547	. . . . 5 class (BaseSet‘𝑢)
11		cmap 8861	. . . . 5 class ↑m
12	8, 10, 11	co 7430	. . . 4 class ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢))
13		vz	. . . . . . . . . . 11 setvar 𝑧
14	13	cv 1568	. . . . . . . . . 10 class 𝑧
15		cnmcv 31207	. . . . . . . . . . 11 class normCV
16	9, 15	cfv 6547	. . . . . . . . . 10 class (normCV‘𝑢)
17	14, 16	cfv 6547	. . . . . . . . 9 class ((normCV‘𝑢)‘𝑧)
18		c1 11214	. . . . . . . . 9 class 1
19		cle 11357	. . . . . . . . 9 class ≤
20	17, 18, 19	wbr 5106	. . . . . . . 8 wff ((normCV‘𝑢)‘𝑧) ≤ 1
21		vx	. . . . . . . . . 10 setvar 𝑥
22	21	cv 1568	. . . . . . . . 9 class 𝑥
23	5	cv 1568	. . . . . . . . . . 11 class 𝑡
24	14, 23	cfv 6547	. . . . . . . . . 10 class (𝑡‘𝑧)
25	6, 15	cfv 6547	. . . . . . . . . 10 class (normCV‘𝑤)
26	24, 25	cfv 6547	. . . . . . . . 9 class ((normCV‘𝑤)‘(𝑡‘𝑧))
27	22, 26	wceq 1569	. . . . . . . 8 wff 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧))
28	20, 27	wa 401	. . . . . . 7 wff (((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))
29	28, 13, 10	wrex 3090	. . . . . 6 wff ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))
30	29, 21	cab 2741	. . . . 5 class {𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}
31		cxr 11355	. . . . 5 class ℝ*
32		clt 11356	. . . . 5 class <
33	30, 31, 32	csup 9445	. . . 4 class sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < )
34	5, 12, 33	cmpt 5189	. . 3 class (𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < ))
35	2, 3, 4, 4, 34	cmpo 7432	. 2 class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < )))
36	1, 35	wceq 1569	1 wff normOpOLD = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < )))

This definition is used by:  nmoofval  31379