Definition df-nmfn 10051

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 9095	. 2 class normfn
2		chil 9063	. . . . 5 class H~
3		cc 5386	. . . . 5 class CC
4		vt	. . . . . 6 set t
5	4	cv 991	. . . . 5 class t
6	2, 3, 5	wf 3259	. . . 4 wff t:H~-->CC
7		vy	. . . . . 6 set y
8	7	cv 991	. . . . 5 class y
9		vz	. . . . . . . . . . . 12 set z
10	9	cv 991	. . . . . . . . . . 11 class z
11		cno 9069	. . . . . . . . . . 11 class normh
12	10, 11	cfv 3263	. . . . . . . . . 10 class (normh` z)
13		c1 5389	. . . . . . . . . 10 class 1
14		cle 5449	. . . . . . . . . 10 class <_
15	12, 13, 14	wbr 2692	. . . . . . . . 9 wff (normh` z) <_ 1
16		vx	. . . . . . . . . . 11 set x
17	16	cv 991	. . . . . . . . . 10 class x
18	10, 5	cfv 3263	. . . . . . . . . . 11 class (t` z)
19		cabs 6951	. . . . . . . . . . 11 class abs
20	18, 19	cfv 3263	. . . . . . . . . 10 class (abs` (t` z))
21	17, 20	wceq 992	. . . . . . . . 9 wff x = (abs` (t` z))
22	15, 21	wa 221	. . . . . . . 8 wff ((normh` z) <_ 1 /\ x = (abs` (t` z)))
23	22, 9, 2	wrex 1692	. . . . . . 7 wff E.z e. H~ ((normh` z) <_ 1 /\ x = (abs` (t` z)))
24	23, 16	cab 1505	. . . . . 6 class {x | E.z e. H~ ((normh` z) <_ 1 /\ x = (abs` (t` z)))}
25		cxr 5639	. . . . . 6 class RR*
26		clt 5640	. . . . . 6 class <
27	24, 25, 26	csup 4716	. . . . 5 class sup({x | E.z e. H~ ((normh` z) <_ 1 /\ x = (abs` (t` z)))}, RR*, < )
28	8, 27	wceq 992	. . . 4 wff y = sup({x | E.z e. H~ ((normh` z) <_ 1 /\ x = (abs` (t` z)))}, RR*, < )
29	6, 28	wa 221	. . 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 2740	. 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 992	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:  nmfnval 10083

Copyright terms: Public domain