Definition df-nmo 9540

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.

Assertion

Ref	Expression
df-nmo	|- normOp = {<.<.u, w>., n>. | ((u e. NrmCVec /\ w e. NrmCVec) /\ n = {<.t, y>. | (t:(BaseSet` u)-->(BaseSet` w) /\ y = sup({x | E.z e. (BaseSet` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ))})}

Distinct variable group:   t,n,u,w,x,y,z

Detailed syntax breakdown of Definition df-nmo

Step	Hyp	Ref	Expression
1		cnmo 9536	. 2 class normOp
2		vu	. . . . . . 7 set u
3	2	cv 1135	. . . . . 6 class u
4		cnv 9330	. . . . . 6 class NrmCVec
5	3, 4	wcel 1138	. . . . 5 wff u e. NrmCVec
6		vw	. . . . . . 7 set w
7	6	cv 1135	. . . . . 6 class w
8	7, 4	wcel 1138	. . . . 5 wff w e. NrmCVec
9	5, 8	wa 239	. . . 4 wff (u e. NrmCVec /\ w e. NrmCVec)
10		vn	. . . . . 6 set n
11	10	cv 1135	. . . . 5 class n
12		cba 9332	. . . . . . . . 9 class BaseSet
13	3, 12	cfv 3809	. . . . . . . 8 class (BaseSet` u)
14	7, 12	cfv 3809	. . . . . . . 8 class (BaseSet` w)
15		vt	. . . . . . . . 9 set t
16	15	cv 1135	. . . . . . . 8 class t
17	13, 14, 16	wf 3805	. . . . . . 7 wff t:(BaseSet` u)-->(BaseSet` w)
18		vy	. . . . . . . . 9 set y
19	18	cv 1135	. . . . . . . 8 class y
20		vz	. . . . . . . . . . . . . . 15 set z
21	20	cv 1135	. . . . . . . . . . . . . 14 class z
22		cnm 9336	. . . . . . . . . . . . . . 15 class norm
23	3, 22	cfv 3809	. . . . . . . . . . . . . 14 class (norm` u)
24	21, 23	cfv 3809	. . . . . . . . . . . . 13 class ((norm` u)` z)
25		c1 6183	. . . . . . . . . . . . 13 class 1
26		cle 6244	. . . . . . . . . . . . 13 class <_
27	24, 25, 26	wbr 3158	. . . . . . . . . . . 12 wff ((norm` u)` z) <_ 1
28		vx	. . . . . . . . . . . . . 14 set x
29	28	cv 1135	. . . . . . . . . . . . 13 class x
30	21, 16	cfv 3809	. . . . . . . . . . . . . 14 class (t` z)
31	7, 22	cfv 3809	. . . . . . . . . . . . . 14 class (norm` w)
32	30, 31	cfv 3809	. . . . . . . . . . . . 13 class ((norm` w)` (t` z))
33	29, 32	wceq 1136	. . . . . . . . . . . 12 wff x = ((norm` w)` (t` z))
34	27, 33	wa 239	. . . . . . . . . . 11 wff (((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))
35	34, 20, 13	wrex 1940	. . . . . . . . . 10 wff E.z e. (BaseSet` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))
36	35, 28	cab 1708	. . . . . . . . 9 class {x | E.z e. (BaseSet` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}
37		cxr 6448	. . . . . . . . 9 class RR*
38		clt 6449	. . . . . . . . 9 class <
39	36, 37, 38	csup 5473	. . . . . . . 8 class sup({x | E.z e. (BaseSet` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < )
40	19, 39	wceq 1136	. . . . . . 7 wff y = sup({x | E.z e. (BaseSet` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < )
41	17, 40	wa 239	. . . . . 6 wff (t:(BaseSet` u)-->(BaseSet` w) /\ y = sup({x | E.z e. (BaseSet` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ))
42	41, 15, 18	copab 3213	. . . . 5 class {<.t, y>. | (t:(BaseSet` u)-->(BaseSet` w) /\ y = sup({x | E.z e. (BaseSet` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ))}
43	11, 42	wceq 1136	. . . 4 wff n = {<.t, y>. | (t:(BaseSet` u)-->(BaseSet` w) /\ y = sup({x | E.z e. (BaseSet` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ))}
44	9, 43	wa 239	. . 3 wff ((u e. NrmCVec /\ w e. NrmCVec) /\ n = {<.t, y>. | (t:(BaseSet` u)-->(BaseSet` w) /\ y = sup({x | E.z e. (BaseSet` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ))})
45	44, 2, 6, 10	copab2 4696	. 2 class {<.<.u, w>., n>. | ((u e. NrmCVec /\ w e. NrmCVec) /\ n = {<.t, y>. | (t:(BaseSet` u)-->(BaseSet` w) /\ y = sup({x | E.z e. (BaseSet` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ))})}
46	1, 45	wceq 1136	1 wff normOp = {<.<.u, w>., n>. | ((u e. NrmCVec /\ w e. NrmCVec) /\ n = {<.t, y>. | (t:(BaseSet` u)-->(BaseSet` w) /\ y = sup({x | E.z e. (BaseSet` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ))})}

This definition is referenced by:  nmofval 9559

Copyright terms: Public domain