Metamath Proof Explorer

Theorem ubthlem2

Description: Lemma for ubth . Given that there is a closed ball B ( P , R ) in AK , for any x e. B ( 0 , 1 ) , we have P + R x. x e. B ( P , R ) and P e. B ( P , R ) , so both of these have norm ( t ( z ) ) <_ K and so norm ( t ( x ) ) <_ ( norm ( t ( P ) ) + norm ( t ( P + R x. x ) ) ) / R <_ ( K + K ) / R , which is our desired uniform bound. (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 ) )
ubthlem.8 
|- ( ph -> A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c )
ubthlem.9 
|- A = ( k e. NN |-> { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } )
ubthlem.10 
|- ( ph -> K e. NN )
ubthlem.11 
|- ( ph -> P e. X )
ubthlem.12 
|- ( ph -> R e. RR+ )
ubthlem.13 
|- ( ph -> { z e. X | ( P D z ) <_ R } C_ ( A ` K ) )
Assertion ubthlem2 
|- ( ph -> 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 ubthlem.8 
 |-  ( ph -> A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c )
9 ubthlem.9 
 |-  A = ( k e. NN |-> { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } )
10 ubthlem.10 
 |-  ( ph -> K e. NN )
11 ubthlem.11 
 |-  ( ph -> P e. X )
12 ubthlem.12 
 |-  ( ph -> R e. RR+ )
13 ubthlem.13 
 |-  ( ph -> { z e. X | ( P D z ) <_ R } C_ ( A ` K ) )
14 10 nnrpd 
 |-  ( ph -> K e. RR+ )
15 14 14 rpaddcld 
 |-  ( ph -> ( K + K ) e. RR+ )
16 15 12 rpdivcld 
 |-  ( ph -> ( ( K + K ) / R ) e. RR+ )
17 16 rpred 
 |-  ( ph -> ( ( K + K ) / R ) e. RR )
18 oveq2 
 |-  ( z = ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) -> ( P D z ) = ( P D ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) )
19 18 breq1d 
 |-  ( z = ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) -> ( ( P D z ) <_ R <-> ( P D ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) <_ R ) )
20 eleq1 
 |-  ( z = ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) -> ( z e. ( A ` K ) <-> ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) e. ( A ` K ) ) )
21 19 20 imbi12d 
 |-  ( z = ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) -> ( ( ( P D z ) <_ R -> z e. ( A ` K ) ) <-> ( ( P D ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) <_ R -> ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) e. ( A ` K ) ) ) )
22 rabss 
 |-  ( { z e. X | ( P D z ) <_ R } C_ ( A ` K ) <-> A. z e. X ( ( P D z ) <_ R -> z e. ( A ` K ) ) )
23 13 22 sylib 
 |-  ( ph -> A. z e. X ( ( P D z ) <_ R -> z e. ( A ` K ) ) )
24 23 ad2antrr 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> A. z e. X ( ( P D z ) <_ R -> z e. ( A ` K ) ) )
25 bnnv 
 |-  ( U e. CBan -> U e. NrmCVec )
26 5 25 ax-mp 
 |-  U e. NrmCVec
27 26 a1i 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> U e. NrmCVec )
28 11 ad2antrr 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> P e. X )
29 12 ad2antrr 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> R e. RR+ )
30 29 rpcnd 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> R e. CC )
31 simpr 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> x e. X )
32 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
33 1 32 nvscl 
 |-  ( ( U e. NrmCVec /\ R e. CC /\ x e. X ) -> ( R ( .sOLD ` U ) x ) e. X )
34 27 30 31 33 syl3anc 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( R ( .sOLD ` U ) x ) e. X )
35 eqid 
 |-  ( +v ` U ) = ( +v ` U )
