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 SBndLinOp
nmoptri.2 TBndLinOp
Assertion bdopcoi STBndLinOp

Proof

Step Hyp Ref Expression
1 nmoptri.1 SBndLinOp
2 nmoptri.2 TBndLinOp
3 bdopln SBndLinOpSLinOp
4 1 3 ax-mp SLinOp
5 bdopln TBndLinOpTLinOp
6 2 5 ax-mp TLinOp
7 4 6 lnopcoi STLinOp
8 4 lnopfi S:
9 6 lnopfi T:
10 8 9 hocofi ST:
11 nmopxr ST:normopST*
12 10 11 ax-mp normopST*
13 nmopre SBndLinOpnormopS
14 1 13 ax-mp normopS
15 nmopre TBndLinOpnormopT
16 2 15 ax-mp normopT
17 14 16 remulcli normopSnormopT
18 nmopgtmnf ST:−∞<normopST
19 10 18 ax-mp −∞<normopST
20 1 2 nmopcoi normopSTnormopSnormopT
21 xrre normopST*normopSnormopT−∞<normopSTnormopSTnormopSnormopTnormopST
22 12 17 19 20 21 mp4an normopST
23 elbdop2 STBndLinOpSTLinOpnormopST
24 7 22 23 mpbir2an STBndLinOp