Metamath Proof Explorer


Theorem nmounbi

Description: Two ways two express that an operator is unbounded. (Contributed by NM, 11-Jan-2008) (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 nmounbi T : X Y N T = +∞ r y X L y 1 r < M T y

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 nmobndi T : X Y N T r y X L y 1 M T y r
9 1 2 5 nmorepnf U NrmCVec W NrmCVec T : X Y N T N T +∞
10 6 7 9 mp3an12 T : X Y N T N T +∞
11 ffvelrn T : X Y y X T y Y
12 2 4 nvcl W NrmCVec T y Y M T y
13 7 11 12 sylancr T : X Y y X M T y
14 lenlt M T y r M T y r ¬ r < M T y
15 13 14 sylan T : X Y y X r M T y r ¬ r < M T y
16 15 an32s T : X Y r y X M T y r ¬ r < M T y
17 16 imbi2d T : X Y r y X L y 1 M T y r L y 1 ¬ r < M T y
18 imnan L y 1 ¬ r < M T y ¬ L y 1 r < M T y
19 17 18 bitrdi T : X Y r y X L y 1 M T y r ¬ L y 1 r < M T y
20 19 ralbidva T : X Y r y X L y 1 M T y r y X ¬ L y 1 r < M T y
21 ralnex y X ¬ L y 1 r < M T y ¬ y X L y 1 r < M T y
22 20 21 bitrdi T : X Y r y X L y 1 M T y r ¬ y X L y 1 r < M T y
23 22 rexbidva T : X Y r y X L y 1 M T y r r ¬ y X L y 1 r < M T y
24 rexnal r ¬ y X L y 1 r < M T y ¬ r y X L y 1 r < M T y
25 23 24 bitrdi T : X Y r y X L y 1 M T y r ¬ r y X L y 1 r < M T y
26 8 10 25 3bitr3d T : X Y N T +∞ ¬ r y X L y 1 r < M T y
27 26 necon4abid T : X Y N T = +∞ r y X L y 1 r < M T y