36 1 35 nvgcl 
 |-  ( ( U e. NrmCVec /\ P e. X /\ ( R ( .sOLD ` U ) x ) e. X ) -> ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) e. X )
37 27 28 34 36 syl3anc 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) e. X )
38 21 24 37 rspcdva 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( P D ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) <_ R -> ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) e. ( A ` K ) ) )
39 1 3 cbncms 
 |-  ( U e. CBan -> D e. ( CMet ` X ) )
40 5 39 ax-mp 
 |-  D e. ( CMet ` X )
41 cmetmet 
 |-  ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
42 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
43 40 41 42 mp2b 
 |-  D e. ( *Met ` X )
44 43 a1i 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> D e. ( *Met ` X ) )
45 xmetsym 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) e. X ) -> ( P D ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) = ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) D P ) )
46 44 28 37 45 syl3anc 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( P D ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) = ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) D P ) )
47 eqid 
 |-  ( -v ` U ) = ( -v ` U )
48 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
49 1 47 48 3 imsdval 
 |-  ( ( U e. NrmCVec /\ ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) e. X /\ P e. X ) -> ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) D P ) = ( ( normCV ` U ) ` ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ( -v ` U ) P ) ) )
50 27 37 28 49 syl3anc 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) D P ) = ( ( normCV ` U ) ` ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ( -v ` U ) P ) ) )
51 1 35 47 nvpncan2 
 |-  ( ( U e. NrmCVec /\ P e. X /\ ( R ( .sOLD ` U ) x ) e. X ) -> ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ( -v ` U ) P ) = ( R ( .sOLD ` U ) x ) )
52 27 28 34 51 syl3anc 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ( -v ` U ) P ) = ( R ( .sOLD ` U ) x ) )
53 52 fveq2d 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( normCV ` U ) ` ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ( -v ` U ) P ) ) = ( ( normCV ` U ) ` ( R ( .sOLD ` U ) x ) ) )
54 46 50 53 3eqtrd 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( P D ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) = ( ( normCV ` U ) ` ( R ( .sOLD ` U ) x ) ) )
55 29 rprege0d 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( R e. RR /\ 0 <_ R ) )
56 1 32 48 nvsge0 
 |-  ( ( U e. NrmCVec /\ ( R e. RR /\ 0 <_ R ) /\ x e. X ) -> ( ( normCV ` U ) ` ( R ( .sOLD ` U ) x ) ) = ( R x. ( ( normCV ` U ) ` x ) ) )
57 27 55 31 56 syl3anc 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( normCV ` U ) ` ( R ( .sOLD ` U ) x ) ) = ( R x. ( ( normCV ` U ) ` x ) ) )
58 54 57 eqtrd 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( P D ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) = ( R x. ( ( normCV ` U ) ` x ) ) )
59 30 mulid1d 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( R x. 1 ) = R )
60 59 eqcomd 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> R = ( R x. 1 ) )
61 58 60 breq12d 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( P D ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) <_ R <-> ( R x. ( ( normCV ` U ) ` x ) ) <_ ( R x. 1 ) ) )
62 1 48 nvcl 
 |-  ( ( U e. NrmCVec /\ x e. X ) -> ( ( normCV ` U ) ` x ) e. RR )
63 26 62 mpan 
 |-  ( x e. X -> ( ( normCV ` U ) ` x ) e. RR )
64 63 adantl 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( normCV ` U ) ` x ) e. RR )
65 1red 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> 1 e. RR )
66 64 65 29 lemul2d 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( ( normCV ` U ) ` x ) <_ 1 <-> ( R x. ( ( normCV ` U ) ` x ) ) <_ ( R x. 1 ) ) )
67 61 66 bitr4d 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( P D ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) <_ R <-> ( ( normCV ` U ) ` x ) <_ 1 ) )
68 breq2 
 |-  ( k = K -> ( ( N ` ( t ` z ) ) <_ k <-> ( N ` ( t ` z ) ) <_ K ) )
69 68 ralbidv 
 |-  ( k = K -> ( A. t e. T ( N ` ( t ` z ) ) <_ k <-> A. t e. T ( N ` ( t ` z ) ) <_ K ) )
70 69 rabbidv 
 |-  ( k = K -> { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } = { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ K } )
71 1 fvexi 
 |-  X e. _V
72 71 rabex 
 |-  { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ K } e. _V
73 70 9 72 fvmpt 
 |-  ( K e. NN -> ( A ` K ) = { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ K } )
74 10 73 syl 
 |-  ( ph -> ( A ` K ) = { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ K } )
