Theorem blof

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

	Ref	Expression
Hypotheses	blof.1	|- X = ( BaseSet ` U )
	blof.2	|- Y = ( BaseSet ` W )
	blof.5	|- B = ( U BLnOp W )
Assertion	blof	|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. B ) -> T : X --> Y )

Proof

Step	Hyp	Ref	Expression
1		blof.1	|- X = ( BaseSet ` U )
2		blof.2	|- Y = ( BaseSet ` W )
3		blof.5	|- B = ( U BLnOp W )
4		eqid	|- ( U LnOp W ) = ( U LnOp W )
5	4 3	bloln	|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. B ) -> T e. ( U LnOp W ) )
6	1 2 4	lnof	|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. ( U LnOp W ) ) -> T : X --> Y )
7	5 6	syld3an3	|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. B ) -> T : X --> Y )