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=normCV⁡U
nmoubi.m ⊢M=normCV⁡W
nmoubi.3 ⊢N=UnormOpOLDW
nmoubi.u ⊢U∈NrmCVec
nmoubi.w ⊢W∈NrmCVec
Assertion nmounbseqi ⊢T:X⟶Y∧N⁡T=+∞→∃ff:ℕ⟶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=normCV⁡U
4 nmoubi.m ⊢M=normCV⁡W
5 nmoubi.3 ⊢N=UnormOpOLDW
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∈XL⁡y≤1∧k<M⁡T⁡y
9 8 biimpa ⊢T:X⟶Y∧N⁡T=+∞→∀k∈ℝ∃y∈XL⁡y≤1∧k<M⁡T⁡y
10 nnre ⊢k∈ℕ→k∈ℝ
11 10 imim1i ⊢k∈ℝ→∃y∈XL⁡y≤1∧k<M⁡T⁡y→k∈ℕ→∃y∈XL⁡y≤1∧k<M⁡T⁡y
12 11 ralimi2 ⊢∀k∈ℝ∃y∈XL⁡y≤1∧k<M⁡T⁡y→∀k∈ℕ∃y∈XL⁡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∈XL⁡y≤1∧k<M⁡T⁡y→∃ff:ℕ⟶X∧∀k∈ℕL⁡f⁡k≤1∧k<M⁡T⁡f⁡k
21 9 12 20 3syl ⊢T:X⟶Y∧N⁡T=+∞→∃ff:ℕ⟶X∧∀k∈ℕL⁡f⁡k≤1∧k<M⁡T⁡f⁡k