Metamath Proof Explorer

Theorem bloln

Description: A bounded operator is a linear operator. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses bloln.4 ⊢ L = U LnOp W
bloln.5 ⊢ B = U BLnOp W
Assertion bloln ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ B → T ∈ L

Proof

Step Hyp Ref Expression
1 bloln.4 ⊢ L = U LnOp W
2 bloln.5 ⊢ B = U BLnOp W
3 eqid ⊢ U normOp OLD W = U normOp OLD W
4 3 1 2 isblo ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → T ∈ B ↔ T ∈ L ∧ U normOp OLD W ⁡ T < +∞
5 4 simprbda ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ B → T ∈ L
6 5 3impa ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ B → T ∈ L