Theorem 0bdop

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

	Ref	Expression
Assertion	0bdop	⊢ 0hop ∈ BndLinOp

Proof

Step	Hyp	Ref	Expression
1		0lnop	⊢ 0hop ∈ LinOp
2		nmop0	⊢ ( normop ‘ 0hop ) = 0
3		0ltpnf	⊢ 0 < +∞
4	2 3	eqbrtri	⊢ ( normop ‘ 0hop ) < +∞
5		elbdop	⊢ ( 0hop ∈ BndLinOp ↔ ( 0hop ∈ LinOp ∧ ( normop ‘ 0hop ) < +∞ ) )
6	1 4 5	mpbir2an	⊢ 0hop ∈ BndLinOp