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 )