75 74 eleq2d 
 |-  ( ph -> ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) e. ( A ` K ) <-> ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) e. { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ K } ) )
76 2fveq3 
 |-  ( z = ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) -> ( N ` ( t ` z ) ) = ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) )
77 76 breq1d 
 |-  ( z = ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) -> ( ( N ` ( t ` z ) ) <_ K <-> ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) <_ K ) )
78 77 ralbidv 
 |-  ( z = ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) -> ( A. t e. T ( N ` ( t ` z ) ) <_ K <-> A. t e. T ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) <_ K ) )
79 78 elrab 
 |-  ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) e. { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ K } <-> ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) e. X /\ A. t e. T ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) <_ K ) )
80 75 79 bitrdi 
 |-  ( ph -> ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) e. ( A ` K ) <-> ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) e. X /\ A. t e. T ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) <_ K ) ) )
81 80 ad2antrr 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) e. ( A ` K ) <-> ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) e. X /\ A. t e. T ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) <_ K ) ) )
82 38 67 81 3imtr3d 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( ( normCV ` U ) ` x ) <_ 1 -> ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) e. X /\ A. t e. T ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) <_ K ) ) )
83 rsp 
 |-  ( A. t e. T ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) <_ K -> ( t e. T -> ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) <_ K ) )
84 83 com12 
 |-  ( t e. T -> ( A. t e. T ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) <_ K -> ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) <_ K ) )
85 84 ad2antlr 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( A. t e. T ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) <_ K -> ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) <_ K ) )
86 xmet0 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( P D P ) = 0 )
87 43 11 86 sylancr 
 |-  ( ph -> ( P D P ) = 0 )
88 12 rpge0d 
 |-  ( ph -> 0 <_ R )
89 87 88 eqbrtrd 
 |-  ( ph -> ( P D P ) <_ R )
90 oveq2 
 |-  ( z = P -> ( P D z ) = ( P D P ) )
91 90 breq1d 
 |-  ( z = P -> ( ( P D z ) <_ R <-> ( P D P ) <_ R ) )
92 91 elrab 
 |-  ( P e. { z e. X | ( P D z ) <_ R } <-> ( P e. X /\ ( P D P ) <_ R ) )
93 11 89 92 sylanbrc 
 |-  ( ph -> P e. { z e. X | ( P D z ) <_ R } )
94 13 93 sseldd 
 |-  ( ph -> P e. ( A ` K ) )
95 94 74 eleqtrd 
 |-  ( ph -> P e. { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ K } )
96 2fveq3 
 |-  ( z = P -> ( N ` ( t ` z ) ) = ( N ` ( t ` P ) ) )
97 96 breq1d 
 |-  ( z = P -> ( ( N ` ( t ` z ) ) <_ K <-> ( N ` ( t ` P ) ) <_ K ) )
98 97 ralbidv 
 |-  ( z = P -> ( A. t e. T ( N ` ( t ` z ) ) <_ K <-> A. t e. T ( N ` ( t ` P ) ) <_ K ) )
99 98 elrab 
 |-  ( P e. { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ K } <-> ( P e. X /\ A. t e. T ( N ` ( t ` P ) ) <_ K ) )
100 95 99 sylib 
 |-  ( ph -> ( P e. X /\ A. t e. T ( N ` ( t ` P ) ) <_ K ) )
101 100 simprd 
 |-  ( ph -> A. t e. T ( N ` ( t ` P ) ) <_ K )
102 101 r19.21bi 
 |-  ( ( ph /\ t e. T ) -> ( N ` ( t ` P ) ) <_ K )
103 102 adantr 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( N ` ( t ` P ) ) <_ K )
104 7 sselda 
 |-  ( ( ph /\ t e. T ) -> t e. ( U BLnOp W ) )
105 eqid 
 |-  ( IndMet ` W ) = ( IndMet ` W )
106 eqid 
 |-  ( MetOpen ` ( IndMet ` W ) ) = ( MetOpen ` ( IndMet ` W ) )
107 eqid 
 |-  ( U BLnOp W ) = ( U BLnOp W )
