Definition df-nmop 9682

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 8753	. 2 class normop
2		chil 8727	. . . . 5 class H~
3		vt	. . . . . 6 set t
4	3	cv 952	. . . . 5 class t
5	2, 2, 4	wf 3168	. . . 4 wff t:H~-->H~
6		vy	. . . . . 6 set y
7	6	cv 952	. . . . 5 class y
8		vz	. . . . . . . . . . . 12 set z
9	8	cv 952	. . . . . . . . . . 11 class z
10		cno 8733	. . . . . . . . . . 11 class normh
11	9, 10	cfv 3172	. . . . . . . . . 10 class (normh` z)
12		c1 5207	. . . . . . . . . 10 class 1
13		cle 5267	. . . . . . . . . 10 class <_
14	11, 12, 13	wbr 2609	. . . . . . . . 9 wff (normh` z) <_ 1
15		vx	. . . . . . . . . . 11 set x
16	15	cv 952	. . . . . . . . . 10 class x
17	9, 4	cfv 3172	. . . . . . . . . . 11 class (t` z)
18	17, 10	cfv 3172	. . . . . . . . . 10 class (normh` (t` z))
19	16, 18	wceq 953	. . . . . . . . 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 1638	. . . . . . 7 wff E.z e. H~ ((normh` z) <_ 1 /\ x = (normh` (t` z)))
22	21, 15	cab 1456	. . . . . 6 class {x | E.z e. H~ ((normh` z) <_ 1 /\ x = (normh` (t` z)))}
23		cxr 5457	. . . . . 6 class RR*
24		clt 5458	. . . . . 6 class <
25	22, 23, 24	csup 4547	. . . . 5 class sup({x | E.z e. H~ ((normh` z) <_ 1 /\ x = (normh` (t` z)))}, RR*, < )
26	7, 25	wceq 953	. . . 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 2656	. 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 953	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 9699  hhnmo 9744

Copyright terms: Public domain