# Metamath Proof Explorer

## Theorem lnocni

Description: If a linear operator is continuous at any point, it is continuous everywhere. Theorem 2.7-9(b) of Kreyszig p. 97. (Contributed by NM, 18-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses blocni.8 ${⊢}{C}=\mathrm{IndMet}\left({U}\right)$
blocni.d ${⊢}{D}=\mathrm{IndMet}\left({W}\right)$
blocni.j ${⊢}{J}=\mathrm{MetOpen}\left({C}\right)$
blocni.k ${⊢}{K}=\mathrm{MetOpen}\left({D}\right)$
blocni.4 ${⊢}{L}={U}\mathrm{LnOp}{W}$
blocni.5 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
blocni.u ${⊢}{U}\in \mathrm{NrmCVec}$
blocni.w ${⊢}{W}\in \mathrm{NrmCVec}$
blocni.l ${⊢}{T}\in {L}$
lnocni.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
Assertion lnocni ${⊢}\left({P}\in {X}\wedge {T}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)\right)\to {T}\in \left({J}\mathrm{Cn}{K}\right)$

### Proof

Step Hyp Ref Expression
1 blocni.8 ${⊢}{C}=\mathrm{IndMet}\left({U}\right)$
2 blocni.d ${⊢}{D}=\mathrm{IndMet}\left({W}\right)$
3 blocni.j ${⊢}{J}=\mathrm{MetOpen}\left({C}\right)$
4 blocni.k ${⊢}{K}=\mathrm{MetOpen}\left({D}\right)$
5 blocni.4 ${⊢}{L}={U}\mathrm{LnOp}{W}$
6 blocni.5 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
7 blocni.u ${⊢}{U}\in \mathrm{NrmCVec}$
8 blocni.w ${⊢}{W}\in \mathrm{NrmCVec}$
9 blocni.l ${⊢}{T}\in {L}$
10 lnocni.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
11 1 2 3 4 5 6 7 8 9 10 blocnilem ${⊢}\left({P}\in {X}\wedge {T}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)\right)\to {T}\in {B}$
12 1 2 3 4 5 6 7 8 9 blocni ${⊢}{T}\in \left({J}\mathrm{Cn}{K}\right)↔{T}\in {B}$
13 11 12 sylibr ${⊢}\left({P}\in {X}\wedge {T}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)\right)\to {T}\in \left({J}\mathrm{Cn}{K}\right)$