Metamath Proof Explorer

Theorem nmounbseqi

Description: An unbounded operator determines an unbounded sequence. (Contributed by NM, 11-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 nmounbseqi ⊢ T : X ⟶ Y ∧ N ⁡ T = +∞ → ∃ f f : ℕ ⟶ X ∧ ∀ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 ∧ k < M ⁡ T ⁡ f ⁡ k

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 1 2 3 4 5 6 7 nmounbi ⊢ T : X ⟶ Y → N ⁡ T = +∞ ↔ ∀ k ∈ ℝ ∃ y ∈ X L ⁡ y ≤ 1 ∧ k < M ⁡ T ⁡ y
9 8 biimpa ⊢ T : X ⟶ Y ∧ N ⁡ T = +∞ → ∀ k ∈ ℝ ∃ y ∈ X L ⁡ y ≤ 1 ∧ k < M ⁡ T ⁡ y
10 nnre ⊢ k ∈ ℕ → k ∈ ℝ
11 10 imim1i ⊢ k ∈ ℝ → ∃ y ∈ X L ⁡ y ≤ 1 ∧ k < M ⁡ T ⁡ y → k ∈ ℕ → ∃ y ∈ X L ⁡ y ≤ 1 ∧ k < M ⁡ T ⁡ y
12 11 ralimi2 ⊢ ∀ k ∈ ℝ ∃ y ∈ X L ⁡ y ≤ 1 ∧ k < M ⁡ T ⁡ y → ∀ k ∈ ℕ ∃ y ∈ X L ⁡ y ≤ 1 ∧ k < M ⁡ T ⁡ y
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 breq2d ⊢ y = f ⁡ k → k < M ⁡ T ⁡ y ↔ k < M ⁡ T ⁡ f ⁡ k
19 16 18 anbi12d ⊢ y = f ⁡ k → L ⁡ y ≤ 1 ∧ k < M ⁡ T ⁡ y ↔ L ⁡ f ⁡ k ≤ 1 ∧ k < M ⁡ T ⁡ f ⁡ k
20 13 14 19 axcc4 ⊢ ∀ k ∈ ℕ ∃ y ∈ X L ⁡ y ≤ 1 ∧ k < M ⁡ T ⁡ y → ∃ f f : ℕ ⟶ X ∧ ∀ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 ∧ k < M ⁡ T ⁡ f ⁡ k
21 9 12 20 3syl ⊢ T : X ⟶ Y ∧ N ⁡ T = +∞ → ∃ f f : ℕ ⟶ X ∧ ∀ k ∈ ℕ L ⁡ f ⁡ k ≤ 1 ∧ k < M ⁡ T ⁡ f ⁡ k