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 LnOp W )
	bloln.5	|- B = ( U BLnOp W )
Assertion	bloln	|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. B ) -> T e. L )

Proof

Step	Hyp	Ref	Expression
1		bloln.4	|- L = ( U LnOp W )
2		bloln.5	|- B = ( U BLnOp W )
3		eqid	|- ( U normOpOLD W ) = ( U normOpOLD W )
4	3 1 2	isblo	|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( T e. B <-> ( T e. L /\ ( ( U normOpOLD W ) ` T ) < +oo ) ) )
5	4	simprbda	|- ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ T e. B ) -> T e. L )
6	5	3impa	|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. B ) -> T e. L )