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