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 = U normOp OLD W
bloval.4 ⊢ L = U LnOp W
bloval.5 ⊢ B = U BLnOp W
Assertion isblo2 ⊢ 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 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 ∈ ℝ