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

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