108 3 105 4 106 107 26 6 blocn2 
 |-  ( t e. ( U BLnOp W ) -> t e. ( J Cn ( MetOpen ` ( IndMet ` W ) ) ) )
109 4 mopntopon 
 |-  ( D e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
110 43 109 ax-mp 
 |-  J e. ( TopOn ` X )
111 eqid 
 |-  ( BaseSet ` W ) = ( BaseSet ` W )
112 111 105 imsxmet 
 |-  ( W e. NrmCVec -> ( IndMet ` W ) e. ( *Met ` ( BaseSet ` W ) ) )
113 106 mopntopon 
 |-  ( ( IndMet ` W ) e. ( *Met ` ( BaseSet ` W ) ) -> ( MetOpen ` ( IndMet ` W ) ) e. ( TopOn ` ( BaseSet ` W ) ) )
114 6 112 113 mp2b 
 |-  ( MetOpen ` ( IndMet ` W ) ) e. ( TopOn ` ( BaseSet ` W ) )
115 iscncl 
 |-  ( ( J e. ( TopOn ` X ) /\ ( MetOpen ` ( IndMet ` W ) ) e. ( TopOn ` ( BaseSet ` W ) ) ) -> ( t e. ( J Cn ( MetOpen ` ( IndMet ` W ) ) ) <-> ( t : X --> ( BaseSet ` W ) /\ A. x e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) ( `' t " x ) e. ( Clsd ` J ) ) ) )
116 110 114 115 mp2an 
 |-  ( t e. ( J Cn ( MetOpen ` ( IndMet ` W ) ) ) <-> ( t : X --> ( BaseSet ` W ) /\ A. x e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) ( `' t " x ) e. ( Clsd ` J ) ) )
117 108 116 sylib 
 |-  ( t e. ( U BLnOp W ) -> ( t : X --> ( BaseSet ` W ) /\ A. x e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) ( `' t " x ) e. ( Clsd ` J ) ) )
118 104 117 syl 
 |-  ( ( ph /\ t e. T ) -> ( t : X --> ( BaseSet ` W ) /\ A. x e. ( Clsd ` ( MetOpen ` ( IndMet ` W ) ) ) ( `' t " x ) e. ( Clsd ` J ) ) )
119 118 simpld 
 |-  ( ( ph /\ t e. T ) -> t : X --> ( BaseSet ` W ) )
120 119 adantr 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> t : X --> ( BaseSet ` W ) )
121 120 37 ffvelrnd 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) e. ( BaseSet ` W ) )
122 111 2 nvcl 
 |-  ( ( W e. NrmCVec /\ ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) e. ( BaseSet ` W ) ) -> ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) e. RR )
123 6 121 122 sylancr 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) e. RR )
124 120 28 ffvelrnd 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( t ` P ) e. ( BaseSet ` W ) )
125 111 2 nvcl 
 |-  ( ( W e. NrmCVec /\ ( t ` P ) e. ( BaseSet ` W ) ) -> ( N ` ( t ` P ) ) e. RR )
126 6 124 125 sylancr 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( N ` ( t ` P ) ) e. RR )
127 10 nnred 
 |-  ( ph -> K e. RR )
128 127 ad2antrr 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> K e. RR )
129 le2add 
 |-  ( ( ( ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) e. RR /\ ( N ` ( t ` P ) ) e. RR ) /\ ( K e. RR /\ K e. RR ) ) -> ( ( ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) <_ K /\ ( N ` ( t ` P ) ) <_ K ) -> ( ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) + ( N ` ( t ` P ) ) ) <_ ( K + K ) ) )
130 123 126 128 128 129 syl22anc 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) <_ K /\ ( N ` ( t ` P ) ) <_ K ) -> ( ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) + ( N ` ( t ` P ) ) ) <_ ( K + K ) ) )
131 103 130 mpan2d 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) <_ K -> ( ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) + ( N ` ( t ` P ) ) ) <_ ( K + K ) ) )
132 52 fveq2d 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( t ` ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ( -v ` U ) P ) ) = ( t ` ( R ( .sOLD ` U ) x ) ) )
133 6 a1i 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> W e. NrmCVec )
134 eqid 
 |-  ( U LnOp W ) = ( U LnOp W )
