Metamath Proof Explorer

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 ⊢ T ∈ BndLinOp ↔ T ∈ LinOp ∧ norm op ⁡ T ∈ ℝ

Proof

Step Hyp Ref Expression
1 elbdop ⊢ T ∈ BndLinOp ↔ T ∈ LinOp ∧ norm op ⁡ T < +∞
2 lnopf ⊢ T ∈ LinOp → T : ℋ ⟶ ℋ
3 nmopreltpnf ⊢ T : ℋ ⟶ ℋ → norm op ⁡ T ∈ ℝ ↔ norm op ⁡ T < +∞
4 2 3 syl ⊢ T ∈ LinOp → norm op ⁡ T ∈ ℝ ↔ norm op ⁡ T < +∞
5 4 pm5.32i ⊢ T ∈ LinOp ∧ norm op ⁡ T ∈ ℝ ↔ T ∈ LinOp ∧ norm op ⁡ T < +∞
6 1 5 bitr4i ⊢ T ∈ BndLinOp ↔ T ∈ LinOp ∧ norm op ⁡ T ∈ ℝ