Theorem pjbdlni

Description: A projector is a bounded linear operator. (Contributed by NM, 3-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	pjhmop.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjbdlni	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{BndLinOp}$$

Proof

Step	Hyp	Ref	Expression
1		pjhmop.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2	1	pjlnopi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{LinOp}$$
3		2fveq3	$$⊢H=0_{\mathscr{H}}\to {norm}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\right)={norm}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(0_{\mathscr{H}}\right)\right)$$
4	3	eleq1d	$$⊢H=0_{\mathscr{H}}\to \left({norm}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\right)\in ℝ\leftrightarrow {norm}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(0_{\mathscr{H}}\right)\right)\in ℝ\right)$$
5	1	pjnmopi	$$⊢H\ne 0_{\mathscr{H}}\to {norm}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\right)=1$$
6		1re	$$⊢1\in ℝ$$
7	5 6	eqeltrdi	$$⊢H\ne 0_{\mathscr{H}}\to {norm}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\right)\in ℝ$$
8	7	adantl	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge H\ne 0_{\mathscr{H}}\right)\to {norm}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\right)\in ℝ$$
9		df-h0op	$$⊢0_{\mathrm{hop}}={\mathrm{proj}}_{ℎ}\left(0_{\mathscr{H}}\right)$$
10	9	fveq2i	$$⊢{norm}_{\mathrm{op}}\left(0_{\mathrm{hop}}\right)={norm}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(0_{\mathscr{H}}\right)\right)$$
11		nmop0	$$⊢{norm}_{\mathrm{op}}\left(0_{\mathrm{hop}}\right)=0$$
12	10 11	eqtr3i	$$⊢{norm}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(0_{\mathscr{H}}\right)\right)=0$$
13		0re	$$⊢0\in ℝ$$
14	12 13	eqeltri	$$⊢{norm}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(0_{\mathscr{H}}\right)\right)\in ℝ$$
15	14	a1i	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to {norm}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(0_{\mathscr{H}}\right)\right)\in ℝ$$
16	4 8 15	pm2.61ne	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to {norm}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\right)\in ℝ$$
17	1 16	ax-mp	$$⊢{norm}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\right)\in ℝ$$
18		elbdop2	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{BndLinOp}\leftrightarrow \left({\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{LinOp}\wedge {norm}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\right)\in ℝ\right)$$
19	2 17 18	mpbir2an	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{BndLinOp}$$