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