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 ) → ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ( 𝑁 ‘ 𝑇 ) < +∞ ) ) )