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

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	$⊢ 0_{hop} \in BndLinOp$

Step	Hyp	Ref	Expression
1		0lnop	$⊢ 0_{hop} \in LinOp$
2		nmop0	$⊢ {norm}_{op} (0_{hop}) = 0$
3		0ltpnf	$⊢ 0 < +∞$
4	2 3	eqbrtri	$⊢ {norm}_{op} (0_{hop}) < +∞$
5		elbdop	$⊢ 0_{hop} \in BndLinOp \leftrightarrow (0_{hop} \in LinOp \land {norm}_{op} (0_{hop}) < +∞)$
6	1 4 5	mpbir2an	$⊢ 0_{hop} \in BndLinOp$