Definition df-nmop 9760

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 8809	. 2 class normop
2		chil 8783	. . . . 5 class H~
3		vt	. . . . . 6 set t
4	3	cv 957	. . . . 5 class t
5	2, 2, 4	wf 3184	. . . 4 wff t:H~-->H~
6		vy	. . . . . 6 set y
7	6	cv 957	. . . . 5 class y
8		vz	. . . . . . . . . . . 12 set z
9	8	cv 957	. . . . . . . . . . 11 class z
10		cno 8789	. . . . . . . . . . 11 class normh
11	9, 10	cfv 3188	. . . . . . . . . 10 class (normh` z)
12		c1 5247	. . . . . . . . . 10 class 1
13		cle 5307	. . . . . . . . . 10 class <_
14	11, 12, 13	wbr 2624	. . . . . . . . 9 wff (normh` z) <_ 1
15		vx	. . . . . . . . . . 11 set x
16	15	cv 957	. . . . . . . . . 10 class x
17	9, 4	cfv 3188	. . . . . . . . . . 11 class (t` z)
18	17, 10	cfv 3188	. . . . . . . . . 10 class (normh` (t` z))
19	16, 18	wceq 958	. . . . . . . . 9 wff x = (normh` (t` z))
20	14, 19	wa 223	. . . . . . . 8 wff ((normh` z) <_ 1 /\ x = (normh` (t` z)))
21	20, 8, 2	wrex 1649	. . . . . . 7 wff E.z e. H~ ((normh` z) <_ 1 /\ x = (normh` (t` z)))
22	21, 15	cab 1466	. . . . . 6 class {x | E.z e. H~ ((normh` z) <_ 1 /\ x = (normh` (t` z)))}
23		cxr 5497	. . . . . 6 class RR*
24		clt 5498	. . . . . 6 class <
25	22, 23, 24	csup 4582	. . . . 5 class sup({x | E.z e. H~ ((normh` z) <_ 1 /\ x = (normh` (t` z)))}, RR*, < )
26	7, 25	wceq 958	. . . 4 wff y = sup({x | E.z e. H~ ((normh` z) <_ 1 /\ x = (normh` (t` z)))}, RR*, < )
27	5, 26	wa 223	. . 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 2671	. 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 958	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:  nmopvalt 9777  hhnmo 9822

Copyright terms: Public domain