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 = ( IndMet ` U )
	blocni.d	|- D = ( IndMet ` W )
	blocni.j	|- J = ( MetOpen ` C )
	blocni.k	|- K = ( MetOpen ` D )
	blocni.4	|- L = ( U LnOp W )
	blocni.5	|- B = ( U BLnOp W )
	blocni.u	|- U e. NrmCVec
	blocni.w	|- W e. NrmCVec
	blocni.l	|- T e. L
	lnocni.1	|- X = ( BaseSet ` U )
Assertion	lnocni	|- ( ( P e. X /\ T e. ( ( J CnP K ) ` P ) ) -> T e. ( J Cn K ) )

Proof

Step	Hyp	Ref	Expression
1		blocni.8	|- C = ( IndMet ` U )
2		blocni.d	|- D = ( IndMet ` W )
3		blocni.j	|- J = ( MetOpen ` C )
4		blocni.k	|- K = ( MetOpen ` D )
5		blocni.4	|- L = ( U LnOp W )
6		blocni.5	|- B = ( U BLnOp W )
7		blocni.u	|- U e. NrmCVec
8		blocni.w	|- W e. NrmCVec
9		blocni.l	|- T e. L
10		lnocni.1	|- X = ( BaseSet ` U )
11	1 2 3 4 5 6 7 8 9 10	blocnilem	|- ( ( P e. X /\ T e. ( ( J CnP K ) ` P ) ) -> T e. B )
12	1 2 3 4 5 6 7 8 9	blocni	|- ( T e. ( J Cn K ) <-> T e. B )
13	11 12	sylibr	|- ( ( P e. X /\ T e. ( ( J CnP K ) ` P ) ) -> T e. ( J Cn K ) )