Metamath Proof Explorer

Theorem ubthlem3

Description: Lemma for ubth . Prove the reverse implication, using nmblolbi . (Contributed by Mario Carneiro, 11-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses ubth.1 
|- X = ( BaseSet ` U )
ubth.2 
|- N = ( normCV ` W )
ubthlem.3 
|- D = ( IndMet ` U )
ubthlem.4 
|- J = ( MetOpen ` D )
ubthlem.5 
|- U e. CBan
ubthlem.6 
|- W e. NrmCVec
ubthlem.7 
|- ( ph -> T C_ ( U BLnOp W ) )
Assertion ubthlem3 
|- ( ph -> ( A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c <-> E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d ) )

Proof

Step Hyp Ref Expression
1 ubth.1 
 |-  X = ( BaseSet ` U )
2 ubth.2 
 |-  N = ( normCV ` W )
3 ubthlem.3 
 |-  D = ( IndMet ` U )
4 ubthlem.4 
 |-  J = ( MetOpen ` D )
5 ubthlem.5 
 |-  U e. CBan
6 ubthlem.6 
 |-  W e. NrmCVec
7 ubthlem.7 
 |-  ( ph -> T C_ ( U BLnOp W ) )
8 fveq1 
 |-  ( u = t -> ( u ` z ) = ( t ` z ) )
9 8 fveq2d 
 |-  ( u = t -> ( N ` ( u ` z ) ) = ( N ` ( t ` z ) ) )
10 9 breq1d 
 |-  ( u = t -> ( ( N ` ( u ` z ) ) <_ d <-> ( N ` ( t ` z ) ) <_ d ) )
11 10 cbvralvw 
 |-  ( A. u e. T ( N ` ( u ` z ) ) <_ d <-> A. t e. T ( N ` ( t ` z ) ) <_ d )
12 breq2 
 |-  ( d = c -> ( ( N ` ( t ` z ) ) <_ d <-> ( N ` ( t ` z ) ) <_ c ) )
13 12 ralbidv 
 |-  ( d = c -> ( A. t e. T ( N ` ( t ` z ) ) <_ d <-> A. t e. T ( N ` ( t ` z ) ) <_ c ) )
14 11 13 bitrid 
 |-  ( d = c -> ( A. u e. T ( N ` ( u ` z ) ) <_ d <-> A. t e. T ( N ` ( t ` z ) ) <_ c ) )
15 14 cbvrexvw 
 |-  ( E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d <-> E. c e. RR A. t e. T ( N ` ( t ` z ) ) <_ c )
16 2fveq3 
 |-  ( z = x -> ( N ` ( t ` z ) ) = ( N ` ( t ` x ) ) )
17 16 breq1d 
 |-  ( z = x -> ( ( N ` ( t ` z ) ) <_ c <-> ( N ` ( t ` x ) ) <_ c ) )
18 17 rexralbidv 
 |-  ( z = x -> ( E. c e. RR A. t e. T ( N ` ( t ` z ) ) <_ c <-> E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c ) )
19 15 18 bitrid 
 |-  ( z = x -> ( E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d <-> E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c ) )
20 19 cbvralvw 
 |-  ( A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d <-> A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c )
21 7 adantr 
 |-  ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) -> T C_ ( U BLnOp W ) )
22 20 bilani 
 |-  ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) -> A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c )
23 fveq1 
 |-  ( u = t -> ( u ` d ) = ( t ` d ) )
24 23 fveq2d 
 |-  ( u = t -> ( N ` ( u ` d ) ) = ( N ` ( t ` d ) ) )
25 24 breq1d 
 |-  ( u = t -> ( ( N ` ( u ` d ) ) <_ m <-> ( N ` ( t ` d ) ) <_ m ) )
26 25 cbvralvw 
 |-  ( A. u e. T ( N ` ( u ` d ) ) <_ m <-> A. t e. T ( N ` ( t ` d ) ) <_ m )
27 2fveq3 
 |-  ( d = z -> ( N ` ( t ` d ) ) = ( N ` ( t ` z ) ) )
28 27 breq1d 
 |-  ( d = z -> ( ( N ` ( t ` d ) ) <_ m <-> ( N ` ( t ` z ) ) <_ m ) )
29 28 ralbidv 
 |-  ( d = z -> ( A. t e. T ( N ` ( t ` d ) ) <_ m <-> A. t e. T ( N ` ( t ` z ) ) <_ m ) )
30 26 29 bitrid 
 |-  ( d = z -> ( A. u e. T ( N ` ( u ` d ) ) <_ m <-> A. t e. T ( N ` ( t ` z ) ) <_ m ) )
31 30 cbvrabv 
 |-  { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } = { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ m }
32 breq2 
 |-  ( m = k -> ( ( N ` ( t ` z ) ) <_ m <-> ( N ` ( t ` z ) ) <_ k ) )
33 32 ralbidv 
 |-  ( m = k -> ( A. t e. T ( N ` ( t ` z ) ) <_ m <-> A. t e. T ( N ` ( t ` z ) ) <_ k ) )
