Metamath Proof Explorer

Theorem blocn2

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

Ref Expression
Hypotheses blocn.8 ⊢ C = IndMet ⁡ U
blocn.d ⊢ D = IndMet ⁡ W
blocn.j ⊢ J = MetOpen ⁡ C
blocn.k ⊢ K = MetOpen ⁡ D
blocn.5 ⊢ B = U BLnOp W
blocn.u ⊢ U ∈ NrmCVec
blocn.w ⊢ W ∈ NrmCVec
Assertion blocn2 ⊢ T ∈ B → T ∈ J Cn K

Proof

Step Hyp Ref Expression
1 blocn.8 ⊢ C = IndMet ⁡ U
2 blocn.d ⊢ D = IndMet ⁡ W
3 blocn.j ⊢ J = MetOpen ⁡ C
4 blocn.k ⊢ K = MetOpen ⁡ D
5 blocn.5 ⊢ B = U BLnOp W
6 blocn.u ⊢ U ∈ NrmCVec
7 blocn.w ⊢ W ∈ NrmCVec
8 eqid ⊢ U LnOp W = U LnOp W
9 8 5 bloln ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ B → T ∈ U LnOp W
10 6 7 9 mp3an12 ⊢ T ∈ B → T ∈ U LnOp W
11 1 2 3 4 5 6 7 8 blocn ⊢ T ∈ U LnOp W → T ∈ J Cn K ↔ T ∈ B
12 11 biimprd ⊢ T ∈ U LnOp W → T ∈ B → T ∈ J Cn K
13 10 12 mpcom ⊢ T ∈ B → T ∈ J Cn K