Metamath Proof Explorer

Theorem isblo2

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

Ref Expression
Hypotheses bloval.3 ⊢N=UnormOpOLDW
bloval.4 ⊢L=ULnOpW
bloval.5 ⊢B=UBLnOpW
Assertion isblo2 ⊢U∈NrmCVec∧W∈NrmCVec→T∈B↔T∈L∧N⁡T∈ℝ

Proof

Step Hyp Ref Expression
1 bloval.3 ⊢N=UnormOpOLDW
2 bloval.4 ⊢L=ULnOpW
3 bloval.5 ⊢B=UBLnOpW
4 1 2 3 isblo ⊢U∈NrmCVec∧W∈NrmCVec→T∈B↔T∈L∧N⁡T<+∞
5 eqid ⊢BaseSet⁡U=BaseSet⁡U
6 eqid ⊢BaseSet⁡W=BaseSet⁡W
7 5 6 2 lnof ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L→T:BaseSet⁡U⟶BaseSet⁡W
8 5 6 1 nmoreltpnf ⊢U∈NrmCVec∧W∈NrmCVec∧T:BaseSet⁡U⟶BaseSet⁡W→N⁡T∈ℝ↔N⁡T<+∞
9 7 8 syld3an3 ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L→N⁡T∈ℝ↔N⁡T<+∞
10 9 3expa ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L→N⁡T∈ℝ↔N⁡T<+∞
11 10 pm5.32da ⊢U∈NrmCVec∧W∈NrmCVec→T∈L∧N⁡T∈ℝ↔T∈L∧N⁡T<+∞
12 4 11 bitr4d ⊢U∈NrmCVec∧W∈NrmCVec→T∈B↔T∈L∧N⁡T∈ℝ