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