Definition df-nmfn 28704

Description: Define the norm of a Hilbert space functional. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)

Assertion

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

Distinct variable group:   x, t, z

Detailed syntax breakdown of Definition df-nmfn

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

This definition is referenced by:  nmfnval  28735