Definition df-nmfn

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

	Ref	Expression
Assertion	df-nmfn	$$⊢{norm}_{\mathrm{fn}}=\left(t\in \left({ℂ}^{\mathscr{H}}\right)⟼sup\left(\left\{x|\exists z\in \mathscr{H}\left({norm}_{ℎ}\left(z\right)\le 1\wedge x=\left|t\left(z\right)\right|\right)\right\},{ℝ}^{*},<\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnmf	$$class{norm}_{\mathrm{fn}}$$
1		vt	$$setvart$$
2		cc	$$classℂ$$
3		cmap	$$class{\uparrow }_{𝑚}$$
4		chba	$$class\mathscr{H}$$
5	2 4 3	co	$$class\left({ℂ}^{\mathscr{H}}\right)$$
6		vx	$$setvarx$$
7		vz	$$setvarz$$
8		cno	$$class{norm}_{ℎ}$$
9	7	cv	$$setvarz$$
10	9 8	cfv	$$class{norm}_{ℎ}\left(z\right)$$
11		cle	$$class\le$$
12		c1	$$class1$$
13	10 12 11	wbr	$$wff{norm}_{ℎ}\left(z\right)\le 1$$
14	6	cv	$$setvarx$$
15		cabs	$$class\mathrm{abs}$$
16	1	cv	$$setvart$$
17	9 16	cfv	$$classt\left(z\right)$$
18	17 15	cfv	$$class\left|t\left(z\right)\right|$$
19	14 18	wceq	$$wffx=\left|t\left(z\right)\right|$$
20	13 19	wa	$$wff\left({norm}_{ℎ}\left(z\right)\le 1\wedge x=\left|t\left(z\right)\right|\right)$$
21	20 7 4	wrex	$$wff\exists z\in \mathscr{H}\left({norm}_{ℎ}\left(z\right)\le 1\wedge x=\left|t\left(z\right)\right|\right)$$
22	21 6	cab	$$class\left\{x|\exists z\in \mathscr{H}\left({norm}_{ℎ}\left(z\right)\le 1\wedge x=\left|t\left(z\right)\right|\right)\right\}$$
23		cxr	$$class{ℝ}^{*}$$
24		clt	$$class<$$
25	22 23 24	csup	$$classsup\left(\left\{x|\exists z\in \mathscr{H}\left({norm}_{ℎ}\left(z\right)\le 1\wedge x=\left|t\left(z\right)\right|\right)\right\},{ℝ}^{*},<\right)$$
26	1 5 25	cmpt	$$class\left(t\in \left({ℂ}^{\mathscr{H}}\right)⟼sup\left(\left\{x|\exists z\in \mathscr{H}\left({norm}_{ℎ}\left(z\right)\le 1\wedge x=\left|t\left(z\right)\right|\right)\right\},{ℝ}^{*},<\right)\right)$$
27	0 26	wceq	$$wff{norm}_{\mathrm{fn}}=\left(t\in \left({ℂ}^{\mathscr{H}}\right)⟼sup\left(\left\{x|\exists z\in \mathscr{H}\left({norm}_{ℎ}\left(z\right)\le 1\wedge x=\left|t\left(z\right)\right|\right)\right\},{ℝ}^{*},<\right)\right)$$