Definition df-nmo 8340

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 8336	. 2 class normOp
2		vu	. . . . . . 7 set u
3	2	cv 952	. . . . . 6 class u
4		cnv 8141	. . . . . 6 class NrmCVec
5	3, 4	wcel 955	. . . . 5 wff u e. NrmCVec
6		vw	. . . . . . 7 set w
7	6	cv 952	. . . . . 6 class w
8	7, 4	wcel 955	. . . . 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 952	. . . . 5 class n
12		cba 8143	. . . . . . . . 9 class Base
13	3, 12	cfv 3172	. . . . . . . 8 class (Base` u)
14	7, 12	cfv 3172	. . . . . . . 8 class (Base` w)
15		vt	. . . . . . . . 9 set t
16	15	cv 952	. . . . . . . 8 class t
17	13, 14, 16	wf 3168	. . . . . . 7 wff t:(Base` u)-->(Base` w)
18		vy	. . . . . . . . 9 set y
19	18	cv 952	. . . . . . . 8 class y
20		vz	. . . . . . . . . . . . . . 15 set z
21	20	cv 952	. . . . . . . . . . . . . 14 class z
22		cnm 8147	. . . . . . . . . . . . . . 15 class norm
23	3, 22	cfv 3172	. . . . . . . . . . . . . 14 class (norm` u)
24	21, 23	cfv 3172	. . . . . . . . . . . . 13 class ((norm` u)` z)
25		c1 5207	. . . . . . . . . . . . 13 class 1
26		cle 5267	. . . . . . . . . . . . 13 class <_
27	24, 25, 26	wbr 2609	. . . . . . . . . . . 12 wff ((norm` u)` z) <_ 1
28		vx	. . . . . . . . . . . . . 14 set x
29	28	cv 952	. . . . . . . . . . . . 13 class x
30	21, 16	cfv 3172	. . . . . . . . . . . . . 14 class (t` z)
31	7, 22	cfv 3172	. . . . . . . . . . . . . 14 class (norm` w)
32	30, 31	cfv 3172	. . . . . . . . . . . . 13 class ((norm` w)` (t` z))
33	29, 32	wceq 953	. . . . . . . . . . . 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 1638	. . . . . . . . . 10 wff E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))
36	35, 28	cab 1456	. . . . . . . . 9 class {x | E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}
37		cxr 5457	. . . . . . . . 9 class RR*
38		clt 5458	. . . . . . . . 9 class <
39	36, 37, 38	csup 4547	. . . . . . . 8 class sup({x | E.z e. (Base` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < )
40	19, 39	wceq 953	. . . . . . 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 2656	. . . . 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 953	. . . 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 3949	. 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 953	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 8357

Copyright terms: Public domain