34 33 rabbidv 
 |-  ( m = k -> { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ m } = { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } )
35 31 34 eqtrid 
 |-  ( m = k -> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } = { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } )
36 35 cbvmptv 
 |-  ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) = ( k e. NN |-> { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } )
37 1 2 3 4 5 6 21 22 36 ubthlem1 
 |-  ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) -> E. n e. NN E. y e. X E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) )
38 7 ad3antrrr 
 |-  ( ( ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) /\ ( n e. NN /\ y e. X ) ) /\ ( r e. RR+ /\ { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) ) ) -> T C_ ( U BLnOp W ) )
39 22 ad2antrr 
 |-  ( ( ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) /\ ( n e. NN /\ y e. X ) ) /\ ( r e. RR+ /\ { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) ) ) -> A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c )
40 simplrl 
 |-  ( ( ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) /\ ( n e. NN /\ y e. X ) ) /\ ( r e. RR+ /\ { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) ) ) -> n e. NN )
41 simplrr 
 |-  ( ( ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) /\ ( n e. NN /\ y e. X ) ) /\ ( r e. RR+ /\ { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) ) ) -> y e. X )
42 simprl 
 |-  ( ( ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) /\ ( n e. NN /\ y e. X ) ) /\ ( r e. RR+ /\ { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) ) ) -> r e. RR+ )
43 simprr 
 |-  ( ( ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) /\ ( n e. NN /\ y e. X ) ) /\ ( r e. RR+ /\ { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) ) ) -> { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) )
44 1 2 3 4 5 6 38 39 36 40 41 42 43 ubthlem2 
 |-  ( ( ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) /\ ( n e. NN /\ y e. X ) ) /\ ( r e. RR+ /\ { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) ) ) -> E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d )
45 44 expr 
 |-  ( ( ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) /\ ( n e. NN /\ y e. X ) ) /\ r e. RR+ ) -> ( { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) -> E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d ) )
46 45 rexlimdva 
 |-  ( ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) /\ ( n e. NN /\ y e. X ) ) -> ( E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) -> E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d ) )
47 46 rexlimdvva 
 |-  ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) -> ( E. n e. NN E. y e. X E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) -> E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d ) )
48 37 47 mpd 
 |-  ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) -> E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d )
49 48 ex 
 |-  ( ph -> ( A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d -> E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d ) )
50 20 49 biimtrrid 
 |-  ( ph -> ( A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c -> E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d ) )
51 simpr 
 |-  ( ( ph /\ d e. RR ) -> d e. RR )
52 bnnv 
 |-  ( U e. CBan -> U e. NrmCVec )
53 5 52 ax-mp 
 |-  U e. NrmCVec
