Theorem nmop0

Description: The norm of the zero operator is zero. (Contributed by NM, 8-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nmop0	$$⊢{norm}_{\mathrm{op}}\left(0_{\mathrm{hop}}\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		ho0f	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}$$
2		nmopval	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}\to {norm}_{\mathrm{op}}\left(0_{\mathrm{hop}}\right)=sup\left(\left\{x|\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left(0_{\mathrm{hop}}\left(y\right)\right)\right)\right\},{ℝ}^{*},<\right)$$
3	1 2	ax-mp	$$⊢{norm}_{\mathrm{op}}\left(0_{\mathrm{hop}}\right)=sup\left(\left\{x|\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left(0_{\mathrm{hop}}\left(y\right)\right)\right)\right\},{ℝ}^{*},<\right)$$
4		ho0val	$$⊢y\in \mathscr{H}\to 0_{\mathrm{hop}}\left(y\right)=0_{ℎ}$$
5	4	fveq2d	$$⊢y\in \mathscr{H}\to {norm}_{ℎ}\left(0_{\mathrm{hop}}\left(y\right)\right)={norm}_{ℎ}\left(0_{ℎ}\right)$$
6		norm0	$$⊢{norm}_{ℎ}\left(0_{ℎ}\right)=0$$
7	5 6	eqtrdi	$$⊢y\in \mathscr{H}\to {norm}_{ℎ}\left(0_{\mathrm{hop}}\left(y\right)\right)=0$$
8	7	eqeq2d	$$⊢y\in \mathscr{H}\to \left(x={norm}_{ℎ}\left(0_{\mathrm{hop}}\left(y\right)\right)\leftrightarrow x=0\right)$$
9	8	anbi2d	$$⊢y\in \mathscr{H}\to \left(\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left(0_{\mathrm{hop}}\left(y\right)\right)\right)\leftrightarrow \left({norm}_{ℎ}\left(y\right)\le 1\wedge x=0\right)\right)$$
10	9	rexbiia	$$⊢\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left(0_{\mathrm{hop}}\left(y\right)\right)\right)\leftrightarrow \exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x=0\right)$$
11		ax-hv0cl	$$⊢0_{ℎ}\in \mathscr{H}$$
12		0le1	$$⊢0\le 1$$
13		fveq2	$$⊢y=0_{ℎ}\to {norm}_{ℎ}\left(y\right)={norm}_{ℎ}\left(0_{ℎ}\right)$$
14	13 6	eqtrdi	$$⊢y=0_{ℎ}\to {norm}_{ℎ}\left(y\right)=0$$
15	14	breq1d	$$⊢y=0_{ℎ}\to \left({norm}_{ℎ}\left(y\right)\le 1\leftrightarrow 0\le 1\right)$$
16	15	rspcev	$$⊢\left(0_{ℎ}\in \mathscr{H}\wedge 0\le 1\right)\to \exists y\in \mathscr{H}{norm}_{ℎ}\left(y\right)\le 1$$
17	11 12 16	mp2an	$$⊢\exists y\in \mathscr{H}{norm}_{ℎ}\left(y\right)\le 1$$
18		r19.41v	$$⊢\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x=0\right)\leftrightarrow \left(\exists y\in \mathscr{H}{norm}_{ℎ}\left(y\right)\le 1\wedge x=0\right)$$
19	17 18	mpbiran	$$⊢\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x=0\right)\leftrightarrow x=0$$
20	10 19	bitri	$$⊢\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left(0_{\mathrm{hop}}\left(y\right)\right)\right)\leftrightarrow x=0$$
21	20	abbii	$$⊢\left\{x|\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left(0_{\mathrm{hop}}\left(y\right)\right)\right)\right\}=\left\{x|x=0\right\}$$
22		df-sn	$$⊢\left\{0\right\}=\left\{x|x=0\right\}$$
23	21 22	eqtr4i	$$⊢\left\{x|\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left(0_{\mathrm{hop}}\left(y\right)\right)\right)\right\}=\left\{0\right\}$$
24	23	supeq1i	$$⊢sup\left(\left\{x|\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left(0_{\mathrm{hop}}\left(y\right)\right)\right)\right\},{ℝ}^{*},<\right)=sup\left(\left\{0\right\},{ℝ}^{*},<\right)$$
25		xrltso	$$⊢<\mathrm{Or}{ℝ}^{*}$$
26		0xr	$$⊢0\in {ℝ}^{*}$$
27		supsn	$$⊢\left(<\mathrm{Or}{ℝ}^{*}\wedge 0\in {ℝ}^{*}\right)\to sup\left(\left\{0\right\},{ℝ}^{*},<\right)=0$$
28	25 26 27	mp2an	$$⊢sup\left(\left\{0\right\},{ℝ}^{*},<\right)=0$$
29	3 24 28	3eqtri	$$⊢{norm}_{\mathrm{op}}\left(0_{\mathrm{hop}}\right)=0$$