Metamath Proof Explorer

Theorem ubth

Description: Uniform Boundedness Theorem, also called the Banach-Steinhaus Theorem. Let T be a collection of bounded linear operators on a Banach space. If, for every vector x , the norms of the operators' values are bounded, then the operators' norms are also bounded. Theorem 4.7-3 of Kreyszig p. 249. See also http://en.wikipedia.org/wiki/Uniform_boundedness_principle . (Contributed by NM, 7-Nov-2007) (Proof shortened by Mario Carneiro, 11-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses ubth.1 ⊢ X = BaseSet ⁡ U
ubth.2 ⊢ N = norm CV ⁡ W
ubth.3 ⊢ M = U normOp OLD W
Assertion ubth ⊢ U ∈ CBan ∧ W ∈ NrmCVec ∧ T ⊆ U BLnOp W → ∀ x ∈ X ∃ c ∈ ℝ ∀ t ∈ T N ⁡ t ⁡ x ≤ c ↔ ∃ d ∈ ℝ ∀ t ∈ T M ⁡ t ≤ d

Proof

Step Hyp Ref Expression
1 ubth.1 ⊢ X = BaseSet ⁡ U
2 ubth.2 ⊢ N = norm CV ⁡ W
3 ubth.3 ⊢ M = U normOp OLD W
4 oveq1 ⊢ U = if U ∈ CBan U + × abs → U BLnOp W = if U ∈ CBan U + × abs BLnOp W
5 4 sseq2d ⊢ U = if U ∈ CBan U + × abs → T ⊆ U BLnOp W ↔ T ⊆ if U ∈ CBan U + × abs BLnOp W
6 fveq2 ⊢ U = if U ∈ CBan U + × abs → BaseSet ⁡ U = BaseSet ⁡ if U ∈ CBan U + × abs
7 1 6 eqtrid ⊢ U = if U ∈ CBan U + × abs → X = BaseSet ⁡ if U ∈ CBan U + × abs
8 7 raleqdv ⊢ U = if U ∈ CBan U + × abs → ∀ x ∈ X ∃ c ∈ ℝ ∀ t ∈ T N ⁡ t ⁡ x ≤ c ↔ ∀ x ∈ BaseSet ⁡ if U ∈ CBan U + × abs ∃ c ∈ ℝ ∀ t ∈ T N ⁡ t ⁡ x ≤ c
9 oveq1 ⊢ U = if U ∈ CBan U + × abs → U normOp OLD W = if U ∈ CBan U + × abs normOp OLD W
10 3 9 eqtrid ⊢ U = if U ∈ CBan U + × abs → M = if U ∈ CBan U + × abs normOp OLD W
11 10 fveq1d ⊢ U = if U ∈ CBan U + × abs → M ⁡ t = if U ∈ CBan U + × abs normOp OLD W ⁡ t
12 11 breq1d ⊢ U = if U ∈ CBan U + × abs → M ⁡ t ≤ d ↔ if U ∈ CBan U + × abs normOp OLD W ⁡ t ≤ d
13 12 rexralbidv ⊢ U = if U ∈ CBan U + × abs → ∃ d ∈ ℝ ∀ t ∈ T M ⁡ t ≤ d ↔ ∃ d ∈ ℝ ∀ t ∈ T if U ∈ CBan U + × abs normOp OLD W ⁡ t ≤ d
14 8 13 bibi12d ⊢ U = if U ∈ CBan U + × abs → ∀ x ∈ X ∃ c ∈ ℝ ∀ t ∈ T N ⁡ t ⁡ x ≤ c ↔ ∃ d ∈ ℝ ∀ t ∈ T M ⁡ t ≤ d ↔ ∀ x ∈ BaseSet ⁡ if U ∈ CBan U + × abs ∃ c ∈ ℝ ∀ t ∈ T N ⁡ t ⁡ x ≤ c ↔ ∃ d ∈ ℝ ∀ t ∈ T if U ∈ CBan U + × abs normOp OLD W ⁡ t ≤ d
15 5 14 imbi12d ⊢ U = if U ∈ CBan U + × abs → T ⊆ U BLnOp W → ∀ x ∈ X ∃ c ∈ ℝ ∀ t ∈ T N ⁡ t ⁡ x ≤ c ↔ ∃ d ∈ ℝ ∀ t ∈ T M ⁡ t ≤ d ↔ T ⊆ if U ∈ CBan U + × abs BLnOp W → ∀ x ∈ BaseSet ⁡ if U ∈ CBan U + × abs ∃ c ∈ ℝ ∀ t ∈ T N ⁡ t ⁡ x ≤ c ↔ ∃ d ∈ ℝ ∀ t ∈ T if U ∈ CBan U + × abs normOp OLD W ⁡ t ≤ d
16 oveq2 ⊢ W = if W ∈ NrmCVec W + × abs → if U ∈ CBan U + × abs BLnOp W = if U ∈ CBan U + × abs BLnOp if W ∈ NrmCVec W + × abs
17 16 sseq2d ⊢ W = if W ∈ NrmCVec W + × abs → T ⊆ if U ∈ CBan U + × abs BLnOp W ↔ T ⊆ if U ∈ CBan U + × abs BLnOp if W ∈ NrmCVec W + × abs
18 fveq2 ⊢ W = if W ∈ NrmCVec W + × abs → norm CV ⁡ W = norm CV ⁡ if W ∈ NrmCVec W + × abs
19 2 18 eqtrid ⊢ W = if W ∈ NrmCVec W + × abs → N = norm CV ⁡ if W ∈ NrmCVec W + × abs
20 19 fveq1d ⊢ W = if W ∈ NrmCVec W + × abs → N ⁡ t ⁡ x = norm CV ⁡ if W ∈ NrmCVec W + × abs ⁡ t ⁡ x
21 20 breq1d ⊢ W = if W ∈ NrmCVec W + × abs → N ⁡ t ⁡ x ≤ c ↔ norm CV ⁡ if W ∈ NrmCVec W + × abs ⁡ t ⁡ x ≤ c
22 21 rexralbidv ⊢ W = if W ∈ NrmCVec W + × abs → ∃ c ∈ ℝ ∀ t ∈ T N ⁡ t ⁡ x ≤ c ↔ ∃ c ∈ ℝ ∀ t ∈ T norm CV ⁡ if W ∈ NrmCVec W + × abs ⁡ t ⁡ x ≤ c
23 22 ralbidv ⊢ W = if W ∈ NrmCVec W + × abs → ∀ x ∈ BaseSet ⁡ if U ∈ CBan U + × abs ∃ c ∈ ℝ ∀ t ∈ T N ⁡ t ⁡ x ≤ c ↔ ∀ x ∈ BaseSet ⁡ if U ∈ CBan U + × abs ∃ c ∈ ℝ ∀ t ∈ T norm CV ⁡ if W ∈ NrmCVec W + × abs ⁡ t ⁡ x ≤ c
24 oveq2 ⊢ W = if W ∈ NrmCVec W + × abs → if U ∈ CBan U + × abs normOp OLD W = if U ∈ CBan U + × abs normOp OLD if W ∈ NrmCVec W + × abs
25 24 fveq1d ⊢ W = if W ∈ NrmCVec W + × abs → if U ∈ CBan U + × abs normOp OLD W ⁡ t = if U ∈ CBan U + × abs normOp OLD if W ∈ NrmCVec W + × abs ⁡ t
26 25 breq1d ⊢ W = if W ∈ NrmCVec W + × abs → if U ∈ CBan U + × abs normOp OLD W ⁡ t ≤ d ↔ if U ∈ CBan U + × abs normOp OLD if W ∈ NrmCVec W + × abs ⁡ t ≤ d
27 26 rexralbidv ⊢ W = if W ∈ NrmCVec W + × abs → ∃ d ∈ ℝ ∀ t ∈ T if U ∈ CBan U + × abs normOp OLD W ⁡ t ≤ d ↔ ∃ d ∈ ℝ ∀ t ∈ T if U ∈ CBan U + × abs normOp OLD if W ∈ NrmCVec W + × abs ⁡ t ≤ d
28 23 27 bibi12d ⊢ W = if W ∈ NrmCVec W + × abs → ∀ x ∈ BaseSet ⁡ if U ∈ CBan U + × abs ∃ c ∈ ℝ ∀ t ∈ T N ⁡ t ⁡ x ≤ c ↔ ∃ d ∈ ℝ ∀ t ∈ T if U ∈ CBan U + × abs normOp OLD W ⁡ t ≤ d ↔ ∀ x ∈ BaseSet ⁡ if U ∈ CBan U + × abs ∃ c ∈ ℝ ∀ t ∈ T norm CV ⁡ if W ∈ NrmCVec W + × abs ⁡ t ⁡ x ≤ c ↔ ∃ d ∈ ℝ ∀ t ∈ T if U ∈ CBan U + × abs normOp OLD if W ∈ NrmCVec W + × abs ⁡ t ≤ d
29 17 28 imbi12d ⊢ W = if W ∈ NrmCVec W + × abs → T ⊆ if U ∈ CBan U + × abs BLnOp W → ∀ x ∈ BaseSet ⁡ if U ∈ CBan U + × abs ∃ c ∈ ℝ ∀ t ∈ T N ⁡ t ⁡ x ≤ c ↔ ∃ d ∈ ℝ ∀ t ∈ T if U ∈ CBan U + × abs normOp OLD W ⁡ t ≤ d ↔ T ⊆ if U ∈ CBan U + × abs BLnOp if W ∈ NrmCVec W + × abs → ∀ x ∈ BaseSet ⁡ if U ∈ CBan U + × abs ∃ c ∈ ℝ ∀ t ∈ T norm CV ⁡ if W ∈ NrmCVec W + × abs ⁡ t ⁡ x ≤ c ↔ ∃ d ∈ ℝ ∀ t ∈ T if U ∈ CBan U + × abs normOp OLD if W ∈ NrmCVec W + × abs ⁡ t ≤ d
30 eqid ⊢ BaseSet ⁡ if U ∈ CBan U + × abs = BaseSet ⁡ if U ∈ CBan U + × abs
31 eqid ⊢ norm CV ⁡ if W ∈ NrmCVec W + × abs = norm CV ⁡ if W ∈ NrmCVec W + × abs
32 eqid ⊢ IndMet ⁡ if U ∈ CBan U + × abs = IndMet ⁡ if U ∈ CBan U + × abs
33 eqid ⊢ MetOpen ⁡ IndMet ⁡ if U ∈ CBan U + × abs = MetOpen ⁡ IndMet ⁡ if U ∈ CBan U + × abs
34 eqid ⊢ + × abs = + × abs
35 34 cnbn ⊢ + × abs ∈ CBan
36 35 elimel ⊢ if U ∈ CBan U + × abs ∈ CBan
37 elimnvu ⊢ if W ∈ NrmCVec W + × abs ∈ NrmCVec
38 id ⊢ T ⊆ if U ∈ CBan U + × abs BLnOp if W ∈ NrmCVec W + × abs → T ⊆ if U ∈ CBan U + × abs BLnOp if W ∈ NrmCVec W + × abs
39 30 31 32 33 36 37 38 ubthlem3 ⊢ T ⊆ if U ∈ CBan U + × abs BLnOp if W ∈ NrmCVec W + × abs → ∀ x ∈ BaseSet ⁡ if U ∈ CBan U + × abs ∃ c ∈ ℝ ∀ t ∈ T norm CV ⁡ if W ∈ NrmCVec W + × abs ⁡ t ⁡ x ≤ c ↔ ∃ d ∈ ℝ ∀ t ∈ T if U ∈ CBan U + × abs normOp OLD if W ∈ NrmCVec W + × abs ⁡ t ≤ d
40 15 29 39 dedth2h ⊢ U ∈ CBan ∧ W ∈ NrmCVec → T ⊆ U BLnOp W → ∀ x ∈ X ∃ c ∈ ℝ ∀ t ∈ T N ⁡ t ⁡ x ≤ c ↔ ∃ d ∈ ℝ ∀ t ∈ T M ⁡ t ≤ d
41 40 3impia ⊢ U ∈ CBan ∧ W ∈ NrmCVec ∧ T ⊆ U BLnOp W → ∀ x ∈ X ∃ c ∈ ℝ ∀ t ∈ T N ⁡ t ⁡ x ≤ c ↔ ∃ d ∈ ℝ ∀ t ∈ T M ⁡ t ≤ d