# Metamath Proof Explorer

## Theorem bdopcoi

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

Ref Expression
Hypotheses nmoptri.1 𝑆 ∈ BndLinOp
nmoptri.2 𝑇 ∈ BndLinOp
Assertion bdopcoi ( 𝑆𝑇 ) ∈ 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 lnopcoi ( 𝑆𝑇 ) ∈ LinOp
8 4 lnopfi 𝑆 : ℋ ⟶ ℋ
9 6 lnopfi 𝑇 : ℋ ⟶ ℋ
10 8 9 hocofi ( 𝑆𝑇 ) : ℋ ⟶ ℋ
11 nmopxr ( ( 𝑆𝑇 ) : ℋ ⟶ ℋ → ( normop ‘ ( 𝑆𝑇 ) ) ∈ ℝ* )
12 10 11 ax-mp ( normop ‘ ( 𝑆𝑇 ) ) ∈ ℝ*
13 nmopre ( 𝑆 ∈ BndLinOp → ( normop𝑆 ) ∈ ℝ )
14 1 13 ax-mp ( normop𝑆 ) ∈ ℝ
15 nmopre ( 𝑇 ∈ BndLinOp → ( normop𝑇 ) ∈ ℝ )
16 2 15 ax-mp ( normop𝑇 ) ∈ ℝ
17 14 16 remulcli ( ( normop𝑆 ) · ( normop𝑇 ) ) ∈ ℝ
18 nmopgtmnf ( ( 𝑆𝑇 ) : ℋ ⟶ ℋ → -∞ < ( normop ‘ ( 𝑆𝑇 ) ) )
19 10 18 ax-mp -∞ < ( normop ‘ ( 𝑆𝑇 ) )
20 1 2 nmopcoi ( normop ‘ ( 𝑆𝑇 ) ) ≤ ( ( normop𝑆 ) · ( normop𝑇 ) )
21 xrre ( ( ( ( normop ‘ ( 𝑆𝑇 ) ) ∈ ℝ* ∧ ( ( normop𝑆 ) · ( normop𝑇 ) ) ∈ ℝ ) ∧ ( -∞ < ( normop ‘ ( 𝑆𝑇 ) ) ∧ ( normop ‘ ( 𝑆𝑇 ) ) ≤ ( ( normop𝑆 ) · ( normop𝑇 ) ) ) ) → ( normop ‘ ( 𝑆𝑇 ) ) ∈ ℝ )
22 12 17 19 20 21 mp4an ( normop ‘ ( 𝑆𝑇 ) ) ∈ ℝ
23 elbdop2 ( ( 𝑆𝑇 ) ∈ BndLinOp ↔ ( ( 𝑆𝑇 ) ∈ LinOp ∧ ( normop ‘ ( 𝑆𝑇 ) ) ∈ ℝ ) )
24 7 22 23 mpbir2an ( 𝑆𝑇 ) ∈ BndLinOp