# Metamath Proof Explorer

## Theorem blocn

Description: A linear operator is continuous iff it is bounded. Theorem 2.7-9(a) of Kreyszig p. 97. (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}$
blocn.4 ${⊢}{L}={U}\mathrm{LnOp}{W}$
Assertion blocn ${⊢}{T}\in {L}\to \left({T}\in \left({J}\mathrm{Cn}{K}\right)↔{T}\in {B}\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 blocn.4 ${⊢}{L}={U}\mathrm{LnOp}{W}$
9 eleq1 ${⊢}{T}=if\left({T}\in {L},{T},{U}{0}_{\mathrm{op}}{W}\right)\to \left({T}\in \left({J}\mathrm{Cn}{K}\right)↔if\left({T}\in {L},{T},{U}{0}_{\mathrm{op}}{W}\right)\in \left({J}\mathrm{Cn}{K}\right)\right)$
10 eleq1 ${⊢}{T}=if\left({T}\in {L},{T},{U}{0}_{\mathrm{op}}{W}\right)\to \left({T}\in {B}↔if\left({T}\in {L},{T},{U}{0}_{\mathrm{op}}{W}\right)\in {B}\right)$
11 9 10 bibi12d ${⊢}{T}=if\left({T}\in {L},{T},{U}{0}_{\mathrm{op}}{W}\right)\to \left(\left({T}\in \left({J}\mathrm{Cn}{K}\right)↔{T}\in {B}\right)↔\left(if\left({T}\in {L},{T},{U}{0}_{\mathrm{op}}{W}\right)\in \left({J}\mathrm{Cn}{K}\right)↔if\left({T}\in {L},{T},{U}{0}_{\mathrm{op}}{W}\right)\in {B}\right)\right)$
12 eqid ${⊢}{U}{0}_{\mathrm{op}}{W}={U}{0}_{\mathrm{op}}{W}$
13 12 8 0lno ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {U}{0}_{\mathrm{op}}{W}\in {L}$
14 6 7 13 mp2an ${⊢}{U}{0}_{\mathrm{op}}{W}\in {L}$
15 14 elimel ${⊢}if\left({T}\in {L},{T},{U}{0}_{\mathrm{op}}{W}\right)\in {L}$
16 1 2 3 4 8 5 6 7 15 blocni ${⊢}if\left({T}\in {L},{T},{U}{0}_{\mathrm{op}}{W}\right)\in \left({J}\mathrm{Cn}{K}\right)↔if\left({T}\in {L},{T},{U}{0}_{\mathrm{op}}{W}\right)\in {B}$
17 11 16 dedth ${⊢}{T}\in {L}\to \left({T}\in \left({J}\mathrm{Cn}{K}\right)↔{T}\in {B}\right)$