Metamath Proof Explorer

Theorem blof

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

	Ref	Expression
Hypotheses	blof.1	$⊢ X = BaseSet (U)$
	blof.2	$⊢ Y = BaseSet (W)$
	blof.5	$⊢ B = U BLnOp W$
Assertion	blof	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in B) \to T : X ⟶ Y$

Step	Hyp	Ref	Expression
1		blof.1	$⊢ X = BaseSet (U)$
2		blof.2	$⊢ Y = BaseSet (W)$
3		blof.5	$⊢ B = U BLnOp W$
4		eqid	$⊢ U LnOp W = U LnOp W$
5	4 3	bloln	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in B) \to T \in (U LnOp W)$
6	1 2 4	lnof	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in (U LnOp W)) \to T : X ⟶ Y$
7	5 6	syld3an3	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in B) \to T : X ⟶ Y$