54 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
55 1 54 nvcl 
 |-  ( ( U e. NrmCVec /\ x e. X ) -> ( ( normCV ` U ) ` x ) e. RR )
56 53 55 mpan 
 |-  ( x e. X -> ( ( normCV ` U ) ` x ) e. RR )
57 remulcl 
 |-  ( ( d e. RR /\ ( ( normCV ` U ) ` x ) e. RR ) -> ( d x. ( ( normCV ` U ) ` x ) ) e. RR )
58 51 56 57 syl2an 
 |-  ( ( ( ph /\ d e. RR ) /\ x e. X ) -> ( d x. ( ( normCV ` U ) ` x ) ) e. RR )
59 7 sselda 
 |-  ( ( ph /\ t e. T ) -> t e. ( U BLnOp W ) )
60 59 adantlr 
 |-  ( ( ( ph /\ d e. RR ) /\ t e. T ) -> t e. ( U BLnOp W ) )
61 60 ad2ant2r 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> t e. ( U BLnOp W ) )
62 eqid 
 |-  ( BaseSet ` W ) = ( BaseSet ` W )
63 eqid 
 |-  ( U BLnOp W ) = ( U BLnOp W )
64 1 62 63 blof 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ t e. ( U BLnOp W ) ) -> t : X --> ( BaseSet ` W ) )
65 53 6 64 mp3an12 
 |-  ( t e. ( U BLnOp W ) -> t : X --> ( BaseSet ` W ) )
66 61 65 syl 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> t : X --> ( BaseSet ` W ) )
67 simplr 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> x e. X )
68 66 67 ffvelcdmd 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( t ` x ) e. ( BaseSet ` W ) )
69 62 2 nvcl 
 |-  ( ( W e. NrmCVec /\ ( t ` x ) e. ( BaseSet ` W ) ) -> ( N ` ( t ` x ) ) e. RR )
70 6 69 mpan 
 |-  ( ( t ` x ) e. ( BaseSet ` W ) -> ( N ` ( t ` x ) ) e. RR )
71 68 70 syl 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( N ` ( t ` x ) ) e. RR )
72 eqid 
 |-  ( U normOpOLD W ) = ( U normOpOLD W )
73 1 62 72 nmoxr 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ t : X --> ( BaseSet ` W ) ) -> ( ( U normOpOLD W ) ` t ) e. RR* )
74 53 6 73 mp3an12 
 |-  ( t : X --> ( BaseSet ` W ) -> ( ( U normOpOLD W ) ` t ) e. RR* )
75 66 74 syl 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( ( U normOpOLD W ) ` t ) e. RR* )
76 simpllr 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> d e. RR )
77 1 62 72 nmogtmnf 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ t : X --> ( BaseSet ` W ) ) -> -oo < ( ( U normOpOLD W ) ` t ) )
78 53 6 77 mp3an12 
 |-  ( t : X --> ( BaseSet ` W ) -> -oo < ( ( U normOpOLD W ) ` t ) )
79 66 78 syl 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> -oo < ( ( U normOpOLD W ) ` t ) )
80 simprr 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( ( U normOpOLD W ) ` t ) <_ d )
81 xrre 
 |-  ( ( ( ( ( U normOpOLD W ) ` t ) e. RR* /\ d e. RR ) /\ ( -oo < ( ( U normOpOLD W ) ` t ) /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( ( U normOpOLD W ) ` t ) e. RR )
82 75 76 79 80 81 syl22anc 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( ( U normOpOLD W ) ` t ) e. RR )
83 56 ad2antlr 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( ( normCV ` U ) ` x ) e. RR )
84 remulcl 
 |-  ( ( ( ( U normOpOLD W ) ` t ) e. RR /\ ( ( normCV ` U ) ` x ) e. RR ) -> ( ( ( U normOpOLD W ) ` t ) x. ( ( normCV ` U ) ` x ) ) e. RR )
85 82 83 84 syl2anc 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( ( ( U normOpOLD W ) ` t ) x. ( ( normCV ` U ) ` x ) ) e. RR )
86 58 adantr 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( d x. ( ( normCV ` U ) ` x ) ) e. RR )
87 1 54 2 72 63 53 6 nmblolbi 
 |-  ( ( t e. ( U BLnOp W ) /\ x e. X ) -> ( N ` ( t ` x ) ) <_ ( ( ( U normOpOLD W ) ` t ) x. ( ( normCV ` U ) ` x ) ) )
88 61 67 87 syl2anc 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( N ` ( t ` x ) ) <_ ( ( ( U normOpOLD W ) ` t ) x. ( ( normCV ` U ) ` x ) ) )
89 1 54 nvge0 
 |-  ( ( U e. NrmCVec /\ x e. X ) -> 0 <_ ( ( normCV ` U ) ` x ) )
90 53 89 mpan 
 |-  ( x e. X -> 0 <_ ( ( normCV ` U ) ` x ) )
91 56 90 jca 
 |-  ( x e. X -> ( ( ( normCV ` U ) ` x ) e. RR /\ 0 <_ ( ( normCV ` U ) ` x ) ) )
92 91 ad2antlr 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( ( ( normCV ` U ) ` x ) e. RR /\ 0 <_ ( ( normCV ` U ) ` x ) ) )
93 lemul1a 
 |-  ( ( ( ( ( U normOpOLD W ) ` t ) e. RR /\ d e. RR /\ ( ( ( normCV ` U ) ` x ) e. RR /\ 0 <_ ( ( normCV ` U ) ` x ) ) ) /\ ( ( U normOpOLD W ) ` t ) <_ d ) -> ( ( ( U normOpOLD W ) ` t ) x. ( ( normCV ` U ) ` x ) ) <_ ( d x. ( ( normCV ` U ) ` x ) ) )
94 82 76 92 80 93 syl31anc 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( ( ( U normOpOLD W ) ` t ) x. ( ( normCV ` U ) ` x ) ) <_ ( d x. ( ( normCV ` U ) ` x ) ) )
95 71 85 86 88 94 letrd 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( N ` ( t ` x ) ) <_ ( d x. ( ( normCV ` U ) ` x ) ) )
96 95 expr 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ t e. T ) -> ( ( ( U normOpOLD W ) ` t ) <_ d -> ( N ` ( t ` x ) ) <_ ( d x. ( ( normCV ` U ) ` x ) ) ) )
97 96 ralimdva 
 |-  ( ( ( ph /\ d e. RR ) /\ x e. X ) -> ( A. t e. T ( ( U normOpOLD W ) ` t ) <_ d -> A. t e. T ( N ` ( t ` x ) ) <_ ( d x. ( ( normCV ` U ) ` x ) ) ) )
98 brralrspcev 
 |-  ( ( ( d x. ( ( normCV ` U ) ` x ) ) e. RR /\ A. t e. T ( N ` ( t ` x ) ) <_ ( d x. ( ( normCV ` U ) ` x ) ) ) -> E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c )
99 58 97 98 syl6an 
 |-  ( ( ( ph /\ d e. RR ) /\ x e. X ) -> ( A. t e. T ( ( U normOpOLD W ) ` t ) <_ d -> E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c ) )
100 99 ralrimdva 
 |-  ( ( ph /\ d e. RR ) -> ( A. t e. T ( ( U normOpOLD W ) ` t ) <_ d -> A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c ) )
101 100 rexlimdva 
 |-  ( ph -> ( E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d -> A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c ) )
102 50 101 impbid 
 |-  ( ph -> ( A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c <-> E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d ) )