Definition df-nmoo

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 <. u , w >. . 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.)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnmoo	⊢ normOpOLD
1		vu	⊢ 𝑢
2		cnv	⊢ NrmCVec
3		vw	⊢ 𝑤
4		vt	⊢ 𝑡
5		cba	⊢ BaseSet
6	3	cv	⊢ 𝑤
7	6 5	cfv	⊢ ( BaseSet ‘ 𝑤 )
8		cmap	⊢ ↑m
9	1	cv	⊢ 𝑢
10	9 5	cfv	⊢ ( BaseSet ‘ 𝑢 )
11	7 10 8	co	⊢ ( ( BaseSet ‘ 𝑤 ) ↑m ( BaseSet ‘ 𝑢 ) )
12		vx	⊢ 𝑥
13		vz	⊢ 𝑧
14		cnmcv	⊢ normCV
15	9 14	cfv	⊢ ( normCV ‘ 𝑢 )
16	13	cv	⊢ 𝑧
17	16 15	cfv	⊢ ( ( normCV ‘ 𝑢 ) ‘ 𝑧 )
18		cle	⊢ ≤
19		c1	⊢ 1
20	17 19 18	wbr	⊢ ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1
21	12	cv	⊢ 𝑥
22	6 14	cfv	⊢ ( normCV ‘ 𝑤 )
23	4	cv	⊢ 𝑡
24	16 23	cfv	⊢ ( 𝑡 ‘ 𝑧 )
25	24 22	cfv	⊢ ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) )
26	21 25	wceq	⊢ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) )
27	20 26	wa	⊢ ( ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) )
28	27 13 10	wrex	⊢ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑢 ) ( ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) )
29	28 12	cab	⊢ { 𝑥 ∣ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑢 ) ( ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) }
30		cxr	⊢ ℝ*
31		clt	⊢ <
32	29 30 31	csup	⊢ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑢 ) ( ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < )
33	4 11 32	cmpt	⊢ ( 𝑡 ∈ ( ( BaseSet ‘ 𝑤 ) ↑m ( BaseSet ‘ 𝑢 ) ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑢 ) ( ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
34	1 3 2 2 33	cmpo	⊢ ( 𝑢 ∈ NrmCVec , 𝑤 ∈ NrmCVec ↦ ( 𝑡 ∈ ( ( BaseSet ‘ 𝑤 ) ↑m ( BaseSet ‘ 𝑢 ) ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑢 ) ( ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) )
35	0 34	wceq	⊢ normOpOLD = ( 𝑢 ∈ NrmCVec , 𝑤 ∈ NrmCVec ↦ ( 𝑡 ∈ ( ( BaseSet ‘ 𝑤 ) ↑m ( BaseSet ‘ 𝑢 ) ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑢 ) ( ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) )