Definition df-nmo 8275

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 8271	. 2 class normOp
2		vu	. . . . . . 7 set u
3	2	cv 1098	. . . . . 6 class u
4		cnv 8084	. . . . . 6 class NrmCVec
5	3, 4	wcel 1105	. . . . 5 wff u e. NrmCVec
6		vw	. . . . . . 7 set w
7	6	cv 1098	. . . . . 6 class w
8	7, 4	wcel 1105	. . . . 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 1098	. . . . 5 class n
12		cba 8086	. . . . . . . . 9 class Base
13	3, 12	cfv 3145	. . . . . . . 8 class (Base` u)
14	7, 12	cfv 3145	. . . . . . . 8 class (Base` w)
15		vt	. . . . . . . . 9 set t
16	15	cv 1098	. . . . . . . 8 class t
17	13, 14, 16	wf 3141	. . . . . . 7 wff t:(Base` u)-->(Base` w)
18		vy	. . . . . . . . 9 set y
19	18	cv 1098	. . . . . . . 8 class y
20		vz	. . . . . . . . . . . . . . 15 set z
21	20	cv 1098	. . . . . . . . . . . . . 14 class z
22		cnm 8090	. . . . . . . . . . . . . . 15 class norm
23	3, 22	cfv 3145	. . . . . . . . . . . . . 14 class (norm` u)
24	21, 23	cfv 3145	. . . . . . . . . . . . 13 class ((norm` u)` z)
25		c1 5158	. . . . . . . . . . . . 13 class 1
26		cle 5218	. . . . . . . . . . . . 13 class <_
27	24, 25, 26	wbr 2587	. . . . . . . . . . . 12 wff ((norm` u)` z) <_ 1
28		vx	. . . . . . . . . . . . . 14 set x
29	28	cv 1098	. . . . . . . . . . . . 13 class x
30	21, 16	cfv 3145	. . . . . . . . . . . . . 14 class (t` z)
31	7, 22	cfv 3145	. . . . . . . . . . . . . 14 class (norm` w)
32	30, 31	cfv 3145	. . . . . . . . . . . . 13 class ((norm` w)` (t` z))
33	29, 32	wceq 1099	. . . . . . . . . . . 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 1622	. . . . . . . . . 10 wff E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))
36	35, 28	cab 1440	. . . . . . . . 9 class {x | E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}
37		cxr 5408	. . . . . . . . 9 class RR*
38		clt 5409	. . . . . . . . 9 class <
39	36, 37, 38	csup 4499	. . . . . . . 8 class sup({x | E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < )
40	19, 39	wceq 1099	. . . . . . 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 2634	. . . . 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 1099	. . . 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 3903	. 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 1099	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 8292

Copyright terms: Public domain