Theorem bdophdi

Description: The difference between two bounded linear operators is bounded. (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	bdophdi	$$⊢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		bdopf	$$⊢S\in \mathrm{BndLinOp}\to S:\mathscr{H}⟶\mathscr{H}$$
4	1 3	ax-mp	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
5		bdopf	$$⊢T\in \mathrm{BndLinOp}\to T:\mathscr{H}⟶\mathscr{H}$$
6	2 5	ax-mp	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
7	4 6	honegsubi	$$⊢S{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)=S{-}_{\mathrm{op}}T$$
8		neg1cn	$$⊢-1\in ℂ$$
9	2	bdophmi	$$⊢-1\in ℂ\to -1{·}_{\mathrm{op}}T\in \mathrm{BndLinOp}$$
10	8 9	ax-mp	$$⊢-1{·}_{\mathrm{op}}T\in \mathrm{BndLinOp}$$
11	1 10	bdophsi	$$⊢S{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}T\right)\in \mathrm{BndLinOp}$$
12	7 11	eqeltrri	$$⊢S{-}_{\mathrm{op}}T\in \mathrm{BndLinOp}$$