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 𝑋 = ( BaseSet ‘ 𝑈 )
ubth.2 𝑁 = ( normCV𝑊 )
ubth.3 𝑀 = ( 𝑈 normOpOLD 𝑊 )
Assertion ubth ( ( 𝑈 ∈ CBan ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ⊆ ( 𝑈 BLnOp 𝑊 ) ) → ( ∀ 𝑥𝑋𝑐 ∈ ℝ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡𝑇 ( 𝑀𝑡 ) ≤ 𝑑 ) )

Proof

Step Hyp Ref Expression
1 ubth.1 𝑋 = ( BaseSet ‘ 𝑈 )
2 ubth.2 𝑁 = ( normCV𝑊 )
3 ubth.3 𝑀 = ( 𝑈 normOpOLD 𝑊 )
4 oveq1 ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝑈 BLnOp 𝑊 ) = ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) BLnOp 𝑊 ) )
5 4 sseq2d ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝑇 ⊆ ( 𝑈 BLnOp 𝑊 ) ↔ 𝑇 ⊆ ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) BLnOp 𝑊 ) ) )
6 fveq2 ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
7 1 6 syl5eq ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → 𝑋 = ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
8 7 raleqdv ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ∀ 𝑥𝑋𝑐 ∈ ℝ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 ↔ ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∃ 𝑐 ∈ ℝ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 ) )
9 oveq1 ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝑈 normOpOLD 𝑊 ) = ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) normOpOLD 𝑊 ) )
10 3 9 syl5eq ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → 𝑀 = ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) normOpOLD 𝑊 ) )
11 10 fveq1d ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝑀𝑡 ) = ( ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) normOpOLD 𝑊 ) ‘ 𝑡 ) )
12 11 breq1d ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( 𝑀𝑡 ) ≤ 𝑑 ↔ ( ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) )
13 12 rexralbidv ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ∃ 𝑑 ∈ ℝ ∀ 𝑡𝑇 ( 𝑀𝑡 ) ≤ 𝑑 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡𝑇 ( ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) )
14 8 13 bibi12d ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( ∀ 𝑥𝑋𝑐 ∈ ℝ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡𝑇 ( 𝑀𝑡 ) ≤ 𝑑 ) ↔ ( ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∃ 𝑐 ∈ ℝ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡𝑇 ( ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) )
15 5 14 imbi12d ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( 𝑇 ⊆ ( 𝑈 BLnOp 𝑊 ) → ( ∀ 𝑥𝑋𝑐 ∈ ℝ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡𝑇 ( 𝑀𝑡 ) ≤ 𝑑 ) ) ↔ ( 𝑇 ⊆ ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) BLnOp 𝑊 ) → ( ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∃ 𝑐 ∈ ℝ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡𝑇 ( ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) ) )
16 oveq2 ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) BLnOp 𝑊 ) = ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) BLnOp if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
17 16 sseq2d ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝑇 ⊆ ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) BLnOp 𝑊 ) ↔ 𝑇 ⊆ ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) BLnOp if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) )
18 fveq2 ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( normCV𝑊 ) = ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
19 2 18 syl5eq ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → 𝑁 = ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
20 19 fveq1d ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝑁 ‘ ( 𝑡𝑥 ) ) = ( ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ ( 𝑡𝑥 ) ) )
21 20 breq1d ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 ↔ ( ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 ) )
22 21 rexralbidv ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑐 ∈ ℝ ∀ 𝑡𝑇 ( ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 ) )
23 22 ralbidv ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∃ 𝑐 ∈ ℝ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 ↔ ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∃ 𝑐 ∈ ℝ ∀ 𝑡𝑇 ( ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 ) )
24 oveq2 ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) normOpOLD 𝑊 ) = ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) normOpOLD if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
25 24 fveq1d ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) normOpOLD 𝑊 ) ‘ 𝑡 ) = ( ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) normOpOLD if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ 𝑡 ) )
26 25 breq1d ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ↔ ( ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) normOpOLD if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ 𝑡 ) ≤ 𝑑 ) )
27 26 rexralbidv ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ∃ 𝑑 ∈ ℝ ∀ 𝑡𝑇 ( ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡𝑇 ( ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) normOpOLD if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ 𝑡 ) ≤ 𝑑 ) )
28 23 27 bibi12d ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∃ 𝑐 ∈ ℝ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡𝑇 ( ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ↔ ( ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∃ 𝑐 ∈ ℝ ∀ 𝑡𝑇 ( ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡𝑇 ( ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) normOpOLD if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ 𝑡 ) ≤ 𝑑 ) ) )
29 17 28 imbi12d ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( 𝑇 ⊆ ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) BLnOp 𝑊 ) → ( ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∃ 𝑐 ∈ ℝ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡𝑇 ( ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) ↔ ( 𝑇 ⊆ ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) BLnOp if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) → ( ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∃ 𝑐 ∈ ℝ ∀ 𝑡𝑇 ( ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡𝑇 ( ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) normOpOLD if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ 𝑡 ) ≤ 𝑑 ) ) ) )
30 eqid ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
31 eqid ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
32 eqid ( IndMet ‘ if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( IndMet ‘ if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
33 eqid ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) = ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
34 eqid ⟨ ⟨ + , · ⟩ , abs ⟩ = ⟨ ⟨ + , · ⟩ , abs ⟩
35 34 cnbn ⟨ ⟨ + , · ⟩ , abs ⟩ ∈ CBan
36 35 elimel if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ∈ CBan
37 elimnvu if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ∈ NrmCVec
38 id ( 𝑇 ⊆ ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) BLnOp if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) → 𝑇 ⊆ ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) BLnOp if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
39 30 31 32 33 36 37 38 ubthlem3 ( 𝑇 ⊆ ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) BLnOp if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) → ( ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∃ 𝑐 ∈ ℝ ∀ 𝑡𝑇 ( ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡𝑇 ( ( if ( 𝑈 ∈ CBan , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) normOpOLD if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ‘ 𝑡 ) ≤ 𝑑 ) )
40 15 29 39 dedth2h ( ( 𝑈 ∈ CBan ∧ 𝑊 ∈ NrmCVec ) → ( 𝑇 ⊆ ( 𝑈 BLnOp 𝑊 ) → ( ∀ 𝑥𝑋𝑐 ∈ ℝ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡𝑇 ( 𝑀𝑡 ) ≤ 𝑑 ) ) )
41 40 3impia ( ( 𝑈 ∈ CBan ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ⊆ ( 𝑈 BLnOp 𝑊 ) ) → ( ∀ 𝑥𝑋𝑐 ∈ ℝ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡𝑇 ( 𝑀𝑡 ) ≤ 𝑑 ) )