# Metamath Proof Explorer

## Theorem unopbd

Description: A unitary operator is a bounded linear operator. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion unopbd
`|- ( T e. UniOp -> T e. BndLinOp )`

### Proof

Step Hyp Ref Expression
1 unoplin
` |-  ( T e. UniOp -> T e. LinOp )`
2 unopf1o
` |-  ( T e. UniOp -> T : ~H -1-1-onto-> ~H )`
3 f1of
` |-  ( T : ~H -1-1-onto-> ~H -> T : ~H --> ~H )`
4 2 3 syl
` |-  ( T e. UniOp -> T : ~H --> ~H )`
5 nmop0h
` |-  ( ( ~H = 0H /\ T : ~H --> ~H ) -> ( normop ` T ) = 0 )`
6 0re
` |-  0 e. RR`
7 5 6 eqeltrdi
` |-  ( ( ~H = 0H /\ T : ~H --> ~H ) -> ( normop ` T ) e. RR )`
8 4 7 sylan2
` |-  ( ( ~H = 0H /\ T e. UniOp ) -> ( normop ` T ) e. RR )`
9 df-ne
` |-  ( ~H =/= 0H <-> -. ~H = 0H )`
10 nmopun
` |-  ( ( ~H =/= 0H /\ T e. UniOp ) -> ( normop ` T ) = 1 )`
11 1re
` |-  1 e. RR`
12 10 11 eqeltrdi
` |-  ( ( ~H =/= 0H /\ T e. UniOp ) -> ( normop ` T ) e. RR )`
13 9 12 sylanbr
` |-  ( ( -. ~H = 0H /\ T e. UniOp ) -> ( normop ` T ) e. RR )`
14 8 13 pm2.61ian
` |-  ( T e. UniOp -> ( normop ` T ) e. RR )`
15 elbdop2
` |-  ( T e. BndLinOp <-> ( T e. LinOp /\ ( normop ` T ) e. RR ) )`
16 1 14 15 sylanbrc
` |-  ( T e. UniOp -> T e. BndLinOp )`