This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ t = T \to {norm}_{op} (t) = {norm}_{op} (T)$
2	1	breq1d	$⊢ t = T \to ({norm}_{op} (t) < +∞ \leftrightarrow {norm}_{op} (T) < +∞)$
3		df-bdop	$⊢ BndLinOp = \{t \in LinOp \| {norm}_{op} (t) < +∞\}$
4	2 3	elrab2	$⊢ T \in BndLinOp \leftrightarrow (T \in LinOp \land {norm}_{op} (T) < +∞)$