Theorem nmoptri2i

Description: Triangle-type inequality for the norms of bounded linear operators. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmoptri.1	$$⊢S\in \mathrm{BndLinOp}$$
	nmoptri.2	$$⊢T\in \mathrm{BndLinOp}$$
Assertion	nmoptri2i	$$⊢{norm}_{\mathrm{op}}\left(S\right)-{norm}_{\mathrm{op}}\left(T\right)\le {norm}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)$$

Proof

Step	Hyp	Ref	Expression
1		nmoptri.1	$$⊢S\in \mathrm{BndLinOp}$$
2		nmoptri.2	$$⊢T\in \mathrm{BndLinOp}$$
3	1 2	bdophsi	$$⊢S{+}_{\mathrm{op}}T\in \mathrm{BndLinOp}$$
4		neg1cn	$$⊢-1\in ℂ$$
5	2	bdophmi	$$⊢-1\in ℂ\to -1{·}_{\mathrm{op}}T\in \mathrm{BndLinOp}$$
6	4 5	ax-mp	$$⊢-1{·}_{\mathrm{op}}T\in \mathrm{BndLinOp}$$
7	3 6	nmoptrii	$$⊢{norm}_{\mathrm{op}}\left(\left(S{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)\right)\le {norm}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)+{norm}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)$$
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	12 11	honegsubi	$$⊢\left(S{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)=\left(S{+}_{\mathrm{op}}T\right){-}_{\mathrm{op}}T$$
14	9 11	hopncani	$$⊢\left(S{+}_{\mathrm{op}}T\right){-}_{\mathrm{op}}T=S$$
15	13 14	eqtri	$$⊢\left(S{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)=S$$
16	15	fveq2i	$$⊢{norm}_{\mathrm{op}}\left(\left(S{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)\right)={norm}_{\mathrm{op}}\left(S\right)$$
17	11	nmopnegi	$$⊢{norm}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)={norm}_{\mathrm{op}}\left(T\right)$$
18	17	oveq2i	$$⊢{norm}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)+{norm}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)={norm}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)+{norm}_{\mathrm{op}}\left(T\right)$$
19	7 16 18	3brtr3i	$$⊢{norm}_{\mathrm{op}}\left(S\right)\le {norm}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)+{norm}_{\mathrm{op}}\left(T\right)$$
20		nmopre	$$⊢S\in \mathrm{BndLinOp}\to {norm}_{\mathrm{op}}\left(S\right)\in ℝ$$
21	1 20	ax-mp	$$⊢{norm}_{\mathrm{op}}\left(S\right)\in ℝ$$
22		nmopre	$$⊢T\in \mathrm{BndLinOp}\to {norm}_{\mathrm{op}}\left(T\right)\in ℝ$$
23	2 22	ax-mp	$$⊢{norm}_{\mathrm{op}}\left(T\right)\in ℝ$$
24		nmopre	$$⊢S{+}_{\mathrm{op}}T\in \mathrm{BndLinOp}\to {norm}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)\in ℝ$$
25	3 24	ax-mp	$$⊢{norm}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)\in ℝ$$
26	21 23 25	lesubaddi	$$⊢{norm}_{\mathrm{op}}\left(S\right)-{norm}_{\mathrm{op}}\left(T\right)\le {norm}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)\leftrightarrow {norm}_{\mathrm{op}}\left(S\right)\le {norm}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)+{norm}_{\mathrm{op}}\left(T\right)$$
27	19 26	mpbir	$$⊢{norm}_{\mathrm{op}}\left(S\right)-{norm}_{\mathrm{op}}\left(T\right)\le {norm}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)$$