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

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 eqtrid ⊢ ( 𝑈 = 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 eqtrid ⊢ ( 𝑈 = 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 eqtrid ⊢ ( 𝑊 = 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 𝑊 ) ) → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑀 ‘ 𝑡 ) ≤ 𝑑 ) )