Theorem elbdop

Description: Property defining a bounded linear Hilbert space operator. (Contributed by NM, 18-Jan-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	elbdop	⊢ ( 𝑇 ∈ BndLinOp ↔ ( 𝑇 ∈ LinOp ∧ ( normop ‘ 𝑇 ) < +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑡 = 𝑇 → ( normop ‘ 𝑡 ) = ( normop ‘ 𝑇 ) )
2	1	breq1d	⊢ ( 𝑡 = 𝑇 → ( ( normop ‘ 𝑡 ) < +∞ ↔ ( normop ‘ 𝑇 ) < +∞ ) )
3		df-bdop	⊢ BndLinOp = { 𝑡 ∈ LinOp ∣ ( normop ‘ 𝑡 ) < +∞ }
4	2 3	elrab2	⊢ ( 𝑇 ∈ BndLinOp ↔ ( 𝑇 ∈ LinOp ∧ ( normop ‘ 𝑇 ) < +∞ ) )