Metamath Proof Explorer

Theorem bdophsi

Description: The sum of two bounded linear operators is a bounded linear operator. (Contributed by NM, 9-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nmoptri.1 
|- S e. BndLinOp
nmoptri.2 
|- T e. BndLinOp
Assertion bdophsi 
|- ( S +op T ) e. BndLinOp

Proof

Step Hyp Ref Expression
1 nmoptri.1 
 |-  S e. BndLinOp
2 nmoptri.2 
 |-  T e. BndLinOp
3 bdopln 
 |-  ( S e. BndLinOp -> S e. LinOp )
4 1 3 ax-mp 
 |-  S e. LinOp
5 bdopln 
 |-  ( T e. BndLinOp -> T e. LinOp )
6 2 5 ax-mp 
 |-  T e. LinOp
7 4 6 lnophsi 
 |-  ( S +op T ) e. LinOp
8 bdopf 
 |-  ( S e. BndLinOp -> S : ~H --> ~H )
9 1 8 ax-mp 
 |-  S : ~H --> ~H
10 bdopf 
 |-  ( T e. BndLinOp -> T : ~H --> ~H )
11 2 10 ax-mp 
 |-  T : ~H --> ~H
12 9 11 hoaddcli 
 |-  ( S +op T ) : ~H --> ~H
13 nmopxr 
 |-  ( ( S +op T ) : ~H --> ~H -> ( normop ` ( S +op T ) ) e. RR* )
14 12 13 ax-mp 
 |-  ( normop ` ( S +op T ) ) e. RR*
15 nmopre 
 |-  ( S e. BndLinOp -> ( normop ` S ) e. RR )
16 1 15 ax-mp 
 |-  ( normop ` S ) e. RR
17 nmopre 
 |-  ( T e. BndLinOp -> ( normop ` T ) e. RR )
18 2 17 ax-mp 
 |-  ( normop ` T ) e. RR
19 16 18 readdcli 
 |-  ( ( normop ` S ) + ( normop ` T ) ) e. RR
20 nmopgtmnf 
 |-  ( ( S +op T ) : ~H --> ~H -> -oo < ( normop ` ( S +op T ) ) )
21 12 20 ax-mp 
 |-  -oo < ( normop ` ( S +op T ) )
22 1 2 nmoptrii 
 |-  ( normop ` ( S +op T ) ) <_ ( ( normop ` S ) + ( normop ` T ) )
23 xrre 
 |-  ( ( ( ( normop ` ( S +op T ) ) e. RR* /\ ( ( normop ` S ) + ( normop ` T ) ) e. RR ) /\ ( -oo < ( normop ` ( S +op T ) ) /\ ( normop ` ( S +op T ) ) <_ ( ( normop ` S ) + ( normop ` T ) ) ) ) -> ( normop ` ( S +op T ) ) e. RR )
24 14 19 21 22 23 mp4an 
 |-  ( normop ` ( S +op T ) ) e. RR
25 elbdop2 
 |-  ( ( S +op T ) e. BndLinOp <-> ( ( S +op T ) e. LinOp /\ ( normop ` ( S +op T ) ) e. RR ) )
26 7 24 25 mpbir2an 
 |-  ( S +op T ) e. BndLinOp