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=normCV⁡U
nmoubi.m ⊢M=normCV⁡W
nmoubi.3 ⊢N=UnormOpOLDW
nmoubi.u ⊢U∈NrmCVec
nmoubi.w ⊢W∈NrmCVec
Assertion nmobndseqi ⊢T:X⟶Y∧∀ff:ℕ⟶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=normCV⁡U
4 nmoubi.m ⊢M=normCV⁡W
5 nmoubi.3 ⊢N=UnormOpOLDW
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 ⊢∀ff:ℕ⟶X∧∀k∈ℕL⁡f⁡k≤1→∃k∈ℕM⁡T⁡f⁡k≤k↔∀ff:ℕ⟶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→∃ff:ℕ⟶X∧∀k∈ℕ¬L⁡f⁡k≤1→M⁡T⁡f⁡k≤k
22 21 con3i ⊢¬∃ff:ℕ⟶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 ⊢∀ff:ℕ⟶X→∃k∈ℕL⁡f⁡k≤1→M⁡T⁡f⁡k≤k↔∀ff:ℕ⟶X→¬∀k∈ℕ¬L⁡f⁡k≤1→M⁡T⁡f⁡k≤k
26 alinexa ⊢∀ff:ℕ⟶X→¬∀k∈ℕ¬L⁡f⁡k≤1→M⁡T⁡f⁡k≤k↔¬∃ff:ℕ⟶X∧∀k∈ℕ¬L⁡f⁡k≤1→M⁡T⁡f⁡k≤k
27 25 26 bitri ⊢∀ff:ℕ⟶X→∃k∈ℕL⁡f⁡k≤1→M⁡T⁡f⁡k≤k↔¬∃ff:ℕ⟶X∧∀k∈ℕ¬L⁡f⁡k≤1→M⁡T⁡f⁡k≤k
28 dfral2 ⊢∀y∈XL⁡y≤1→M⁡T⁡y≤k↔¬∃y∈X¬L⁡y≤1→M⁡T⁡y≤k
29 28 rexbii ⊢∃k∈ℕ∀y∈XL⁡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∈XL⁡y≤1→M⁡T⁡y≤k↔¬∀k∈ℕ∃y∈X¬L⁡y≤1→M⁡T⁡y≤k
32 22 27 31 3imtr4i ⊢∀ff:ℕ⟶X→∃k∈ℕL⁡f⁡k≤1→M⁡T⁡f⁡k≤k→∃k∈ℕ∀y∈XL⁡y≤1→M⁡T⁡y≤k
33 nnre ⊢k∈ℕ→k∈ℝ
34 33 anim1i ⊢k∈ℕ∧∀y∈XL⁡y≤1→M⁡T⁡y≤k→k∈ℝ∧∀y∈XL⁡y≤1→M⁡T⁡y≤k
35 34 reximi2 ⊢∃k∈ℕ∀y∈XL⁡y≤1→M⁡T⁡y≤k→∃k∈ℝ∀y∈XL⁡y≤1→M⁡T⁡y≤k
36 32 35 syl ⊢∀ff:ℕ⟶X→∃k∈ℕL⁡f⁡k≤1→M⁡T⁡f⁡k≤k→∃k∈ℝ∀y∈XL⁡y≤1→M⁡T⁡y≤k
37 12 36 sylbi ⊢∀ff:ℕ⟶X∧∀k∈ℕL⁡f⁡k≤1→∃k∈ℕM⁡T⁡f⁡k≤k→∃k∈ℝ∀y∈XL⁡y≤1→M⁡T⁡y≤k
38 1 2 3 4 5 6 7 nmobndi ⊢T:X⟶Y→N⁡T∈ℝ↔∃k∈ℝ∀y∈XL⁡y≤1→M⁡T⁡y≤k
39 37 38 imbitrrid ⊢T:X⟶Y→∀ff:ℕ⟶X∧∀k∈ℕL⁡f⁡k≤1→∃k∈ℕM⁡T⁡f⁡k≤k→N⁡T∈ℝ
40 39 imp ⊢T:X⟶Y∧∀ff:ℕ⟶X∧∀k∈ℕL⁡f⁡k≤1→∃k∈ℕM⁡T⁡f⁡k≤k→N⁡T∈ℝ