Theorem bdophsi

Description: The sum of two bounded linear operators is a bounded linear operator. (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	bdophsi	$$⊢S{+}_{\mathrm{op}}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	lnophsi	$$⊢S{+}_{\mathrm{op}}T\in \mathrm{LinOp}$$
8		bdopf	$$⊢S\in \mathrm{BndLinOp}\to S:\mathscr{H}⟶\mathscr{H}$$
9	1 8	ax-mp	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
10		bdopf	$$⊢T\in \mathrm{BndLinOp}\to T:\mathscr{H}⟶\mathscr{H}$$
11	2 10	ax-mp	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
12	9 11	hoaddcli	$$⊢\left(S{+}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$
13		nmopxr	$$⊢\left(S{+}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}\to {norm}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)\in {ℝ}^{*}$$
14	12 13	ax-mp	$$⊢{norm}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)\in {ℝ}^{*}$$
15		nmopre	$$⊢S\in \mathrm{BndLinOp}\to {norm}_{\mathrm{op}}\left(S\right)\in ℝ$$
16	1 15	ax-mp	$$⊢{norm}_{\mathrm{op}}\left(S\right)\in ℝ$$
17		nmopre	$$⊢T\in \mathrm{BndLinOp}\to {norm}_{\mathrm{op}}\left(T\right)\in ℝ$$
18	2 17	ax-mp	$$⊢{norm}_{\mathrm{op}}\left(T\right)\in ℝ$$
19	16 18	readdcli	$$⊢{norm}_{\mathrm{op}}\left(S\right)+{norm}_{\mathrm{op}}\left(T\right)\in ℝ$$
20		nmopgtmnf	$$⊢\left(S{+}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}\to \mathrm{-\infty }<{norm}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)$$
21	12 20	ax-mp	$$⊢\mathrm{-\infty }<{norm}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)$$
22	1 2	nmoptrii	$$⊢{norm}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)\le {norm}_{\mathrm{op}}\left(S\right)+{norm}_{\mathrm{op}}\left(T\right)$$
23		xrre	$$⊢\left(\left({norm}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}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{+}_{\mathrm{op}}T\right)\wedge {norm}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)\le {norm}_{\mathrm{op}}\left(S\right)+{norm}_{\mathrm{op}}\left(T\right)\right)\right)\to {norm}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)\in ℝ$$
24	14 19 21 22 23	mp4an	$$⊢{norm}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)\in ℝ$$
25		elbdop2	$$⊢S{+}_{\mathrm{op}}T\in \mathrm{BndLinOp}\leftrightarrow \left(S{+}_{\mathrm{op}}T\in \mathrm{LinOp}\wedge {norm}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)\in ℝ\right)$$
26	7 24 25	mpbir2an	$$⊢S{+}_{\mathrm{op}}T\in \mathrm{BndLinOp}$$