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

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 < +∞