Definition df-nmop 11194

Description: Define the norm of a Hilbert space operator.

Assertion

Ref	Expression
df-nmop	|- normop = {<.t, y>. | (t:~H-->~H /\ y = sup({x | E.z e. ~H ((normh` z) <_ 1 /\ x = (normh` (t` z)))}, RR*, < ))}

Distinct variable group:   x,t,y,z

Detailed syntax breakdown of Definition df-nmop

Step	Hyp	Ref	Expression
1		cnop 10238	. 2 class normop
2		chil 10212	. . . . 5 class ~H
3		vt	. . . . . 6 set t
4	3	cv 1135	. . . . 5 class t
5	2, 2, 4	wf 3805	. . . 4 wff t:~H-->~H
6		vy	. . . . . 6 set y
7	6	cv 1135	. . . . 5 class y
8		vz	. . . . . . . . . . . 12 set z
9	8	cv 1135	. . . . . . . . . . 11 class z
10		cno 10218	. . . . . . . . . . 11 class normh
11	9, 10	cfv 3809	. . . . . . . . . 10 class (normh` z)
12		c1 6183	. . . . . . . . . 10 class 1
13		cle 6244	. . . . . . . . . 10 class <_
14	11, 12, 13	wbr 3158	. . . . . . . . 9 wff (normh` z) <_ 1
15		vx	. . . . . . . . . . 11 set x
16	15	cv 1135	. . . . . . . . . 10 class x
17	9, 4	cfv 3809	. . . . . . . . . . 11 class (t` z)
18	17, 10	cfv 3809	. . . . . . . . . 10 class (normh` (t` z))
19	16, 18	wceq 1136	. . . . . . . . 9 wff x = (normh` (t` z))
20	14, 19	wa 239	. . . . . . . 8 wff ((normh` z) <_ 1 /\ x = (normh` (t` z)))
21	20, 8, 2	wrex 1940	. . . . . . 7 wff E.z e. ~H ((normh` z) <_ 1 /\ x = (normh` (t` z)))
22	21, 15	cab 1708	. . . . . 6 class {x | E.z e. ~H ((normh` z) <_ 1 /\ x = (normh` (t` z)))}
23		cxr 6448	. . . . . 6 class RR*
24		clt 6449	. . . . . 6 class <
25	22, 23, 24	csup 5473	. . . . 5 class sup({x | E.z e. ~H ((normh` z) <_ 1 /\ x = (normh` (t` z)))}, RR*, < )
26	7, 25	wceq 1136	. . . 4 wff y = sup({x | E.z e. ~H ((normh` z) <_ 1 /\ x = (normh` (t` z)))}, RR*, < )
27	5, 26	wa 239	. . 3 wff (t:~H-->~H /\ y = sup({x | E.z e. ~H ((normh` z) <_ 1 /\ x = (normh` (t` z)))}, RR*, < ))
28	27, 3, 6	copab 3213	. 2 class {<.t, y>. | (t:~H-->~H /\ y = sup({x | E.z e. ~H ((normh` z) <_ 1 /\ x = (normh` (t` z)))}, RR*, < ))}
29	1, 28	wceq 1136	1 wff normop = {<.t, y>. | (t:~H-->~H /\ y = sup({x | E.z e. ~H ((normh` z) <_ 1 /\ x = (normh` (t` z)))}, RR*, < ))}

This definition is referenced by:  nmopval 11211  hhnmoi 11256

Copyright terms: Public domain