Theorem isblo

Description: The predicate "is a bounded linear operator." (Contributed by NM, 6-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bloval.3	$$⊢N=U{normOp}_{\mathrm{OLD}}W$$
	bloval.4	$$⊢L=U\mathrm{LnOp}W$$
	bloval.5	$$⊢B=U\mathrm{BLnOp}W$$
Assertion	isblo	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in \mathrm{NrmCVec}\right)\to \left(T\in B\leftrightarrow \left(T\in L\wedge N\left(T\right)<\mathrm{+\infty }\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		bloval.3	$$⊢N=U{normOp}_{\mathrm{OLD}}W$$
2		bloval.4	$$⊢L=U\mathrm{LnOp}W$$
3		bloval.5	$$⊢B=U\mathrm{BLnOp}W$$
4	1 2 3	bloval	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in \mathrm{NrmCVec}\right)\to B=\left\{t\in L|N\left(t\right)<\mathrm{+\infty }\right\}$$
5	4	eleq2d	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in \mathrm{NrmCVec}\right)\to \left(T\in B\leftrightarrow T\in \left\{t\in L|N\left(t\right)<\mathrm{+\infty }\right\}\right)$$
6		fveq2	$$⊢t=T\to N\left(t\right)=N\left(T\right)$$
7	6	breq1d	$$⊢t=T\to \left(N\left(t\right)<\mathrm{+\infty }\leftrightarrow N\left(T\right)<\mathrm{+\infty }\right)$$
8	7	elrab	$$⊢T\in \left\{t\in L|N\left(t\right)<\mathrm{+\infty }\right\}\leftrightarrow \left(T\in L\wedge N\left(T\right)<\mathrm{+\infty }\right)$$
9	5 8	bitrdi	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in \mathrm{NrmCVec}\right)\to \left(T\in B\leftrightarrow \left(T\in L\wedge N\left(T\right)<\mathrm{+\infty }\right)\right)$$