Theorem 0blo

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

	Ref	Expression
Hypotheses	0blo.0	|- Z = ( U 0op W )
	0blo.7	|- B = ( U BLnOp W )
Assertion	0blo	|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> Z e. B )

Proof

Step	Hyp	Ref	Expression
1		0blo.0	|- Z = ( U 0op W )
2		0blo.7	|- B = ( U BLnOp W )
3		eqid	|- ( U LnOp W ) = ( U LnOp W )
4	1 3	0lno	|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> Z e. ( U LnOp W ) )
5		eqid	|- ( U normOpOLD W ) = ( U normOpOLD W )
6	5 1	nmoo0	|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( ( U normOpOLD W ) ` Z ) = 0 )
7		0re	|- 0 e. RR
8	6 7	eqeltrdi	|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( ( U normOpOLD W ) ` Z ) e. RR )
9	5 3 2	isblo2	|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( Z e. B <-> ( Z e. ( U LnOp W ) /\ ( ( U normOpOLD W ) ` Z ) e. RR ) ) )
10	4 8 9	mpbir2and	|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> Z e. B )