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	⊢ 𝑆 ∈ BndLinOp
	nmoptri.2	⊢ 𝑇 ∈ BndLinOp
Assertion	bdophdi	⊢ ( 𝑆 −op 𝑇 ) ∈ BndLinOp

Proof

Step	Hyp	Ref	Expression
1		nmoptri.1	⊢ 𝑆 ∈ BndLinOp
2		nmoptri.2	⊢ 𝑇 ∈ BndLinOp
3		bdopf	⊢ ( 𝑆 ∈ BndLinOp → 𝑆 : ℋ ⟶ ℋ )
4	1 3	ax-mp	⊢ 𝑆 : ℋ ⟶ ℋ
5		bdopf	⊢ ( 𝑇 ∈ BndLinOp → 𝑇 : ℋ ⟶ ℋ )
6	2 5	ax-mp	⊢ 𝑇 : ℋ ⟶ ℋ
7	4 6	honegsubi	⊢ ( 𝑆 +op ( - 1 ·op 𝑇 ) ) = ( 𝑆 −op 𝑇 )
8		neg1cn	⊢ - 1 ∈ ℂ
9	2	bdophmi	⊢ ( - 1 ∈ ℂ → ( - 1 ·op 𝑇 ) ∈ BndLinOp )
10	8 9	ax-mp	⊢ ( - 1 ·op 𝑇 ) ∈ BndLinOp
11	1 10	bdophsi	⊢ ( 𝑆 +op ( - 1 ·op 𝑇 ) ) ∈ BndLinOp
12	7 11	eqeltrri	⊢ ( 𝑆 −op 𝑇 ) ∈ BndLinOp