This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = 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 \in NrmCVec$
		blocni.w	$⊢ W \in NrmCVec$
		blocni.l	$⊢ T \in L$
		lnocni.1	$⊢ X = BaseSet (U)$
	Assertion	lnocni	$⊢ (P \in X \land T \in (J CnP K) (P)) \to T \in (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 \in NrmCVec$
8		blocni.w	$⊢ W \in NrmCVec$
9		blocni.l	$⊢ T \in L$
10		lnocni.1	$⊢ X = BaseSet (U)$
11	1 2 3 4 5 6 7 8 9 10	blocnilem	$⊢ (P \in X \land T \in (J CnP K) (P)) \to T \in B$
12	1 2 3 4 5 6 7 8 9	blocni	$⊢ T \in (J Cn K) \leftrightarrow T \in B$
13	11 12	sylibr	$⊢ (P \in X \land T \in (J CnP K) (P)) \to T \in (J Cn K)$