Metamath Proof Explorer


Theorem isblo

Description: The predicate "is a bounded linear operator." (Contributed by NM, 6-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses bloval.3 N = U normOp OLD W
bloval.4 L = U LnOp W
bloval.5 B = U BLnOp W
Assertion isblo U NrmCVec W NrmCVec T B T L N T < +∞

Proof

Step Hyp Ref Expression
1 bloval.3 N = U normOp OLD W
2 bloval.4 L = U LnOp W
3 bloval.5 B = U BLnOp W
4 1 2 3 bloval U NrmCVec W NrmCVec B = t L | N t < +∞
5 4 eleq2d U NrmCVec W NrmCVec T B T t L | N t < +∞
6 fveq2 t = T N t = N T
7 6 breq1d t = T N t < +∞ N T < +∞
8 7 elrab T t L | N t < +∞ T L N T < +∞
9 5 8 bitrdi U NrmCVec W NrmCVec T B T L N T < +∞