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