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}\in \mathrm{UniOp}\to {T}\in \mathrm{BndLinOp}$

Proof

Step Hyp Ref Expression
1 unoplin ${⊢}{T}\in \mathrm{UniOp}\to {T}\in \mathrm{LinOp}$
2 unopf1o ${⊢}{T}\in \mathrm{UniOp}\to {T}:ℋ\underset{1-1 onto}{⟶}ℋ$
3 f1of ${⊢}{T}:ℋ\underset{1-1 onto}{⟶}ℋ\to {T}:ℋ⟶ℋ$
4 2 3 syl ${⊢}{T}\in \mathrm{UniOp}\to {T}:ℋ⟶ℋ$
5 nmop0h ${⊢}\left(ℋ={0}_{ℋ}\wedge {T}:ℋ⟶ℋ\right)\to {norm}_{\mathrm{op}}\left({T}\right)=0$
6 0re ${⊢}0\in ℝ$
7 5 6 syl6eqel ${⊢}\left(ℋ={0}_{ℋ}\wedge {T}:ℋ⟶ℋ\right)\to {norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
8 4 7 sylan2 ${⊢}\left(ℋ={0}_{ℋ}\wedge {T}\in \mathrm{UniOp}\right)\to {norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
9 df-ne ${⊢}ℋ\ne {0}_{ℋ}↔¬ℋ={0}_{ℋ}$
10 nmopun ${⊢}\left(ℋ\ne {0}_{ℋ}\wedge {T}\in \mathrm{UniOp}\right)\to {norm}_{\mathrm{op}}\left({T}\right)=1$
11 1re ${⊢}1\in ℝ$
12 10 11 syl6eqel ${⊢}\left(ℋ\ne {0}_{ℋ}\wedge {T}\in \mathrm{UniOp}\right)\to {norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
13 9 12 sylanbr ${⊢}\left(¬ℋ={0}_{ℋ}\wedge {T}\in \mathrm{UniOp}\right)\to {norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
14 8 13 pm2.61ian ${⊢}{T}\in \mathrm{UniOp}\to {norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
15 elbdop2 ${⊢}{T}\in \mathrm{BndLinOp}↔\left({T}\in \mathrm{LinOp}\wedge {norm}_{\mathrm{op}}\left({T}\right)\in ℝ\right)$
16 1 14 15 sylanbrc ${⊢}{T}\in \mathrm{UniOp}\to {T}\in \mathrm{BndLinOp}$