# 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}{0}_{\mathrm{op}}{W}$
0blo.7 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
Assertion 0blo ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {Z}\in {B}$

### Proof

Step Hyp Ref Expression
1 0blo.0 ${⊢}{Z}={U}{0}_{\mathrm{op}}{W}$
2 0blo.7 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
3 eqid ${⊢}{U}\mathrm{LnOp}{W}={U}\mathrm{LnOp}{W}$
4 1 3 0lno ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {Z}\in \left({U}\mathrm{LnOp}{W}\right)$
5 eqid ${⊢}{U}{normOp}_{\mathrm{OLD}}{W}={U}{normOp}_{\mathrm{OLD}}{W}$
6 5 1 nmoo0 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({Z}\right)=0$
7 0re ${⊢}0\in ℝ$
8 6 7 eqeltrdi ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({Z}\right)\in ℝ$
9 5 3 2 isblo2 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left({Z}\in {B}↔\left({Z}\in \left({U}\mathrm{LnOp}{W}\right)\wedge \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({Z}\right)\in ℝ\right)\right)$
10 4 8 9 mpbir2and ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {Z}\in {B}$