Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  bdopcoi Structured version   Visualization version   GIF version

Theorem bdopcoi 29885
 Description: The composition of two bounded linear operators is bounded. (Contributed by NM, 9-Mar-2006.) (New usage is discouraged.)
Hypotheses
Ref Expression
nmoptri.1 𝑆 ∈ BndLinOp
nmoptri.2 𝑇 ∈ BndLinOp
Assertion
Ref Expression
bdopcoi (𝑆𝑇) ∈ BndLinOp

Proof of Theorem bdopcoi
StepHypRef Expression
1 nmoptri.1 . . . 4 𝑆 ∈ BndLinOp
2 bdopln 29648 . . . 4 (𝑆 ∈ BndLinOp → 𝑆 ∈ LinOp)
31, 2ax-mp 5 . . 3 𝑆 ∈ LinOp
4 nmoptri.2 . . . 4 𝑇 ∈ BndLinOp
5 bdopln 29648 . . . 4 (𝑇 ∈ BndLinOp → 𝑇 ∈ LinOp)
64, 5ax-mp 5 . . 3 𝑇 ∈ LinOp
73, 6lnopcoi 29790 . 2 (𝑆𝑇) ∈ LinOp
83lnopfi 29756 . . . . 5 𝑆: ℋ⟶ ℋ
96lnopfi 29756 . . . . 5 𝑇: ℋ⟶ ℋ
108, 9hocofi 29553 . . . 4 (𝑆𝑇): ℋ⟶ ℋ
11 nmopxr 29653 . . . 4 ((𝑆𝑇): ℋ⟶ ℋ → (normop‘(𝑆𝑇)) ∈ ℝ*)
1210, 11ax-mp 5 . . 3 (normop‘(𝑆𝑇)) ∈ ℝ*
13 nmopre 29657 . . . . 5 (𝑆 ∈ BndLinOp → (normop𝑆) ∈ ℝ)
141, 13ax-mp 5 . . . 4 (normop𝑆) ∈ ℝ
15 nmopre 29657 . . . . 5 (𝑇 ∈ BndLinOp → (normop𝑇) ∈ ℝ)
164, 15ax-mp 5 . . . 4 (normop𝑇) ∈ ℝ
1714, 16remulcli 10650 . . 3 ((normop𝑆) · (normop𝑇)) ∈ ℝ
18 nmopgtmnf 29655 . . . 4 ((𝑆𝑇): ℋ⟶ ℋ → -∞ < (normop‘(𝑆𝑇)))
1910, 18ax-mp 5 . . 3 -∞ < (normop‘(𝑆𝑇))
201, 4nmopcoi 29882 . . 3 (normop‘(𝑆𝑇)) ≤ ((normop𝑆) · (normop𝑇))
21 xrre 12554 . . 3 ((((normop‘(𝑆𝑇)) ∈ ℝ* ∧ ((normop𝑆) · (normop𝑇)) ∈ ℝ) ∧ (-∞ < (normop‘(𝑆𝑇)) ∧ (normop‘(𝑆𝑇)) ≤ ((normop𝑆) · (normop𝑇)))) → (normop‘(𝑆𝑇)) ∈ ℝ)
2212, 17, 19, 20, 21mp4an 692 . 2 (normop‘(𝑆𝑇)) ∈ ℝ
23 elbdop2 29658 . 2 ((𝑆𝑇) ∈ BndLinOp ↔ ((𝑆𝑇) ∈ LinOp ∧ (normop‘(𝑆𝑇)) ∈ ℝ))
247, 22, 23mpbir2an 710 1 (𝑆𝑇) ∈ BndLinOp