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 ⊢ X = BaseSet ⁡ U
nmoubi.y ⊢ Y = BaseSet ⁡ W
nmoubi.l ⊢ L = norm CV ⁡ U
nmoubi.m ⊢ M = norm CV ⁡ W
nmoubi.3 ⊢ N = U normOp OLD W
nmoubi.u ⊢ U ∈ NrmCVec
nmoubi.w ⊢ W ∈ NrmCVec
Assertion nmobndseqi ⊢ T : X ⟶ Y ∧ ∀ f f : ℕ ⟶ X ∧ ∀ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 → ∃ k ∈ ℕ M ⁡ T ⁡ f ⁡ k ≤ k → N ⁡ T ∈ ℝ

Proof

Step Hyp Ref Expression
1 nmoubi.1 ⊢ X = BaseSet ⁡ U
2 nmoubi.y ⊢ Y = BaseSet ⁡ W
3 nmoubi.l ⊢ L = norm CV ⁡ U
4 nmoubi.m ⊢ M = norm CV ⁡ W
5 nmoubi.3 ⊢ N = U normOp OLD W
6 nmoubi.u ⊢ U ∈ NrmCVec
7 nmoubi.w ⊢ W ∈ NrmCVec
8 impexp ⊢ f : ℕ ⟶ X ∧ ∀ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 → ∃ k ∈ ℕ M ⁡ T ⁡ f ⁡ k ≤ k ↔ f : ℕ ⟶ X → ∀ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 → ∃ k ∈ ℕ M ⁡ T ⁡ f ⁡ k ≤ k
9 r19.35 ⊢ ∃ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 → M ⁡ T ⁡ f ⁡ k ≤ k ↔ ∀ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 → ∃ k ∈ ℕ M ⁡ T ⁡ f ⁡ k ≤ k
10 9 imbi2i ⊢ f : ℕ ⟶ X → ∃ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 → M ⁡ T ⁡ f ⁡ k ≤ k ↔ f : ℕ ⟶ X → ∀ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 → ∃ k ∈ ℕ M ⁡ T ⁡ f ⁡ k ≤ k
11 8 10 bitr4i ⊢ f : ℕ ⟶ X ∧ ∀ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 → ∃ k ∈ ℕ M ⁡ T ⁡ f ⁡ k ≤ k ↔ f : ℕ ⟶ X → ∃ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 → M ⁡ T ⁡ f ⁡ k ≤ k
12 11 albii ⊢ ∀ f f : ℕ ⟶ X ∧ ∀ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 → ∃ k ∈ ℕ M ⁡ T ⁡ f ⁡ k ≤ k ↔ ∀ f f : ℕ ⟶ X → ∃ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 → M ⁡ T ⁡ f ⁡ k ≤ k
13 1 fvexi ⊢ X ∈ V
14 nnenom ⊢ ℕ ≈ ω
15 fveq2 ⊢ y = f ⁡ k → L ⁡ y = L ⁡ f ⁡ k
16 15 breq1d ⊢ y = f ⁡ k → L ⁡ y ≤ 1 ↔ L ⁡ f ⁡ k ≤ 1
17 2fveq3 ⊢ y = f ⁡ k → M ⁡ T ⁡ y = M ⁡ T ⁡ f ⁡ k
18 17 breq1d ⊢ y = f ⁡ k → M ⁡ T ⁡ y ≤ k ↔ M ⁡ T ⁡ f ⁡ k ≤ k
19 16 18 imbi12d ⊢ y = f ⁡ k → L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ k ↔ L ⁡ f ⁡ k ≤ 1 → M ⁡ T ⁡ f ⁡ k ≤ k
20 19 notbid ⊢ y = f ⁡ k → ¬ L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ k ↔ ¬ L ⁡ f ⁡ k ≤ 1 → M ⁡ T ⁡ f ⁡ k ≤ k
21 13 14 20 axcc4 ⊢ ∀ k ∈ ℕ ∃ y ∈ X ¬ L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ k → ∃ f f : ℕ ⟶ X ∧ ∀ k ∈ ℕ ¬ L ⁡ f ⁡ k ≤ 1 → M ⁡ T ⁡ f ⁡ k ≤ k
22 21 con3i ⊢ ¬ ∃ f f : ℕ ⟶ X ∧ ∀ k ∈ ℕ ¬ L ⁡ f ⁡ k ≤ 1 → M ⁡ T ⁡ f ⁡ k ≤ k → ¬ ∀ k ∈ ℕ ∃ y ∈ X ¬ L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ k
23 dfrex2 ⊢ ∃ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 → M ⁡ T ⁡ f ⁡ k ≤ k ↔ ¬ ∀ k ∈ ℕ ¬ L ⁡ f ⁡ k ≤ 1 → M ⁡ T ⁡ f ⁡ k ≤ k
24 23 imbi2i ⊢ f : ℕ ⟶ X → ∃ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 → M ⁡ T ⁡ f ⁡ k ≤ k ↔ f : ℕ ⟶ X → ¬ ∀ k ∈ ℕ ¬ L ⁡ f ⁡ k ≤ 1 → M ⁡ T ⁡ f ⁡ k ≤ k
25 24 albii ⊢ ∀ f f : ℕ ⟶ X → ∃ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 → M ⁡ T ⁡ f ⁡ k ≤ k ↔ ∀ f f : ℕ ⟶ X → ¬ ∀ k ∈ ℕ ¬ L ⁡ f ⁡ k ≤ 1 → M ⁡ T ⁡ f ⁡ k ≤ k
26 alinexa ⊢ ∀ f f : ℕ ⟶ X → ¬ ∀ k ∈ ℕ ¬ L ⁡ f ⁡ k ≤ 1 → M ⁡ T ⁡ f ⁡ k ≤ k ↔ ¬ ∃ f f : ℕ ⟶ X ∧ ∀ k ∈ ℕ ¬ L ⁡ f ⁡ k ≤ 1 → M ⁡ T ⁡ f ⁡ k ≤ k
27 25 26 bitri ⊢ ∀ f f : ℕ ⟶ X → ∃ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 → M ⁡ T ⁡ f ⁡ k ≤ k ↔ ¬ ∃ f f : ℕ ⟶ X ∧ ∀ k ∈ ℕ ¬ L ⁡ f ⁡ k ≤ 1 → M ⁡ T ⁡ f ⁡ k ≤ k
28 dfral2 ⊢ ∀ y ∈ X L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ k ↔ ¬ ∃ y ∈ X ¬ L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ k
29 28 rexbii ⊢ ∃ k ∈ ℕ ∀ y ∈ X L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ k ↔ ∃ k ∈ ℕ ¬ ∃ y ∈ X ¬ L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ k
30 rexnal ⊢ ∃ k ∈ ℕ ¬ ∃ y ∈ X ¬ L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ k ↔ ¬ ∀ k ∈ ℕ ∃ y ∈ X ¬ L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ k
31 29 30 bitri ⊢ ∃ k ∈ ℕ ∀ y ∈ X L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ k ↔ ¬ ∀ k ∈ ℕ ∃ y ∈ X ¬ L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ k
32 22 27 31 3imtr4i ⊢ ∀ f f : ℕ ⟶ X → ∃ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 → M ⁡ T ⁡ f ⁡ k ≤ k → ∃ k ∈ ℕ ∀ y ∈ X L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ k
33 nnre ⊢ k ∈ ℕ → k ∈ ℝ
34 33 anim1i ⊢ k ∈ ℕ ∧ ∀ y ∈ X L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ k → k ∈ ℝ ∧ ∀ y ∈ X L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ k
35 34 reximi2 ⊢ ∃ k ∈ ℕ ∀ y ∈ X L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ k → ∃ k ∈ ℝ ∀ y ∈ X L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ k
36 32 35 syl ⊢ ∀ f f : ℕ ⟶ X → ∃ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 → M ⁡ T ⁡ f ⁡ k ≤ k → ∃ k ∈ ℝ ∀ y ∈ X L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ k
37 12 36 sylbi ⊢ ∀ f f : ℕ ⟶ X ∧ ∀ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 → ∃ k ∈ ℕ M ⁡ T ⁡ f ⁡ k ≤ k → ∃ k ∈ ℝ ∀ y ∈ X L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ k
38 1 2 3 4 5 6 7 nmobndi ⊢ T : X ⟶ Y → N ⁡ T ∈ ℝ ↔ ∃ k ∈ ℝ ∀ y ∈ X L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ k
39 37 38 syl5ibr ⊢ T : X ⟶ Y → ∀ f f : ℕ ⟶ X ∧ ∀ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 → ∃ k ∈ ℕ M ⁡ T ⁡ f ⁡ k ≤ k → N ⁡ T ∈ ℝ
40 39 imp ⊢ T : X ⟶ Y ∧ ∀ f f : ℕ ⟶ X ∧ ∀ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 → ∃ k ∈ ℕ M ⁡ T ⁡ f ⁡ k ≤ k → N ⁡ T ∈ ℝ