Definition df-nmo 8353

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:(Base` u)-->(Base` w) /\ y = sup({x | E.z e. (Base` 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 8349	. 2 class normOp
2		vu	. . . . . . 7 set u
3	2	cv 953	. . . . . 6 class u
4		cnv 8155	. . . . . 6 class NrmCVec
5	3, 4	wcel 956	. . . . 5 wff u e. NrmCVec
6		vw	. . . . . . 7 set w
7	6	cv 953	. . . . . 6 class w
8	7, 4	wcel 956	. . . . 5 wff w e. NrmCVec
9	5, 8	wa 223	. . . 4 wff (u e. NrmCVec /\ w e. NrmCVec)
10		vn	. . . . . 6 set n
11	10	cv 953	. . . . 5 class n
12		cba 8157	. . . . . . . . 9 class Base
13	3, 12	cfv 3177	. . . . . . . 8 class (Base` u)
14	7, 12	cfv 3177	. . . . . . . 8 class (Base` w)
15		vt	. . . . . . . . 9 set t
16	15	cv 953	. . . . . . . 8 class t
17	13, 14, 16	wf 3173	. . . . . . 7 wff t:(Base` u)-->(Base` w)
18		vy	. . . . . . . . 9 set y
19	18	cv 953	. . . . . . . 8 class y
20		vz	. . . . . . . . . . . . . . 15 set z
21	20	cv 953	. . . . . . . . . . . . . 14 class z
22		cnm 8161	. . . . . . . . . . . . . . 15 class norm
23	3, 22	cfv 3177	. . . . . . . . . . . . . 14 class (norm` u)
24	21, 23	cfv 3177	. . . . . . . . . . . . 13 class ((norm` u)` z)
25		c1 5215	. . . . . . . . . . . . 13 class 1
26		cle 5275	. . . . . . . . . . . . 13 class <_
27	24, 25, 26	wbr 2614	. . . . . . . . . . . 12 wff ((norm` u)` z) <_ 1
28		vx	. . . . . . . . . . . . . 14 set x
29	28	cv 953	. . . . . . . . . . . . 13 class x
30	21, 16	cfv 3177	. . . . . . . . . . . . . 14 class (t` z)
31	7, 22	cfv 3177	. . . . . . . . . . . . . 14 class (norm` w)
32	30, 31	cfv 3177	. . . . . . . . . . . . 13 class ((norm` w)` (t` z))
33	29, 32	wceq 954	. . . . . . . . . . . 12 wff x = ((norm` w)` (t` z))
34	27, 33	wa 223	. . . . . . . . . . 11 wff (((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))
35	34, 20, 13	wrex 1643	. . . . . . . . . 10 wff E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))
36	35, 28	cab 1461	. . . . . . . . 9 class {x | E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}
37		cxr 5465	. . . . . . . . 9 class RR*
38		clt 5466	. . . . . . . . 9 class <
39	36, 37, 38	csup 4553	. . . . . . . 8 class sup({x | E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < )
40	19, 39	wceq 954	. . . . . . 7 wff y = sup({x | E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < )
41	17, 40	wa 223	. . . . . 6 wff (t:(Base` u)-->(Base` w) /\ y = sup({x | E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ))
42	41, 15, 18	copab 2661	. . . . 5 class {<.t, y>. | (t:(Base` u)-->(Base` w) /\ y = sup({x | E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ))}
43	11, 42	wceq 954	. . . 4 wff n = {<.t, y>. | (t:(Base` u)-->(Base` w) /\ y = sup({x | E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ))}
44	9, 43	wa 223	. . 3 wff ((u e. NrmCVec /\ w e. NrmCVec) /\ n = {<.t, y>. | (t:(Base` u)-->(Base` w) /\ y = sup({x | E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ))})
45	44, 2, 6, 10	copab2 3955	. 2 class {<.<.u, w>., n>. | ((u e. NrmCVec /\ w e. NrmCVec) /\ n = {<.t, y>. | (t:(Base` u)-->(Base` w) /\ y = sup({x | E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ))})}
46	1, 45	wceq 954	1 wff normOp = {<.<.u, w>., n>. | ((u e. NrmCVec /\ w e. NrmCVec) /\ n = {<.t, y>. | (t:(Base` u)-->(Base` w) /\ y = sup({x | E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ))})}

This definition is referenced by:  nmofval 8370

Copyright terms: Public domain