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 ⊢ 𝑁 = ( 𝑈 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 bitrdi ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ( 𝑁 ‘ 𝑇 ) < +∞ ) ) )