Theorem nmcfnexi

Description: The norm of a continuous linear Hilbert space functional exists. Theorem 3.5(i) of Beran p. 99. (Contributed by NM, 14-Feb-2006) (Proof shortened by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmcfnex.1	$$⊢T\in \mathrm{LinFn}$$
	nmcfnex.2	$$⊢T\in \mathrm{ContFn}$$
Assertion	nmcfnexi	$$⊢{norm}_{\mathrm{fn}}\left(T\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		nmcfnex.1	$$⊢T\in \mathrm{LinFn}$$
2		nmcfnex.2	$$⊢T\in \mathrm{ContFn}$$
3		ax-hv0cl	$$⊢0_{ℎ}\in \mathscr{H}$$
4		1rp	$$⊢1\in {ℝ}^{+}$$
5		cnfnc	$$⊢\left(T\in \mathrm{ContFn}\wedge 0_{ℎ}\in \mathscr{H}\wedge 1\in {ℝ}^{+}\right)\to \exists y\in {ℝ}^{+}\forall z\in \mathscr{H}\left({norm}_{ℎ}\left(z{-}_{ℎ}{0}_{ℎ}\right)<y\to \left|T\left(z\right)-T\left(0_{ℎ}\right)\right|<1\right)$$
6	2 3 4 5	mp3an	$$⊢\exists y\in {ℝ}^{+}\forall z\in \mathscr{H}\left({norm}_{ℎ}\left(z{-}_{ℎ}{0}_{ℎ}\right)<y\to \left|T\left(z\right)-T\left(0_{ℎ}\right)\right|<1\right)$$
7		hvsub0	$$⊢z\in \mathscr{H}\to z{-}_{ℎ}{0}_{ℎ}=z$$
8	7	fveq2d	$$⊢z\in \mathscr{H}\to {norm}_{ℎ}\left(z{-}_{ℎ}{0}_{ℎ}\right)={norm}_{ℎ}\left(z\right)$$
9	8	breq1d	$$⊢z\in \mathscr{H}\to \left({norm}_{ℎ}\left(z{-}_{ℎ}{0}_{ℎ}\right)<y\leftrightarrow {norm}_{ℎ}\left(z\right)<y\right)$$
10	1	lnfn0i	$$⊢T\left(0_{ℎ}\right)=0$$
11	10	oveq2i	$$⊢T\left(z\right)-T\left(0_{ℎ}\right)=T\left(z\right)-0$$
12	1	lnfnfi	$$⊢T:\mathscr{H}⟶ℂ$$
13	12	ffvelrni	$$⊢z\in \mathscr{H}\to T\left(z\right)\in ℂ$$
14	13	subid1d	$$⊢z\in \mathscr{H}\to T\left(z\right)-0=T\left(z\right)$$
15	11 14	syl5eq	$$⊢z\in \mathscr{H}\to T\left(z\right)-T\left(0_{ℎ}\right)=T\left(z\right)$$
16	15	fveq2d	$$⊢z\in \mathscr{H}\to \left|T\left(z\right)-T\left(0_{ℎ}\right)\right|=\left|T\left(z\right)\right|$$
17	16	breq1d	$$⊢z\in \mathscr{H}\to \left(\left|T\left(z\right)-T\left(0_{ℎ}\right)\right|<1\leftrightarrow \left|T\left(z\right)\right|<1\right)$$
18	9 17	imbi12d	$$⊢z\in \mathscr{H}\to \left(\left({norm}_{ℎ}\left(z{-}_{ℎ}{0}_{ℎ}\right)<y\to \left|T\left(z\right)-T\left(0_{ℎ}\right)\right|<1\right)\leftrightarrow \left({norm}_{ℎ}\left(z\right)<y\to \left|T\left(z\right)\right|<1\right)\right)$$
19	18	ralbiia	$$⊢\forall z\in \mathscr{H}\left({norm}_{ℎ}\left(z{-}_{ℎ}{0}_{ℎ}\right)<y\to \left|T\left(z\right)-T\left(0_{ℎ}\right)\right|<1\right)\leftrightarrow \forall z\in \mathscr{H}\left({norm}_{ℎ}\left(z\right)<y\to \left|T\left(z\right)\right|<1\right)$$
20	19	rexbii	$$⊢\exists y\in {ℝ}^{+}\forall z\in \mathscr{H}\left({norm}_{ℎ}\left(z{-}_{ℎ}{0}_{ℎ}\right)<y\to \left|T\left(z\right)-T\left(0_{ℎ}\right)\right|<1\right)\leftrightarrow \exists y\in {ℝ}^{+}\forall z\in \mathscr{H}\left({norm}_{ℎ}\left(z\right)<y\to \left|T\left(z\right)\right|<1\right)$$
21	6 20	mpbi	$$⊢\exists y\in {ℝ}^{+}\forall z\in \mathscr{H}\left({norm}_{ℎ}\left(z\right)<y\to \left|T\left(z\right)\right|<1\right)$$
22		nmfnval	$$⊢T:\mathscr{H}⟶ℂ\to {norm}_{\mathrm{fn}}\left(T\right)=sup\left(\left\{m|\exists x\in \mathscr{H}\left({norm}_{ℎ}\left(x\right)\le 1\wedge m=\left|T\left(x\right)\right|\right)\right\},{ℝ}^{*},<\right)$$
23	12 22	ax-mp	$$⊢{norm}_{\mathrm{fn}}\left(T\right)=sup\left(\left\{m|\exists x\in \mathscr{H}\left({norm}_{ℎ}\left(x\right)\le 1\wedge m=\left|T\left(x\right)\right|\right)\right\},{ℝ}^{*},<\right)$$
24	12	ffvelrni	$$⊢x\in \mathscr{H}\to T\left(x\right)\in ℂ$$
25	24	abscld	$$⊢x\in \mathscr{H}\to \left|T\left(x\right)\right|\in ℝ$$
26	10	fveq2i	$$⊢\left|T\left(0_{ℎ}\right)\right|=\left|0\right|$$
27		abs0	$$⊢\left|0\right|=0$$
28	26 27	eqtri	$$⊢\left|T\left(0_{ℎ}\right)\right|=0$$
29		rpcn	$$⊢\frac{y}{2}\in {ℝ}^{+}\to \frac{y}{2}\in ℂ$$
30	1	lnfnmuli	$$⊢\left(\frac{y}{2}\in ℂ\wedge x\in \mathscr{H}\right)\to T\left(\left(\frac{y}{2}\right){\cdot }_{ℎ}x\right)=\left(\frac{y}{2}\right)T\left(x\right)$$
31	29 30	sylan	$$⊢\left(\frac{y}{2}\in {ℝ}^{+}\wedge x\in \mathscr{H}\right)\to T\left(\left(\frac{y}{2}\right){\cdot }_{ℎ}x\right)=\left(\frac{y}{2}\right)T\left(x\right)$$
32	31	fveq2d	$$⊢\left(\frac{y}{2}\in {ℝ}^{+}\wedge x\in \mathscr{H}\right)\to \left|T\left(\left(\frac{y}{2}\right){\cdot }_{ℎ}x\right)\right|=\left|\left(\frac{y}{2}\right)T\left(x\right)\right|$$
33		absmul	$$⊢\left(\frac{y}{2}\in ℂ\wedge T\left(x\right)\in ℂ\right)\to \left|\left(\frac{y}{2}\right)T\left(x\right)\right|=\left|\frac{y}{2}\right|\left|T\left(x\right)\right|$$
34	29 24 33	syl2an	$$⊢\left(\frac{y}{2}\in {ℝ}^{+}\wedge x\in \mathscr{H}\right)\to \left|\left(\frac{y}{2}\right)T\left(x\right)\right|=\left|\frac{y}{2}\right|\left|T\left(x\right)\right|$$
35		rpre	$$⊢\frac{y}{2}\in {ℝ}^{+}\to \frac{y}{2}\in ℝ$$
36		rpge0	$$⊢\frac{y}{2}\in {ℝ}^{+}\to 0\le \frac{y}{2}$$
37	35 36	absidd	$$⊢\frac{y}{2}\in {ℝ}^{+}\to \left|\frac{y}{2}\right|=\frac{y}{2}$$
38	37	adantr	$$⊢\left(\frac{y}{2}\in {ℝ}^{+}\wedge x\in \mathscr{H}\right)\to \left|\frac{y}{2}\right|=\frac{y}{2}$$
39	38	oveq1d	$$⊢\left(\frac{y}{2}\in {ℝ}^{+}\wedge x\in \mathscr{H}\right)\to \left|\frac{y}{2}\right|\left|T\left(x\right)\right|=\left(\frac{y}{2}\right)\left|T\left(x\right)\right|$$
40	32 34 39	3eqtrrd	$$⊢\left(\frac{y}{2}\in {ℝ}^{+}\wedge x\in \mathscr{H}\right)\to \left(\frac{y}{2}\right)\left|T\left(x\right)\right|=\left|T\left(\left(\frac{y}{2}\right){\cdot }_{ℎ}x\right)\right|$$
41	21 23 25 28 40	nmcexi	$$⊢{norm}_{\mathrm{fn}}\left(T\right)\in ℝ$$