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	⊢ 𝐶 = ( IndMet ‘ 𝑈 )
		blocni.d	⊢ 𝐷 = ( IndMet ‘ 𝑊 )
		blocni.j	⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
		blocni.k	⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
		blocni.4	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
		blocni.5	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
		blocni.u	⊢ 𝑈 ∈ NrmCVec
		blocni.w	⊢ 𝑊 ∈ NrmCVec
		blocni.l	⊢ 𝑇 ∈ 𝐿
		lnocni.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	Assertion	lnocni	⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝑇 ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		blocni.8	⊢ 𝐶 = ( IndMet ‘ 𝑈 )
2		blocni.d	⊢ 𝐷 = ( IndMet ‘ 𝑊 )
3		blocni.j	⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
4		blocni.k	⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
5		blocni.4	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
6		blocni.5	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
7		blocni.u	⊢ 𝑈 ∈ NrmCVec
8		blocni.w	⊢ 𝑊 ∈ NrmCVec
9		blocni.l	⊢ 𝑇 ∈ 𝐿
10		lnocni.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
11	1 2 3 4 5 6 7 8 9 10	blocnilem	⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝑇 ∈ 𝐵 )
12	1 2 3 4 5 6 7 8 9	blocni	⊢ ( 𝑇 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝑇 ∈ 𝐵 )
13	11 12	sylibr	⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝑇 ∈ ( 𝐽 Cn 𝐾 ) )