This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑇 ∈ UniOp → 𝑇 ∈ BndLinOp )

Proof

Step Hyp Ref Expression
1 unoplin ⊢ ( 𝑇 ∈ UniOp → 𝑇 ∈ LinOp )
2 unopf1o ⊢ ( 𝑇 ∈ UniOp → 𝑇 : ℋ –1-1-onto→ ℋ )
3 f1of ⊢ ( 𝑇 : ℋ –1-1-onto→ ℋ → 𝑇 : ℋ ⟶ ℋ )
4 2 3 syl ⊢ ( 𝑇 ∈ UniOp → 𝑇 : ℋ ⟶ ℋ )
5 nmop0h ⊢ ( ( ℋ = 0ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( normop ‘ 𝑇 ) = 0 )
6 0re ⊢ 0 ∈ ℝ
7 5 6 eqeltrdi ⊢ ( ( ℋ = 0ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( normop ‘ 𝑇 ) ∈ ℝ )
8 4 7 sylan2 ⊢ ( ( ℋ = 0ℋ ∧ 𝑇 ∈ UniOp ) → ( normop ‘ 𝑇 ) ∈ ℝ )
9 df-ne ⊢ ( ℋ ≠ 0ℋ ↔ ¬ ℋ = 0ℋ )
10 nmopun ⊢ ( ( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp ) → ( normop ‘ 𝑇 ) = 1 )
11 1re ⊢ 1 ∈ ℝ
12 10 11 eqeltrdi ⊢ ( ( ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp ) → ( normop ‘ 𝑇 ) ∈ ℝ )
13 9 12 sylanbr ⊢ ( ( ¬ ℋ = 0ℋ ∧ 𝑇 ∈ UniOp ) → ( normop ‘ 𝑇 ) ∈ ℝ )
14 8 13 pm2.61ian ⊢ ( 𝑇 ∈ UniOp → ( normop ‘ 𝑇 ) ∈ ℝ )
15 elbdop2 ⊢ ( 𝑇 ∈ BndLinOp ↔ ( 𝑇 ∈ LinOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) )
16 1 14 15 sylanbrc ⊢ ( 𝑇 ∈ UniOp → 𝑇 ∈ BndLinOp )