Theorem bloln

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

	Ref	Expression
Hypotheses	bloln.4	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
	bloln.5	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
Assertion	bloln	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → 𝑇 ∈ 𝐿 )

Proof

Step	Hyp	Ref	Expression
1		bloln.4	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
2		bloln.5	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
3		eqid	⊢ ( 𝑈 normOpOLD 𝑊 ) = ( 𝑈 normOpOLD 𝑊 )
4	3 1 2	isblo	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) < +∞ ) ) )
5	4	simprbda	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑇 ∈ 𝐵 ) → 𝑇 ∈ 𝐿 )
6	5	3impa	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → 𝑇 ∈ 𝐿 )