Definition df-nmfn 11200

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 10244	. 2 class normfn
2		chil 10212	. . . . 5 class ~H
3		cc 6180	. . . . 5 class CC
4		vt	. . . . . 6 set t
5	4	cv 1135	. . . . 5 class t
6	2, 3, 5	wf 3805	. . . 4 wff t:~H-->CC
7		vy	. . . . . 6 set y
8	7	cv 1135	. . . . 5 class y
9		vz	. . . . . . . . . . . 12 set z
10	9	cv 1135	. . . . . . . . . . 11 class z
11		cno 10218	. . . . . . . . . . 11 class normh
12	10, 11	cfv 3809	. . . . . . . . . 10 class (normh` z)
13		c1 6183	. . . . . . . . . 10 class 1
14		cle 6244	. . . . . . . . . 10 class <_
15	12, 13, 14	wbr 3158	. . . . . . . . 9 wff (normh` z) <_ 1
16		vx	. . . . . . . . . . 11 set x
17	16	cv 1135	. . . . . . . . . 10 class x
18	10, 5	cfv 3809	. . . . . . . . . . 11 class (t` z)
19		cabs 7795	. . . . . . . . . . 11 class abs
20	18, 19	cfv 3809	. . . . . . . . . 10 class (abs` (t` z))
21	17, 20	wceq 1136	. . . . . . . . 9 wff x = (abs` (t` z))
22	15, 21	wa 239	. . . . . . . 8 wff ((normh` z) <_ 1 /\ x = (abs` (t` z)))
23	22, 9, 2	wrex 1940	. . . . . . 7 wff E.z e. ~H ((normh` z) <_ 1 /\ x = (abs` (t` z)))
24	23, 16	cab 1708	. . . . . 6 class {x | E.z e. ~H ((normh` z) <_ 1 /\ x = (abs` (t` z)))}
25		cxr 6448	. . . . . 6 class RR*
26		clt 6449	. . . . . 6 class <
27	24, 25, 26	csup 5473	. . . . 5 class sup({x | E.z e. ~H ((normh` z) <_ 1 /\ x = (abs` (t` z)))}, RR*, < )
28	8, 27	wceq 1136	. . . 4 wff y = sup({x | E.z e. ~H ((normh` z) <_ 1 /\ x = (abs` (t` z)))}, RR*, < )
29	6, 28	wa 239	. . 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 3213	. 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 1136	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 11232

Copyright terms: Public domain