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 \in BndLinOp \leftrightarrow (T \in LinOp \land {norm}_{op} (T) \in ℝ)$

Step	Hyp	Ref	Expression
1		elbdop	$⊢ T \in BndLinOp \leftrightarrow (T \in LinOp \land {norm}_{op} (T) < +∞)$
2		lnopf	$⊢ T \in LinOp \to T : ℋ ⟶ ℋ$
3		nmopreltpnf	$⊢ T : ℋ ⟶ ℋ \to ({norm}_{op} (T) \in ℝ \leftrightarrow {norm}_{op} (T) < +∞)$
4	2 3	syl	$⊢ T \in LinOp \to ({norm}_{op} (T) \in ℝ \leftrightarrow {norm}_{op} (T) < +∞)$
5	4	pm5.32i	$⊢ (T \in LinOp \land {norm}_{op} (T) \in ℝ) \leftrightarrow (T \in LinOp \land {norm}_{op} (T) < +∞)$
6	1 5	bitr4i	$⊢ T \in BndLinOp \leftrightarrow (T \in LinOp \land {norm}_{op} (T) \in ℝ)$

Metamath Proof Explorer