Definition df-nmfn 9902

Description: Define the norm of a Hilbert space functional.

Assertion

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

Distinct variable group:   x,t,y,z

Detailed syntax breakdown of Definition df-nmfn

Step	Hyp	Ref	Expression
1		cnmf 9000	. 2 class normfn
2		chil 8968	. . . . 5 class H~
3		cc 5155	. . . . 5 class CC
4		vt	. . . . . 6 set t
5	4	cv 1098	. . . . 5 class t
6	2, 3, 5	wf 3141	. . . 4 wff t:H~-->CC
7		vy	. . . . . 6 set y
8	7	cv 1098	. . . . 5 class y
9		vz	. . . . . . . . . . . 12 set z
10	9	cv 1098	. . . . . . . . . . 11 class z
11		cno 8974	. . . . . . . . . . 11 class normh
12	10, 11	cfv 3145	. . . . . . . . . 10 class (normh` z)
13		c1 5158	. . . . . . . . . 10 class 1
14		cle 5218	. . . . . . . . . 10 class <_
15	12, 13, 14	wbr 2587	. . . . . . . . 9 wff (normh` z) <_ 1
16		vx	. . . . . . . . . . 11 set x
17	16	cv 1098	. . . . . . . . . 10 class x
18	10, 5	cfv 3145	. . . . . . . . . . 11 class (t` z)
19		cabs 6632	. . . . . . . . . . 11 class abs
20	18, 19	cfv 3145	. . . . . . . . . 10 class (abs` (t` z))
21	17, 20	wceq 1099	. . . . . . . . 9 wff x = (abs` (t` z))
22	15, 21	wa 223	. . . . . . . 8 wff ((normh` z) <_ 1 /\ x = (abs` (t` z)))
23	22, 9, 2	wrex 1622	. . . . . . 7 wff E.z e. H~ ((normh` z) <_ 1 /\ x = (abs` (t` z)))
24	23, 16	cab 1440	. . . . . 6 class {x | E.z e. H~ ((normh` z) <_ 1 /\ x = (abs` (t` z)))}
25		cxr 5408	. . . . . 6 class RR*
26		clt 5409	. . . . . 6 class <
27	24, 25, 26	csup 4499	. . . . 5 class sup({x | E.z e. H~ ((normh` z) <_ 1 /\ x = (abs` (t` z)))}, RR*, < )
28	8, 27	wceq 1099	. . . 4 wff y = sup({x | E.z e. H~ ((normh` z) <_ 1 /\ x = (abs` (t` z)))}, RR*, < )
29	6, 28	wa 223	. . 3 wff (t:H~-->CC /\ y = sup({x | E.z e. H~ ((normh` z) <_ 1 /\ x = (abs` (t` z)))}, RR*, < ))
30	29, 4, 7	copab 2634	. 2 class {<.t, y>. | (t:H~-->CC /\ y = sup({x | E.z e. H~ ((normh` z) <_ 1 /\ x = (abs` (t` z)))}, RR*, < ))}
31	1, 30	wceq 1099	1 wff normfn = {<.t, y>. | (t:H~-->CC /\ y = sup({x | E.z e. H~ ((normh` z) <_ 1 /\ x = (abs` (t` z)))}, RR*, < ))}

This definition is referenced by:  nmfnvalt 9934

Copyright terms: Public domain