# 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`