Theorem elbdop2

Description: Property defining a bounded linear Hilbert space operator. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	elbdop2	⊢ ( 𝑇 ∈ BndLinOp ↔ ( 𝑇 ∈ LinOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) )

Proof

Step	Hyp	Ref	Expression
1		elbdop	⊢ ( 𝑇 ∈ BndLinOp ↔ ( 𝑇 ∈ LinOp ∧ ( normop ‘ 𝑇 ) < +∞ ) )
2		lnopf	⊢ ( 𝑇 ∈ LinOp → 𝑇 : ℋ ⟶ ℋ )
3		nmopreltpnf	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( ( normop ‘ 𝑇 ) ∈ ℝ ↔ ( normop ‘ 𝑇 ) < +∞ ) )
4	2 3	syl	⊢ ( 𝑇 ∈ LinOp → ( ( normop ‘ 𝑇 ) ∈ ℝ ↔ ( normop ‘ 𝑇 ) < +∞ ) )
5	4	pm5.32i	⊢ ( ( 𝑇 ∈ LinOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ↔ ( 𝑇 ∈ LinOp ∧ ( normop ‘ 𝑇 ) < +∞ ) )
6	1 5	bitr4i	⊢ ( 𝑇 ∈ BndLinOp ↔ ( 𝑇 ∈ LinOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) )