Theorem blocn

Description: A linear operator is continuous iff it is bounded. Theorem 2.7-9(a) of Kreyszig p. 97. (Contributed by NM, 25-Dec-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	blocn.8	⊢ 𝐶 = ( IndMet ‘ 𝑈 )
	blocn.d	⊢ 𝐷 = ( IndMet ‘ 𝑊 )
	blocn.j	⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
	blocn.k	⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
	blocn.5	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
	blocn.u	⊢ 𝑈 ∈ NrmCVec
	blocn.w	⊢ 𝑊 ∈ NrmCVec
	blocn.4	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
Assertion	blocn	⊢ ( 𝑇 ∈ 𝐿 → ( 𝑇 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝑇 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		blocn.8	⊢ 𝐶 = ( IndMet ‘ 𝑈 )
2		blocn.d	⊢ 𝐷 = ( IndMet ‘ 𝑊 )
3		blocn.j	⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
4		blocn.k	⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
5		blocn.5	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
6		blocn.u	⊢ 𝑈 ∈ NrmCVec
7		blocn.w	⊢ 𝑊 ∈ NrmCVec
8		blocn.4	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
9		eleq1	⊢ ( 𝑇 = if ( 𝑇 ∈ 𝐿 , 𝑇 , ( 𝑈 0op 𝑊 ) ) → ( 𝑇 ∈ ( 𝐽 Cn 𝐾 ) ↔ if ( 𝑇 ∈ 𝐿 , 𝑇 , ( 𝑈 0op 𝑊 ) ) ∈ ( 𝐽 Cn 𝐾 ) ) )
10		eleq1	⊢ ( 𝑇 = if ( 𝑇 ∈ 𝐿 , 𝑇 , ( 𝑈 0op 𝑊 ) ) → ( 𝑇 ∈ 𝐵 ↔ if ( 𝑇 ∈ 𝐿 , 𝑇 , ( 𝑈 0op 𝑊 ) ) ∈ 𝐵 ) )
11	9 10	bibi12d	⊢ ( 𝑇 = if ( 𝑇 ∈ 𝐿 , 𝑇 , ( 𝑈 0op 𝑊 ) ) → ( ( 𝑇 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝑇 ∈ 𝐵 ) ↔ ( if ( 𝑇 ∈ 𝐿 , 𝑇 , ( 𝑈 0op 𝑊 ) ) ∈ ( 𝐽 Cn 𝐾 ) ↔ if ( 𝑇 ∈ 𝐿 , 𝑇 , ( 𝑈 0op 𝑊 ) ) ∈ 𝐵 ) ) )
12		eqid	⊢ ( 𝑈 0op 𝑊 ) = ( 𝑈 0op 𝑊 )
13	12 8	0lno	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑈 0op 𝑊 ) ∈ 𝐿 )
14	6 7 13	mp2an	⊢ ( 𝑈 0op 𝑊 ) ∈ 𝐿
15	14	elimel	⊢ if ( 𝑇 ∈ 𝐿 , 𝑇 , ( 𝑈 0op 𝑊 ) ) ∈ 𝐿
16	1 2 3 4 8 5 6 7 15	blocni	⊢ ( if ( 𝑇 ∈ 𝐿 , 𝑇 , ( 𝑈 0op 𝑊 ) ) ∈ ( 𝐽 Cn 𝐾 ) ↔ if ( 𝑇 ∈ 𝐿 , 𝑇 , ( 𝑈 0op 𝑊 ) ) ∈ 𝐵 )
17	11 16	dedth	⊢ ( 𝑇 ∈ 𝐿 → ( 𝑇 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝑇 ∈ 𝐵 ) )