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 𝑁 = ( 𝑈 normOpOLD 𝑊 )
bloval.4 𝐿 = ( 𝑈 LnOp 𝑊 )
bloval.5 𝐵 = ( 𝑈 BLnOp 𝑊 )
Assertion isblo ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑇𝐵 ↔ ( 𝑇𝐿 ∧ ( 𝑁𝑇 ) < +∞ ) ) )

Proof

Step Hyp Ref Expression
1 bloval.3 𝑁 = ( 𝑈 normOpOLD 𝑊 )
2 bloval.4 𝐿 = ( 𝑈 LnOp 𝑊 )
3 bloval.5 𝐵 = ( 𝑈 BLnOp 𝑊 )
4 1 2 3 bloval ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝐵 = { 𝑡𝐿 ∣ ( 𝑁𝑡 ) < +∞ } )
5 4 eleq2d ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑇𝐵𝑇 ∈ { 𝑡𝐿 ∣ ( 𝑁𝑡 ) < +∞ } ) )
6 fveq2 ( 𝑡 = 𝑇 → ( 𝑁𝑡 ) = ( 𝑁𝑇 ) )
7 6 breq1d ( 𝑡 = 𝑇 → ( ( 𝑁𝑡 ) < +∞ ↔ ( 𝑁𝑇 ) < +∞ ) )
8 7 elrab ( 𝑇 ∈ { 𝑡𝐿 ∣ ( 𝑁𝑡 ) < +∞ } ↔ ( 𝑇𝐿 ∧ ( 𝑁𝑇 ) < +∞ ) )
9 5 8 syl6bb ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑇𝐵 ↔ ( 𝑇𝐿 ∧ ( 𝑁𝑇 ) < +∞ ) ) )