This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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