Theorem bdopcoi

Description: The composition of two bounded linear operators is bounded. (Contributed by NM, 9-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmoptri.1	$$⊢S\in \mathrm{BndLinOp}$$
	nmoptri.2	$$⊢T\in \mathrm{BndLinOp}$$
Assertion	bdopcoi	$$⊢S\circ T\in \mathrm{BndLinOp}$$

Proof

Step	Hyp	Ref	Expression
1		nmoptri.1	$$⊢S\in \mathrm{BndLinOp}$$
2		nmoptri.2	$$⊢T\in \mathrm{BndLinOp}$$
3		bdopln	$$⊢S\in \mathrm{BndLinOp}\to S\in \mathrm{LinOp}$$
4	1 3	ax-mp	$$⊢S\in \mathrm{LinOp}$$
5		bdopln	$$⊢T\in \mathrm{BndLinOp}\to T\in \mathrm{LinOp}$$
6	2 5	ax-mp	$$⊢T\in \mathrm{LinOp}$$
7	4 6	lnopcoi	$$⊢S\circ T\in \mathrm{LinOp}$$
8	4	lnopfi	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
9	6	lnopfi	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
10	8 9	hocofi	$$⊢\left(S\circ T\right):\mathscr{H}⟶\mathscr{H}$$
11		nmopxr	$$⊢\left(S\circ T\right):\mathscr{H}⟶\mathscr{H}\to {norm}_{\mathrm{op}}\left(S\circ T\right)\in {ℝ}^{*}$$
12	10 11	ax-mp	$$⊢{norm}_{\mathrm{op}}\left(S\circ T\right)\in {ℝ}^{*}$$
13		nmopre	$$⊢S\in \mathrm{BndLinOp}\to {norm}_{\mathrm{op}}\left(S\right)\in ℝ$$
14	1 13	ax-mp	$$⊢{norm}_{\mathrm{op}}\left(S\right)\in ℝ$$
15		nmopre	$$⊢T\in \mathrm{BndLinOp}\to {norm}_{\mathrm{op}}\left(T\right)\in ℝ$$
16	2 15	ax-mp	$$⊢{norm}_{\mathrm{op}}\left(T\right)\in ℝ$$
17	14 16	remulcli	$$⊢{norm}_{\mathrm{op}}\left(S\right){norm}_{\mathrm{op}}\left(T\right)\in ℝ$$
18		nmopgtmnf	$$⊢\left(S\circ T\right):\mathscr{H}⟶\mathscr{H}\to \mathrm{-\infty }<{norm}_{\mathrm{op}}\left(S\circ T\right)$$
19	10 18	ax-mp	$$⊢\mathrm{-\infty }<{norm}_{\mathrm{op}}\left(S\circ T\right)$$
20	1 2	nmopcoi	$$⊢{norm}_{\mathrm{op}}\left(S\circ T\right)\le {norm}_{\mathrm{op}}\left(S\right){norm}_{\mathrm{op}}\left(T\right)$$
21		xrre	$$⊢\left(\left({norm}_{\mathrm{op}}\left(S\circ T\right)\in {ℝ}^{*}\wedge {norm}_{\mathrm{op}}\left(S\right){norm}_{\mathrm{op}}\left(T\right)\in ℝ\right)\wedge \left(\mathrm{-\infty }<{norm}_{\mathrm{op}}\left(S\circ T\right)\wedge {norm}_{\mathrm{op}}\left(S\circ T\right)\le {norm}_{\mathrm{op}}\left(S\right){norm}_{\mathrm{op}}\left(T\right)\right)\right)\to {norm}_{\mathrm{op}}\left(S\circ T\right)\in ℝ$$
22	12 17 19 20 21	mp4an	$$⊢{norm}_{\mathrm{op}}\left(S\circ T\right)\in ℝ$$
23		elbdop2	$$⊢S\circ T\in \mathrm{BndLinOp}\leftrightarrow \left(S\circ T\in \mathrm{LinOp}\wedge {norm}_{\mathrm{op}}\left(S\circ T\right)\in ℝ\right)$$
24	7 22 23	mpbir2an	$$⊢S\circ T\in \mathrm{BndLinOp}$$