Definition df-nmop 28698

Description: Define the norm of a Hilbert space operator. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)

Assertion

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

Distinct variable group:   x, t, z

Detailed syntax breakdown of Definition df-nmop

Step	Hyp	Ref	Expression
1		cnop 27802	. 2 class normop
2		vt	. . 3 setvar t
3		chil 27776	. . . 4 class ~H
4		cmap 7857	. . . 4 class ^m
5	3, 3, 4	co 6650	. . 3 class ( ~H ^m ~H )
6		vz	. . . . . . . . . 10 setvar z
7	6	cv 1482	. . . . . . . . 9 class z
8		cno 27780	. . . . . . . . 9 class normh
9	7, 8	cfv 5888	. . . . . . . 8 class ( normh ` z )
10		c1 9937	. . . . . . . 8 class 1
11		cle 10075	. . . . . . . 8 class <_
12	9, 10, 11	wbr 4653	. . . . . . 7 wff ( normh ` z ) <_ 1
13		vx	. . . . . . . . 9 setvar x
14	13	cv 1482	. . . . . . . 8 class x
15	2	cv 1482	. . . . . . . . . 10 class t
16	7, 15	cfv 5888	. . . . . . . . 9 class ( t ` z )
17	16, 8	cfv 5888	. . . . . . . 8 class ( normh ` ( t ` z ) )
18	14, 17	wceq 1483	. . . . . . 7 wff x = ( normh ` ( t ` z ) )
19	12, 18	wa 384	. . . . . 6 wff ( ( normh ` z ) <_ 1 /\ x = ( normh ` ( t ` z ) ) )
20	19, 6, 3	wrex 2913	. . . . 5 wff E. z e. ~H ( ( normh ` z ) <_ 1 /\ x = ( normh ` ( t ` z ) ) )
21	20, 13	cab 2608	. . . 4 class { x | E. z e. ~H ( ( normh ` z ) <_ 1 /\ x = ( normh ` ( t ` z ) ) ) }
22		cxr 10073	. . . 4 class RR*
23		clt 10074	. . . 4 class <
24	21, 22, 23	csup 8346	. . 3 class sup ( { x | E. z e. ~H ( ( normh ` z ) <_ 1 /\ x = ( normh ` ( t ` z ) ) ) } , RR* , < )
25	2, 5, 24	cmpt 4729	. 2 class ( t e. ( ~H ^m ~H ) |-> sup ( { x | E. z e. ~H ( ( normh ` z ) <_ 1 /\ x = ( normh ` ( t ` z ) ) ) } , RR* , < ) )
26	1, 25	wceq 1483	1 wff normop = ( t e. ( ~H ^m ~H ) |-> sup ( { x | E. z e. ~H ( ( normh ` z ) <_ 1 /\ x = ( normh ` ( t ` z ) ) ) } , RR* , < ) )

This definition is referenced by:  nmopval  28715  hhnmoi  28760