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 op W
0blo.7 ⊢ B = U BLnOp W
Assertion 0blo ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → Z ∈ B

Proof

Step Hyp Ref Expression
1 0blo.0 ⊢ Z = U 0 op W
2 0blo.7 ⊢ B = U BLnOp W
3 eqid ⊢ U LnOp W = U LnOp W
4 1 3 0lno ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → Z ∈ U LnOp W
5 eqid ⊢ U normOp OLD W = U normOp OLD W
6 5 1 nmoo0 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → U normOp OLD W ⁡ Z = 0
7 0re ⊢ 0 ∈ ℝ
8 6 7 eqeltrdi ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → U normOp OLD W ⁡ Z ∈ ℝ
9 5 3 2 isblo2 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → Z ∈ B ↔ Z ∈ U LnOp W ∧ U normOp OLD W ⁡ Z ∈ ℝ
10 4 8 9 mpbir2and ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → Z ∈ B