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 
|- S e. BndLinOp
nmoptri.2 
|- T e. BndLinOp
Assertion bdopcoi 
|- ( S o. T ) e. BndLinOp

Proof

Step Hyp Ref Expression
1 nmoptri.1 
 |-  S e. BndLinOp
2 nmoptri.2 
 |-  T e. BndLinOp
3 bdopln 
 |-  ( S e. BndLinOp -> S e. LinOp )
4 1 3 ax-mp 
 |-  S e. LinOp
5 bdopln 
 |-  ( T e. BndLinOp -> T e. LinOp )
6 2 5 ax-mp 
 |-  T e. LinOp
7 4 6 lnopcoi 
 |-  ( S o. T ) e. LinOp
8 4 lnopfi 
 |-  S : ~H --> ~H
9 6 lnopfi 
 |-  T : ~H --> ~H
10 8 9 hocofi 
 |-  ( S o. T ) : ~H --> ~H
11 nmopxr 
 |-  ( ( S o. T ) : ~H --> ~H -> ( normop ` ( S o. T ) ) e. RR* )
12 10 11 ax-mp 
 |-  ( normop ` ( S o. T ) ) e. RR*
13 nmopre 
 |-  ( S e. BndLinOp -> ( normop ` S ) e. RR )
14 1 13 ax-mp 
 |-  ( normop ` S ) e. RR
15 nmopre 
 |-  ( T e. BndLinOp -> ( normop ` T ) e. RR )
16 2 15 ax-mp 
 |-  ( normop ` T ) e. RR
17 14 16 remulcli 
 |-  ( ( normop ` S ) x. ( normop ` T ) ) e. RR
18 nmopgtmnf 
 |-  ( ( S o. T ) : ~H --> ~H -> -oo < ( normop ` ( S o. T ) ) )
19 10 18 ax-mp 
 |-  -oo < ( normop ` ( S o. T ) )
20 1 2 nmopcoi 
 |-  ( normop ` ( S o. T ) ) <_ ( ( normop ` S ) x. ( normop ` T ) )
21 xrre 
 |-  ( ( ( ( normop ` ( S o. T ) ) e. RR* /\ ( ( normop ` S ) x. ( normop ` T ) ) e. RR ) /\ ( -oo < ( normop ` ( S o. T ) ) /\ ( normop ` ( S o. T ) ) <_ ( ( normop ` S ) x. ( normop ` T ) ) ) ) -> ( normop ` ( S o. T ) ) e. RR )
22 12 17 19 20 21 mp4an 
 |-  ( normop ` ( S o. T ) ) e. RR
23 elbdop2 
 |-  ( ( S o. T ) e. BndLinOp <-> ( ( S o. T ) e. LinOp /\ ( normop ` ( S o. T ) ) e. RR ) )
24 7 22 23 mpbir2an 
 |-  ( S o. T ) e. BndLinOp