Metamath Proof Explorer

Theorem nmobndseqi

Description: A bounded sequence determines a bounded operator. (Contributed by NM, 18-Jan-2008) (Revised by Mario Carneiro, 7-Apr-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nmoubi.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nmoubi.y ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
nmoubi.l ⊢ 𝐿 = ( normCV ‘ 𝑈 )
nmoubi.m ⊢ 𝑀 = ( normCV ‘ 𝑊 )
nmoubi.3 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
nmoubi.u ⊢ 𝑈 ∈ NrmCVec
nmoubi.w ⊢ 𝑊 ∈ NrmCVec
Assertion nmobndseqi ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 ) → ∃ 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) → ( 𝑁 ‘ 𝑇 ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 nmoubi.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nmoubi.y ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3 nmoubi.l ⊢ 𝐿 = ( normCV ‘ 𝑈 )
4 nmoubi.m ⊢ 𝑀 = ( normCV ‘ 𝑊 )
5 nmoubi.3 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
6 nmoubi.u ⊢ 𝑈 ∈ NrmCVec
7 nmoubi.w ⊢ 𝑊 ∈ NrmCVec
8 impexp ⊢ ( ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 ) → ∃ 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ↔ ( 𝑓 : ℕ ⟶ 𝑋 → ( ∀ 𝑘 ∈ ℕ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ∃ 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) )
9 r19.35 ⊢ ( ∃ 𝑘 ∈ ℕ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ↔ ( ∀ 𝑘 ∈ ℕ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ∃ 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) )
10 9 imbi2i ⊢ ( ( 𝑓 : ℕ ⟶ 𝑋 → ∃ 𝑘 ∈ ℕ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) ↔ ( 𝑓 : ℕ ⟶ 𝑋 → ( ∀ 𝑘 ∈ ℕ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ∃ 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) )
11 8 10 bitr4i ⊢ ( ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 ) → ∃ 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ↔ ( 𝑓 : ℕ ⟶ 𝑋 → ∃ 𝑘 ∈ ℕ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) )
12 11 albii ⊢ ( ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 ) → ∃ 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ↔ ∀ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 → ∃ 𝑘 ∈ ℕ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) )
13 1 fvexi ⊢ 𝑋 ∈ V
14 nnenom ⊢ ℕ ≈ ω
15 fveq2 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑘 ) → ( 𝐿 ‘ 𝑦 ) = ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) )
16 15 breq1d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑘 ) → ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ↔ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 ) )
17 2fveq3 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑘 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) )
18 17 breq1d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑘 ) → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ↔ ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) )
19 16 18 imbi12d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑘 ) → ( ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) ↔ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) )
20 19 notbid ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑘 ) → ( ¬ ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) ↔ ¬ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) )
21 13 14 20 axcc4 ⊢ ( ∀ 𝑘 ∈ ℕ ∃ 𝑦 ∈ 𝑋 ¬ ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ¬ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) )
22 21 con3i ⊢ ( ¬ ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ¬ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) → ¬ ∀ 𝑘 ∈ ℕ ∃ 𝑦 ∈ 𝑋 ¬ ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) )
23 dfrex2 ⊢ ( ∃ 𝑘 ∈ ℕ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ↔ ¬ ∀ 𝑘 ∈ ℕ ¬ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) )
24 23 imbi2i ⊢ ( ( 𝑓 : ℕ ⟶ 𝑋 → ∃ 𝑘 ∈ ℕ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) ↔ ( 𝑓 : ℕ ⟶ 𝑋 → ¬ ∀ 𝑘 ∈ ℕ ¬ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) )
25 24 albii ⊢ ( ∀ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 → ∃ 𝑘 ∈ ℕ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) ↔ ∀ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 → ¬ ∀ 𝑘 ∈ ℕ ¬ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) )
26 alinexa ⊢ ( ∀ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 → ¬ ∀ 𝑘 ∈ ℕ ¬ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) ↔ ¬ ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ¬ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) )
27 25 26 bitri ⊢ ( ∀ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 → ∃ 𝑘 ∈ ℕ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) ↔ ¬ ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ¬ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) )
28 dfral2 ⊢ ( ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) ↔ ¬ ∃ 𝑦 ∈ 𝑋 ¬ ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) )
29 28 rexbii ⊢ ( ∃ 𝑘 ∈ ℕ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) ↔ ∃ 𝑘 ∈ ℕ ¬ ∃ 𝑦 ∈ 𝑋 ¬ ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) )
30 rexnal ⊢ ( ∃ 𝑘 ∈ ℕ ¬ ∃ 𝑦 ∈ 𝑋 ¬ ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) ↔ ¬ ∀ 𝑘 ∈ ℕ ∃ 𝑦 ∈ 𝑋 ¬ ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) )
31 29 30 bitri ⊢ ( ∃ 𝑘 ∈ ℕ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) ↔ ¬ ∀ 𝑘 ∈ ℕ ∃ 𝑦 ∈ 𝑋 ¬ ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) )
32 22 27 31 3imtr4i ⊢ ( ∀ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 → ∃ 𝑘 ∈ ℕ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) → ∃ 𝑘 ∈ ℕ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) )
33 nnre ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
34 33 anim1i ⊢ ( ( 𝑘 ∈ ℕ ∧ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) ) → ( 𝑘 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) ) )
35 34 reximi2 ⊢ ( ∃ 𝑘 ∈ ℕ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) )
36 32 35 syl ⊢ ( ∀ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 → ∃ 𝑘 ∈ ℕ ( ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) )
37 12 36 sylbi ⊢ ( ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 ) → ∃ 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) )
38 1 2 3 4 5 6 7 nmobndi ⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑘 ) ) )
39 37 38 imbitrrid ⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 ) → ∃ 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) → ( 𝑁 ‘ 𝑇 ) ∈ ℝ ) )
40 39 imp ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ ∀ 𝑘 ∈ ℕ ( 𝐿 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ 1 ) → ∃ 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑇 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ≤ 𝑘 ) ) → ( 𝑁 ‘ 𝑇 ) ∈ ℝ )