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)\leftrightarrow 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)$$