Metamath Proof Explorer


Theorem nmounbseqiALT

Description: Alternate shorter proof of nmounbseqi based on Axioms ax-reg and ax-ac2 instead of ax-cc . (Contributed by NM, 11-Jan-2008) (New usage is discouraged.) (Proof modification 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 nmounbseqiALT 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 nnex V
14 fveq2 y = f k L y = L f k
15 14 breq1d y = f k L y 1 L f k 1
16 fveq2 y = f k T y = T f k
17 16 fveq2d 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 15 18 anbi12d y = f k L y 1 k < M T y L f k 1 k < M T f k
20 13 19 ac6s 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