Theorem bloln

Description: A bounded operator is a linear operator. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bloln.4	$$⊢L=U\mathrm{LnOp}W$$
	bloln.5	$$⊢B=U\mathrm{BLnOp}W$$
Assertion	bloln	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in \mathrm{NrmCVec}\wedge T\in B\right)\to T\in L$$

Proof

Step	Hyp	Ref	Expression
1		bloln.4	$$⊢L=U\mathrm{LnOp}W$$
2		bloln.5	$$⊢B=U\mathrm{BLnOp}W$$
3		eqid	$$⊢U{normOp}_{\mathrm{OLD}}W=U{normOp}_{\mathrm{OLD}}W$$
4	3 1 2	isblo	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in \mathrm{NrmCVec}\right)\to \left(T\in B\leftrightarrow \left(T\in L\wedge \left(U{normOp}_{\mathrm{OLD}}W\right)\left(T\right)<\mathrm{+\infty }\right)\right)$$
5	4	simprbda	$$⊢\left(\left(U\in \mathrm{NrmCVec}\wedge W\in \mathrm{NrmCVec}\right)\wedge T\in B\right)\to T\in L$$
6	5	3impa	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in \mathrm{NrmCVec}\wedge T\in B\right)\to T\in L$$