135 134 107 bloln 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ t e. ( U BLnOp W ) ) -> t e. ( U LnOp W ) )
136 26 6 135 mp3an12 
 |-  ( t e. ( U BLnOp W ) -> t e. ( U LnOp W ) )
137 104 136 syl 
 |-  ( ( ph /\ t e. T ) -> t e. ( U LnOp W ) )
138 137 adantr 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> t e. ( U LnOp W ) )
139 eqid 
 |-  ( -v ` W ) = ( -v ` W )
140 1 47 139 134 lnosub 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ t e. ( U LnOp W ) ) /\ ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) e. X /\ P e. X ) ) -> ( t ` ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ( -v ` U ) P ) ) = ( ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ( -v ` W ) ( t ` P ) ) )
141 27 133 138 37 28 140 syl32anc 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( t ` ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ( -v ` U ) P ) ) = ( ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ( -v ` W ) ( t ` P ) ) )
142 eqid 
 |-  ( .sOLD ` W ) = ( .sOLD ` W )
143 1 32 142 134 lnomul 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ t e. ( U LnOp W ) ) /\ ( R e. CC /\ x e. X ) ) -> ( t ` ( R ( .sOLD ` U ) x ) ) = ( R ( .sOLD ` W ) ( t ` x ) ) )
144 27 133 138 30 31 143 syl32anc 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( t ` ( R ( .sOLD ` U ) x ) ) = ( R ( .sOLD ` W ) ( t ` x ) ) )
145 132 141 144 3eqtr3d 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ( -v ` W ) ( t ` P ) ) = ( R ( .sOLD ` W ) ( t ` x ) ) )
146 145 fveq2d 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( N ` ( ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ( -v ` W ) ( t ` P ) ) ) = ( N ` ( R ( .sOLD ` W ) ( t ` x ) ) ) )
147 119 ffvelrnda 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( t ` x ) e. ( BaseSet ` W ) )
148 111 142 2 nvsge0 
 |-  ( ( W e. NrmCVec /\ ( R e. RR /\ 0 <_ R ) /\ ( t ` x ) e. ( BaseSet ` W ) ) -> ( N ` ( R ( .sOLD ` W ) ( t ` x ) ) ) = ( R x. ( N ` ( t ` x ) ) ) )
149 133 55 147 148 syl3anc 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( N ` ( R ( .sOLD ` W ) ( t ` x ) ) ) = ( R x. ( N ` ( t ` x ) ) ) )
150 146 149 eqtrd 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( N ` ( ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ( -v ` W ) ( t ` P ) ) ) = ( R x. ( N ` ( t ` x ) ) ) )
151 111 139 2 nvmtri 
 |-  ( ( W e. NrmCVec /\ ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) e. ( BaseSet ` W ) /\ ( t ` P ) e. ( BaseSet ` W ) ) -> ( N ` ( ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ( -v ` W ) ( t ` P ) ) ) <_ ( ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) + ( N ` ( t ` P ) ) ) )
152 133 121 124 151 syl3anc 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( N ` ( ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ( -v ` W ) ( t ` P ) ) ) <_ ( ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) + ( N ` ( t ` P ) ) ) )
153 150 152 eqbrtrrd 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( R x. ( N ` ( t ` x ) ) ) <_ ( ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) + ( N ` ( t ` P ) ) ) )
154 29 rpred 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> R e. RR )
155 111 2 nvcl 
 |-  ( ( W e. NrmCVec /\ ( t ` x ) e. ( BaseSet ` W ) ) -> ( N ` ( t ` x ) ) e. RR )
156 6 147 155 sylancr 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( N ` ( t ` x ) ) e. RR )
157 154 156 remulcld 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( R x. ( N ` ( t ` x ) ) ) e. RR )
158 123 126 readdcld 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) + ( N ` ( t ` P ) ) ) e. RR )
159 15 rpred 
 |-  ( ph -> ( K + K ) e. RR )
