This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )