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 )