Theorem unopbd

Description: A unitary operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	unopbd	$$⊢T\in \mathrm{UniOp}\to T\in \mathrm{BndLinOp}$$

Proof

Step	Hyp	Ref	Expression
1		unoplin	$$⊢T\in \mathrm{UniOp}\to T\in \mathrm{LinOp}$$
2		unopf1o	$$⊢T\in \mathrm{UniOp}\to T:\mathscr{H}\underset{1-1\; onto}{⟶}\mathscr{H}$$
3		f1of	$$⊢T:\mathscr{H}\underset{1-1\; onto}{⟶}\mathscr{H}\to T:\mathscr{H}⟶\mathscr{H}$$
4	2 3	syl	$$⊢T\in \mathrm{UniOp}\to T:\mathscr{H}⟶\mathscr{H}$$
5		nmop0h	$$⊢\left(\mathscr{H}=0_{\mathscr{H}}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to {norm}_{\mathrm{op}}\left(T\right)=0$$
6		0re	$$⊢0\in ℝ$$
7	5 6	eqeltrdi	$$⊢\left(\mathscr{H}=0_{\mathscr{H}}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to {norm}_{\mathrm{op}}\left(T\right)\in ℝ$$
8	4 7	sylan2	$$⊢\left(\mathscr{H}=0_{\mathscr{H}}\wedge T\in \mathrm{UniOp}\right)\to {norm}_{\mathrm{op}}\left(T\right)\in ℝ$$
9		df-ne	$$⊢\mathscr{H}\ne 0_{\mathscr{H}}\leftrightarrow \neg \mathscr{H}=0_{\mathscr{H}}$$
10		nmopun	$$⊢\left(\mathscr{H}\ne 0_{\mathscr{H}}\wedge T\in \mathrm{UniOp}\right)\to {norm}_{\mathrm{op}}\left(T\right)=1$$
11		1re	$$⊢1\in ℝ$$
12	10 11	eqeltrdi	$$⊢\left(\mathscr{H}\ne 0_{\mathscr{H}}\wedge T\in \mathrm{UniOp}\right)\to {norm}_{\mathrm{op}}\left(T\right)\in ℝ$$
13	9 12	sylanbr	$$⊢\left(\neg \mathscr{H}=0_{\mathscr{H}}\wedge T\in \mathrm{UniOp}\right)\to {norm}_{\mathrm{op}}\left(T\right)\in ℝ$$
14	8 13	pm2.61ian	$$⊢T\in \mathrm{UniOp}\to {norm}_{\mathrm{op}}\left(T\right)\in ℝ$$
15		elbdop2	$$⊢T\in \mathrm{BndLinOp}\leftrightarrow \left(T\in \mathrm{LinOp}\wedge {norm}_{\mathrm{op}}\left(T\right)\in ℝ\right)$$
16	1 14 15	sylanbrc	$$⊢T\in \mathrm{UniOp}\to T\in \mathrm{BndLinOp}$$