# 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}=\mathrm{IndMet}\left({U}\right)$
blocn.d ${⊢}{D}=\mathrm{IndMet}\left({W}\right)$
blocn.j ${⊢}{J}=\mathrm{MetOpen}\left({C}\right)$
blocn.k ${⊢}{K}=\mathrm{MetOpen}\left({D}\right)$
blocn.5 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
blocn.u ${⊢}{U}\in \mathrm{NrmCVec}$
blocn.w ${⊢}{W}\in \mathrm{NrmCVec}$
Assertion blocn2 ${⊢}{T}\in {B}\to {T}\in \left({J}\mathrm{Cn}{K}\right)$

### Proof

Step Hyp Ref Expression
1 blocn.8 ${⊢}{C}=\mathrm{IndMet}\left({U}\right)$
2 blocn.d ${⊢}{D}=\mathrm{IndMet}\left({W}\right)$
3 blocn.j ${⊢}{J}=\mathrm{MetOpen}\left({C}\right)$
4 blocn.k ${⊢}{K}=\mathrm{MetOpen}\left({D}\right)$
5 blocn.5 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
6 blocn.u ${⊢}{U}\in \mathrm{NrmCVec}$
7 blocn.w ${⊢}{W}\in \mathrm{NrmCVec}$
8 eqid ${⊢}{U}\mathrm{LnOp}{W}={U}\mathrm{LnOp}{W}$
9 8 5 bloln ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {B}\right)\to {T}\in \left({U}\mathrm{LnOp}{W}\right)$
10 6 7 9 mp3an12 ${⊢}{T}\in {B}\to {T}\in \left({U}\mathrm{LnOp}{W}\right)$
11 1 2 3 4 5 6 7 8 blocn ${⊢}{T}\in \left({U}\mathrm{LnOp}{W}\right)\to \left({T}\in \left({J}\mathrm{Cn}{K}\right)↔{T}\in {B}\right)$
12 11 biimprd ${⊢}{T}\in \left({U}\mathrm{LnOp}{W}\right)\to \left({T}\in {B}\to {T}\in \left({J}\mathrm{Cn}{K}\right)\right)$
13 10 12 mpcom ${⊢}{T}\in {B}\to {T}\in \left({J}\mathrm{Cn}{K}\right)$