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 ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ B → T : X ⟶ Y

Proof

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 ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ B → T ∈ U LnOp W
6 1 2 4 lnof ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ U LnOp W → T : X ⟶ Y
7 5 6 syld3an3 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ B → T : X ⟶ Y