# 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