Metamath Proof Explorer

Theorem 0bdop

Description: The identically zero operator is bounded. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion 0bdop 
|- 0hop e. BndLinOp

Proof

Step Hyp Ref Expression
1 0lnop 
 |-  0hop e. LinOp
2 nmop0 
 |-  ( normop ` 0hop ) = 0
3 0ltpnf 
 |-  0 < +oo
4 2 3 eqbrtri 
 |-  ( normop ` 0hop ) < +oo
5 elbdop 
 |-  ( 0hop e. BndLinOp <-> ( 0hop e. LinOp /\ ( normop ` 0hop ) < +oo ) )
6 1 4 5 mpbir2an 
 |-  0hop e. BndLinOp