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 UniOp T BndLinOp

Proof

Step Hyp Ref Expression
1 unoplin T UniOp T LinOp
2 unopf1o T UniOp T : 1-1 onto
3 f1of T : 1-1 onto T :
4 2 3 syl T UniOp T :
5 nmop0h = 0 T : norm op T = 0
6 0re 0
7 5 6 syl6eqel = 0 T : norm op T
8 4 7 sylan2 = 0 T UniOp norm op T
9 df-ne 0 ¬ = 0
10 nmopun 0 T UniOp norm op T = 1
11 1re 1
12 10 11 syl6eqel 0 T UniOp norm op T
13 9 12 sylanbr ¬ = 0 T UniOp norm op T
14 8 13 pm2.61ian T UniOp norm op T
15 elbdop2 T BndLinOp T LinOp norm op T
16 1 14 15 sylanbrc T UniOp T BndLinOp