# 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 𝑆 ∈ BndLinOp
nmoptri.2 𝑇 ∈ BndLinOp
Assertion bdophsi ( 𝑆 +op 𝑇 ) ∈ BndLinOp

### Proof

Step Hyp Ref Expression
1 nmoptri.1 𝑆 ∈ BndLinOp
2 nmoptri.2 𝑇 ∈ BndLinOp
3 bdopln ( 𝑆 ∈ BndLinOp → 𝑆 ∈ LinOp )
4 1 3 ax-mp 𝑆 ∈ LinOp
5 bdopln ( 𝑇 ∈ BndLinOp → 𝑇 ∈ LinOp )
6 2 5 ax-mp 𝑇 ∈ LinOp
7 4 6 lnophsi ( 𝑆 +op 𝑇 ) ∈ LinOp
8 bdopf ( 𝑆 ∈ BndLinOp → 𝑆 : ℋ ⟶ ℋ )
9 1 8 ax-mp 𝑆 : ℋ ⟶ ℋ
10 bdopf ( 𝑇 ∈ BndLinOp → 𝑇 : ℋ ⟶ ℋ )
11 2 10 ax-mp 𝑇 : ℋ ⟶ ℋ
12 9 11 hoaddcli ( 𝑆 +op 𝑇 ) : ℋ ⟶ ℋ
13 nmopxr ( ( 𝑆 +op 𝑇 ) : ℋ ⟶ ℋ → ( normop ‘ ( 𝑆 +op 𝑇 ) ) ∈ ℝ* )
14 12 13 ax-mp ( normop ‘ ( 𝑆 +op 𝑇 ) ) ∈ ℝ*
15 nmopre ( 𝑆 ∈ BndLinOp → ( normop𝑆 ) ∈ ℝ )
16 1 15 ax-mp ( normop𝑆 ) ∈ ℝ
17 nmopre ( 𝑇 ∈ BndLinOp → ( normop𝑇 ) ∈ ℝ )
18 2 17 ax-mp ( normop𝑇 ) ∈ ℝ
19 16 18 readdcli ( ( normop𝑆 ) + ( normop𝑇 ) ) ∈ ℝ
20 nmopgtmnf ( ( 𝑆 +op 𝑇 ) : ℋ ⟶ ℋ → -∞ < ( normop ‘ ( 𝑆 +op 𝑇 ) ) )
21 12 20 ax-mp -∞ < ( normop ‘ ( 𝑆 +op 𝑇 ) )
22 1 2 nmoptrii ( normop ‘ ( 𝑆 +op 𝑇 ) ) ≤ ( ( normop𝑆 ) + ( normop𝑇 ) )
23 xrre ( ( ( ( normop ‘ ( 𝑆 +op 𝑇 ) ) ∈ ℝ* ∧ ( ( normop𝑆 ) + ( normop𝑇 ) ) ∈ ℝ ) ∧ ( -∞ < ( normop ‘ ( 𝑆 +op 𝑇 ) ) ∧ ( normop ‘ ( 𝑆 +op 𝑇 ) ) ≤ ( ( normop𝑆 ) + ( normop𝑇 ) ) ) ) → ( normop ‘ ( 𝑆 +op 𝑇 ) ) ∈ ℝ )
24 14 19 21 22 23 mp4an ( normop ‘ ( 𝑆 +op 𝑇 ) ) ∈ ℝ
25 elbdop2 ( ( 𝑆 +op 𝑇 ) ∈ BndLinOp ↔ ( ( 𝑆 +op 𝑇 ) ∈ LinOp ∧ ( normop ‘ ( 𝑆 +op 𝑇 ) ) ∈ ℝ ) )
26 7 24 25 mpbir2an ( 𝑆 +op 𝑇 ) ∈ BndLinOp