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 ⊢ C = IndMet ⁡ U
blocn.d ⊢ D = IndMet ⁡ W
blocn.j ⊢ J = MetOpen ⁡ C
blocn.k ⊢ K = MetOpen ⁡ D
blocn.5 ⊢ B = U BLnOp W
blocn.u ⊢ U ∈ NrmCVec
blocn.w ⊢ W ∈ NrmCVec
blocn.4 ⊢ L = U LnOp W
Assertion blocn ⊢ T ∈ L → T ∈ J Cn K ↔ T ∈ B

Proof

Step Hyp Ref Expression
1 blocn.8 ⊢ C = IndMet ⁡ U
2 blocn.d ⊢ D = IndMet ⁡ W
3 blocn.j ⊢ J = MetOpen ⁡ C
4 blocn.k ⊢ K = MetOpen ⁡ D
5 blocn.5 ⊢ B = U BLnOp W
6 blocn.u ⊢ U ∈ NrmCVec
7 blocn.w ⊢ W ∈ NrmCVec
8 blocn.4 ⊢ L = U LnOp W
9 eleq1 ⊢ T = if T ∈ L T U 0 op W → T ∈ J Cn K ↔ if T ∈ L T U 0 op W ∈ J Cn K
10 eleq1 ⊢ T = if T ∈ L T U 0 op W → T ∈ B ↔ if T ∈ L T U 0 op W ∈ B
11 9 10 bibi12d ⊢ T = if T ∈ L T U 0 op W → T ∈ J Cn K ↔ T ∈ B ↔ if T ∈ L T U 0 op W ∈ J Cn K ↔ if T ∈ L T U 0 op W ∈ B
12 eqid ⊢ U 0 op W = U 0 op W
13 12 8 0lno ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → U 0 op W ∈ L
14 6 7 13 mp2an ⊢ U 0 op W ∈ L
15 14 elimel ⊢ if T ∈ L T U 0 op W ∈ L
16 1 2 3 4 8 5 6 7 15 blocni ⊢ if T ∈ L T U 0 op W ∈ J Cn K ↔ if T ∈ L T U 0 op W ∈ B
17 11 16 dedth ⊢ T ∈ L → T ∈ J Cn K ↔ T ∈ B