160 159 ad2antrr 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( K + K ) e. RR )
161 letr 
 |-  ( ( ( R x. ( N ` ( t ` x ) ) ) e. RR /\ ( ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) + ( N ` ( t ` P ) ) ) e. RR /\ ( K + K ) e. RR ) -> ( ( ( R x. ( N ` ( t ` x ) ) ) <_ ( ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) + ( N ` ( t ` P ) ) ) /\ ( ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) + ( N ` ( t ` P ) ) ) <_ ( K + K ) ) -> ( R x. ( N ` ( t ` x ) ) ) <_ ( K + K ) ) )
162 157 158 160 161 syl3anc 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( ( R x. ( N ` ( t ` x ) ) ) <_ ( ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) + ( N ` ( t ` P ) ) ) /\ ( ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) + ( N ` ( t ` P ) ) ) <_ ( K + K ) ) -> ( R x. ( N ` ( t ` x ) ) ) <_ ( K + K ) ) )
163 153 162 mpand 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) + ( N ` ( t ` P ) ) ) <_ ( K + K ) -> ( R x. ( N ` ( t ` x ) ) ) <_ ( K + K ) ) )
164 131 163 syld 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) <_ K -> ( R x. ( N ` ( t ` x ) ) ) <_ ( K + K ) ) )
165 156 160 29 lemuldiv2d 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( R x. ( N ` ( t ` x ) ) ) <_ ( K + K ) <-> ( N ` ( t ` x ) ) <_ ( ( K + K ) / R ) ) )
166 164 165 sylibd 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) <_ K -> ( N ` ( t ` x ) ) <_ ( ( K + K ) / R ) ) )
167 85 166 syld 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( A. t e. T ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) <_ K -> ( N ` ( t ` x ) ) <_ ( ( K + K ) / R ) ) )
168 167 adantld 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) e. X /\ A. t e. T ( N ` ( t ` ( P ( +v ` U ) ( R ( .sOLD ` U ) x ) ) ) ) <_ K ) -> ( N ` ( t ` x ) ) <_ ( ( K + K ) / R ) ) )
169 82 168 syld 
 |-  ( ( ( ph /\ t e. T ) /\ x e. X ) -> ( ( ( normCV ` U ) ` x ) <_ 1 -> ( N ` ( t ` x ) ) <_ ( ( K + K ) / R ) ) )
170 169 ralrimiva 
 |-  ( ( ph /\ t e. T ) -> A. x e. X ( ( ( normCV ` U ) ` x ) <_ 1 -> ( N ` ( t ` x ) ) <_ ( ( K + K ) / R ) ) )
171 16 rpxrd 
 |-  ( ph -> ( ( K + K ) / R ) e. RR* )
172 171 adantr 
 |-  ( ( ph /\ t e. T ) -> ( ( K + K ) / R ) e. RR* )
173 eqid 
 |-  ( U normOpOLD W ) = ( U normOpOLD W )
174 1 111 48 2 173 26 6 nmoubi 
 |-  ( ( t : X --> ( BaseSet ` W ) /\ ( ( K + K ) / R ) e. RR* ) -> ( ( ( U normOpOLD W ) ` t ) <_ ( ( K + K ) / R ) <-> A. x e. X ( ( ( normCV ` U ) ` x ) <_ 1 -> ( N ` ( t ` x ) ) <_ ( ( K + K ) / R ) ) ) )
175 119 172 174 syl2anc 
 |-  ( ( ph /\ t e. T ) -> ( ( ( U normOpOLD W ) ` t ) <_ ( ( K + K ) / R ) <-> A. x e. X ( ( ( normCV ` U ) ` x ) <_ 1 -> ( N ` ( t ` x ) ) <_ ( ( K + K ) / R ) ) ) )
176 170 175 mpbird 
 |-  ( ( ph /\ t e. T ) -> ( ( U normOpOLD W ) ` t ) <_ ( ( K + K ) / R ) )
177 176 ralrimiva 
 |-  ( ph -> A. t e. T ( ( U normOpOLD W ) ` t ) <_ ( ( K + K ) / R ) )
178 brralrspcev 
 |-  ( ( ( ( K + K ) / R ) e. RR /\ A. t e. T ( ( U normOpOLD W ) ` t ) <_ ( ( K + K ) / R ) ) -> E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d )
179 17 177 178 syl2anc 
 |-  ( ph -> E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d )