Theorem blof

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

	Ref	Expression
Hypotheses	blof.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	blof.2	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	blof.5	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
Assertion	blof	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → 𝑇 : 𝑋 ⟶ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		blof.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		blof.2	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3		blof.5	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
4		eqid	⊢ ( 𝑈 LnOp 𝑊 ) = ( 𝑈 LnOp 𝑊 )
5	4 3	bloln	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → 𝑇 ∈ ( 𝑈 LnOp 𝑊 ) )
6	1 2 4	lnof	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ ( 𝑈 LnOp 𝑊 ) ) → 𝑇 : 𝑋 ⟶ 𝑌 )
7	5 6	syld3an3	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → 𝑇 : 𝑋 ⟶ 𝑌 )