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 e. BndLinOp
	nmoptri.2	|- T e. BndLinOp
Assertion	bdophdi	|- ( S -op T ) e. BndLinOp

Proof

Step	Hyp	Ref	Expression
1		nmoptri.1	|- S e. BndLinOp
2		nmoptri.2	|- T e. BndLinOp
3		bdopf	|- ( S e. BndLinOp -> S : ~H --> ~H )
4	1 3	ax-mp	|- S : ~H --> ~H
5		bdopf	|- ( T e. BndLinOp -> T : ~H --> ~H )
6	2 5	ax-mp	|- T : ~H --> ~H
7	4 6	honegsubi	|- ( S +op ( -u 1 .op T ) ) = ( S -op T )
8		neg1cn	|- -u 1 e. CC
9	2	bdophmi	|- ( -u 1 e. CC -> ( -u 1 .op T ) e. BndLinOp )
10	8 9	ax-mp	|- ( -u 1 .op T ) e. BndLinOp
11	1 10	bdophsi	|- ( S +op ( -u 1 .op T ) ) e. BndLinOp
12	7 11	eqeltrri	|- ( S -op T ) e. BndLinOp