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

Metamath Proof Explorer

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 𝐾 ) ↔ 𝑇 ∈ 𝐵 ) )