MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  htthlem Unicode version

Theorem htthlem 22381
Description: Lemma for htth 22382. The collection  K, which consists of functions  F ( z ) ( w )  =  <. w  |  T
( z ) >.  =  <. T ( w )  |  z >. for each  z in the unit ball, is a collection of bounded linear functions by ipblnfi 22318, so by the Uniform Boundedness theorem ubth 22336, there is a uniform bound  y on  ||  F ( x )  || for all  x in the unit ball. Then  |  T (
x )  |  ^
2  =  <. T ( x )  |  T
( x ) >.  =  F ( x ) (  T ( x ) )  <_  y  |  T ( x )  |, so  |  T ( x )  |  <_  y and 
T is bounded. (Contributed by NM, 11-Jan-2008.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
htth.1  |-  X  =  ( BaseSet `  U )
htth.2  |-  P  =  ( .i OLD `  U
)
htth.3  |-  L  =  ( U  LnOp  U
)
htth.4  |-  B  =  ( U  BLnOp  U )
htthlem.5  |-  N  =  ( normCV `  U )
htthlem.6  |-  U  e. 
CHil OLD
htthlem.7  |-  W  = 
<. <.  +  ,  x.  >. ,  abs >.
htthlem.8  |-  ( ph  ->  T  e.  L )
htthlem.9  |-  ( ph  ->  A. x  e.  X  A. y  e.  X  ( x P ( T `  y ) )  =  ( ( T `  x ) P y ) )
htthlem.10  |-  F  =  ( z  e.  X  |->  ( w  e.  X  |->  ( w P ( T `  z ) ) ) )
htthlem.11  |-  K  =  ( F " {
z  e.  X  | 
( N `  z
)  <_  1 }
)
Assertion
Ref Expression
htthlem  |-  ( ph  ->  T  e.  B )
Distinct variable groups:    y, w, F    x, w, z, K, y    w, N, x, y, z    w, P, z    w, W, x, y, z    ph, w, x, y, z    w, T, x, y, z    w, U, x, y, z    w, X, x, y, z
Allowed substitution hints:    B( x, y, z, w)    P( x, y)    F( x, z)    L( x, y, z, w)

Proof of Theorem htthlem
StepHypRef Expression
1 htthlem.8 . 2  |-  ( ph  ->  T  e.  L )
2 htthlem.6 . . . . . . . . . 10  |-  U  e. 
CHil OLD
32hlnvi 22355 . . . . . . . . 9  |-  U  e.  NrmCVec
4 htth.1 . . . . . . . . . . . . 13  |-  X  =  ( BaseSet `  U )
5 htth.3 . . . . . . . . . . . . 13  |-  L  =  ( U  LnOp  U
)
64, 4, 5lnof 22217 . . . . . . . . . . . 12  |-  ( ( U  e.  NrmCVec  /\  U  e.  NrmCVec  /\  T  e.  L )  ->  T : X --> X )
73, 3, 6mp3an12 1269 . . . . . . . . . . 11  |-  ( T  e.  L  ->  T : X --> X )
81, 7syl 16 . . . . . . . . . 10  |-  ( ph  ->  T : X --> X )
98ffvelrnda 5837 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  X )  ->  ( T `  x )  e.  X )
10 htthlem.5 . . . . . . . . . 10  |-  N  =  ( normCV `  U )
114, 10nvcl 22109 . . . . . . . . 9  |-  ( ( U  e.  NrmCVec  /\  ( T `  x )  e.  X )  ->  ( N `  ( T `  x ) )  e.  RR )
123, 9, 11sylancr 645 . . . . . . . 8  |-  ( (
ph  /\  x  e.  X )  ->  ( N `  ( T `  x ) )  e.  RR )
138ffvelrnda 5837 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  z  e.  X )  ->  ( T `  z )  e.  X )
14 htth.2 . . . . . . . . . . . . . . . . 17  |-  P  =  ( .i OLD `  U
)
15 hlph 22352 . . . . . . . . . . . . . . . . . 18  |-  ( U  e.  CHil OLD  ->  U  e.  CPreHil
OLD )
162, 15ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  U  e.  CPreHil
OLD
17 htthlem.7 . . . . . . . . . . . . . . . . 17  |-  W  = 
<. <.  +  ,  x.  >. ,  abs >.
18 eqid 2412 . . . . . . . . . . . . . . . . 17  |-  ( U 
BLnOp  W )  =  ( U  BLnOp  W )
19 eqid 2412 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  X  |->  ( w P ( T `  z ) ) )  =  ( w  e.  X  |->  ( w P ( T `  z
) ) )
204, 14, 16, 17, 18, 19ipblnfi 22318 . . . . . . . . . . . . . . . 16  |-  ( ( T `  z )  e.  X  ->  (
w  e.  X  |->  ( w P ( T `
 z ) ) )  e.  ( U 
BLnOp  W ) )
2113, 20syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  X )  ->  (
w  e.  X  |->  ( w P ( T `
 z ) ) )  e.  ( U 
BLnOp  W ) )
22 htthlem.10 . . . . . . . . . . . . . . 15  |-  F  =  ( z  e.  X  |->  ( w  e.  X  |->  ( w P ( T `  z ) ) ) )
2321, 22fmptd 5860 . . . . . . . . . . . . . 14  |-  ( ph  ->  F : X --> ( U 
BLnOp  W ) )
24 ffun 5560 . . . . . . . . . . . . . 14  |-  ( F : X --> ( U 
BLnOp  W )  ->  Fun  F )
2523, 24syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  Fun  F )
2625adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  X )  ->  Fun  F )
27 id 20 . . . . . . . . . . . . 13  |-  ( w  e.  K  ->  w  e.  K )
28 htthlem.11 . . . . . . . . . . . . 13  |-  K  =  ( F " {
z  e.  X  | 
( N `  z
)  <_  1 }
)
2927, 28syl6eleq 2502 . . . . . . . . . . . 12  |-  ( w  e.  K  ->  w  e.  ( F " {
z  e.  X  | 
( N `  z
)  <_  1 }
) )
30 fvelima 5745 . . . . . . . . . . . 12  |-  ( ( Fun  F  /\  w  e.  ( F " {
z  e.  X  | 
( N `  z
)  <_  1 }
) )  ->  E. y  e.  { z  e.  X  |  ( N `  z )  <_  1 }  ( F `  y )  =  w )
3126, 29, 30syl2an 464 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  X )  /\  w  e.  K )  ->  E. y  e.  { z  e.  X  |  ( N `  z )  <_  1 }  ( F `  y )  =  w )
3231ex 424 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  X )  ->  (
w  e.  K  ->  E. y  e.  { z  e.  X  |  ( N `  z )  <_  1 }  ( F `  y )  =  w ) )
33 fveq2 5695 . . . . . . . . . . . . . . 15  |-  ( z  =  y  ->  ( N `  z )  =  ( N `  y ) )
3433breq1d 4190 . . . . . . . . . . . . . 14  |-  ( z  =  y  ->  (
( N `  z
)  <_  1  <->  ( N `  y )  <_  1
) )
3534elrab 3060 . . . . . . . . . . . . 13  |-  ( y  e.  { z  e.  X  |  ( N `
 z )  <_ 
1 }  <->  ( y  e.  X  /\  ( N `  y )  <_  1 ) )
36 fveq2 5695 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  =  y  ->  ( T `  z )  =  ( T `  y ) )
3736oveq2d 6064 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  =  y  ->  (
w P ( T `
 z ) )  =  ( w P ( T `  y
) ) )
3837mpteq2dv 4264 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  y  ->  (
w  e.  X  |->  ( w P ( T `
 z ) ) )  =  ( w  e.  X  |->  ( w P ( T `  y ) ) ) )
394hlex 22361 . . . . . . . . . . . . . . . . . . . . 21  |-  X  e. 
_V
4039mptex 5933 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  X  |->  ( w P ( T `  y ) ) )  e.  _V
4138, 22, 40fvmpt 5773 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  X  ->  ( F `  y )  =  ( w  e.  X  |->  ( w P ( T `  y
) ) ) )
4241fveq1d 5697 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  X  ->  (
( F `  y
) `  x )  =  ( ( w  e.  X  |->  ( w P ( T `  y ) ) ) `
 x ) )
43 oveq1 6055 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  x  ->  (
w P ( T `
 y ) )  =  ( x P ( T `  y
) ) )
44 eqid 2412 . . . . . . . . . . . . . . . . . . 19  |-  ( w  e.  X  |->  ( w P ( T `  y ) ) )  =  ( w  e.  X  |->  ( w P ( T `  y
) ) )
45 ovex 6073 . . . . . . . . . . . . . . . . . . 19  |-  ( x P ( T `  y ) )  e. 
_V
4643, 44, 45fvmpt 5773 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  X  ->  (
( w  e.  X  |->  ( w P ( T `  y ) ) ) `  x
)  =  ( x P ( T `  y ) ) )
4742, 46sylan9eqr 2466 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  X  /\  y  e.  X )  ->  ( ( F `  y ) `  x
)  =  ( x P ( T `  y ) ) )
4847ad2ant2lr 729 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  X )  /\  (
y  e.  X  /\  ( N `  y )  <_  1 ) )  ->  ( ( F `
 y ) `  x )  =  ( x P ( T `
 y ) ) )
49 htthlem.9 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A. x  e.  X  A. y  e.  X  ( x P ( T `  y ) )  =  ( ( T `  x ) P y ) )
50 rsp2 2736 . . . . . . . . . . . . . . . . . . 19  |-  ( A. x  e.  X  A. y  e.  X  (
x P ( T `
 y ) )  =  ( ( T `
 x ) P y )  ->  (
( x  e.  X  /\  y  e.  X
)  ->  ( x P ( T `  y ) )  =  ( ( T `  x ) P y ) ) )
5149, 50syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( x  e.  X  /\  y  e.  X )  ->  (
x P ( T `
 y ) )  =  ( ( T `
 x ) P y ) ) )
5251impl 604 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  X )  /\  y  e.  X )  ->  (
x P ( T `
 y ) )  =  ( ( T `
 x ) P y ) )
5352adantrr 698 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  X )  /\  (
y  e.  X  /\  ( N `  y )  <_  1 ) )  ->  ( x P ( T `  y
) )  =  ( ( T `  x
) P y ) )
5448, 53eqtrd 2444 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  X )  /\  (
y  e.  X  /\  ( N `  y )  <_  1 ) )  ->  ( ( F `
 y ) `  x )  =  ( ( T `  x
) P y ) )
5554fveq2d 5699 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  X )  /\  (
y  e.  X  /\  ( N `  y )  <_  1 ) )  ->  ( abs `  (
( F `  y
) `  x )
)  =  ( abs `  ( ( T `  x ) P y ) ) )
56 simpl 444 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  X  /\  ( N `  y )  <_  1 )  -> 
y  e.  X )
574, 14dipcl 22172 . . . . . . . . . . . . . . . . . 18  |-  ( ( U  e.  NrmCVec  /\  ( T `  x )  e.  X  /\  y  e.  X )  ->  (
( T `  x
) P y )  e.  CC )
583, 57mp3an1 1266 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T `  x
)  e.  X  /\  y  e.  X )  ->  ( ( T `  x ) P y )  e.  CC )
599, 56, 58syl2an 464 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  X )  /\  (
y  e.  X  /\  ( N `  y )  <_  1 ) )  ->  ( ( T `
 x ) P y )  e.  CC )
6059abscld 12201 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  X )  /\  (
y  e.  X  /\  ( N `  y )  <_  1 ) )  ->  ( abs `  (
( T `  x
) P y ) )  e.  RR )
6112adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  X )  /\  (
y  e.  X  /\  ( N `  y )  <_  1 ) )  ->  ( N `  ( T `  x ) )  e.  RR )
624, 10nvcl 22109 . . . . . . . . . . . . . . . . . 18  |-  ( ( U  e.  NrmCVec  /\  y  e.  X )  ->  ( N `  y )  e.  RR )
633, 62mpan 652 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  X  ->  ( N `  y )  e.  RR )
6463ad2antrl 709 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  X )  /\  (
y  e.  X  /\  ( N `  y )  <_  1 ) )  ->  ( N `  y )  e.  RR )
6561, 64remulcld 9080 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  X )  /\  (
y  e.  X  /\  ( N `  y )  <_  1 ) )  ->  ( ( N `
 ( T `  x ) )  x.  ( N `  y
) )  e.  RR )
664, 10, 14, 16sii 22316 . . . . . . . . . . . . . . . 16  |-  ( ( ( T `  x
)  e.  X  /\  y  e.  X )  ->  ( abs `  (
( T `  x
) P y ) )  <_  ( ( N `  ( T `  x ) )  x.  ( N `  y
) ) )
679, 56, 66syl2an 464 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  X )  /\  (
y  e.  X  /\  ( N `  y )  <_  1 ) )  ->  ( abs `  (
( T `  x
) P y ) )  <_  ( ( N `  ( T `  x ) )  x.  ( N `  y
) ) )
68 1re 9054 . . . . . . . . . . . . . . . . . 18  |-  1  e.  RR
6968a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  X )  /\  (
y  e.  X  /\  ( N `  y )  <_  1 ) )  ->  1  e.  RR )
704, 10nvge0 22124 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( U  e.  NrmCVec  /\  ( T `  x )  e.  X )  ->  0  <_  ( N `  ( T `  x )
) )
713, 9, 70sylancr 645 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  X )  ->  0  <_  ( N `  ( T `  x )
) )
7212, 71jca 519 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  X )  ->  (
( N `  ( T `  x )
)  e.  RR  /\  0  <_  ( N `  ( T `  x ) ) ) )
7372adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  X )  /\  (
y  e.  X  /\  ( N `  y )  <_  1 ) )  ->  ( ( N `
 ( T `  x ) )  e.  RR  /\  0  <_ 
( N `  ( T `  x )
) ) )
74 simprr 734 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  X )  /\  (
y  e.  X  /\  ( N `  y )  <_  1 ) )  ->  ( N `  y )  <_  1
)
75 lemul2a 9829 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( N `  y )  e.  RR  /\  1  e.  RR  /\  ( ( N `  ( T `  x ) )  e.  RR  /\  0  <_  ( N `  ( T `  x ) ) ) )  /\  ( N `  y )  <_  1 )  -> 
( ( N `  ( T `  x ) )  x.  ( N `
 y ) )  <_  ( ( N `
 ( T `  x ) )  x.  1 ) )
7664, 69, 73, 74, 75syl31anc 1187 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  X )  /\  (
y  e.  X  /\  ( N `  y )  <_  1 ) )  ->  ( ( N `
 ( T `  x ) )  x.  ( N `  y
) )  <_  (
( N `  ( T `  x )
)  x.  1 ) )
7761recnd 9078 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  X )  /\  (
y  e.  X  /\  ( N `  y )  <_  1 ) )  ->  ( N `  ( T `  x ) )  e.  CC )
7877mulid1d 9069 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  X )  /\  (
y  e.  X  /\  ( N `  y )  <_  1 ) )  ->  ( ( N `
 ( T `  x ) )  x.  1 )  =  ( N `  ( T `
 x ) ) )
7976, 78breqtrd 4204 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  X )  /\  (
y  e.  X  /\  ( N `  y )  <_  1 ) )  ->  ( ( N `
 ( T `  x ) )  x.  ( N `  y
) )  <_  ( N `  ( T `  x ) ) )
8060, 65, 61, 67, 79letrd 9191 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  X )  /\  (
y  e.  X  /\  ( N `  y )  <_  1 ) )  ->  ( abs `  (
( T `  x
) P y ) )  <_  ( N `  ( T `  x
) ) )
8155, 80eqbrtrd 4200 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  X )  /\  (
y  e.  X  /\  ( N `  y )  <_  1 ) )  ->  ( abs `  (
( F `  y
) `  x )
)  <_  ( N `  ( T `  x
) ) )
8235, 81sylan2b 462 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  X )  /\  y  e.  { z  e.  X  |  ( N `  z )  <_  1 } )  ->  ( abs `  ( ( F `
 y ) `  x ) )  <_ 
( N `  ( T `  x )
) )
83 fveq1 5694 . . . . . . . . . . . . . 14  |-  ( ( F `  y )  =  w  ->  (
( F `  y
) `  x )  =  ( w `  x ) )
8483fveq2d 5699 . . . . . . . . . . . . 13  |-  ( ( F `  y )  =  w  ->  ( abs `  ( ( F `
 y ) `  x ) )  =  ( abs `  (
w `  x )
) )
8584breq1d 4190 . . . . . . . . . . . 12  |-  ( ( F `  y )  =  w  ->  (
( abs `  (
( F `  y
) `  x )
)  <_  ( N `  ( T `  x
) )  <->  ( abs `  ( w `  x
) )  <_  ( N `  ( T `  x ) ) ) )
8682, 85syl5ibcom 212 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  X )  /\  y  e.  { z  e.  X  |  ( N `  z )  <_  1 } )  ->  (
( F `  y
)  =  w  -> 
( abs `  (
w `  x )
)  <_  ( N `  ( T `  x
) ) ) )
8786rexlimdva 2798 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  X )  ->  ( E. y  e.  { z  e.  X  |  ( N `  z )  <_  1 }  ( F `  y )  =  w  ->  ( abs `  ( w `  x
) )  <_  ( N `  ( T `  x ) ) ) )
8832, 87syld 42 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  X )  ->  (
w  e.  K  -> 
( abs `  (
w `  x )
)  <_  ( N `  ( T `  x
) ) ) )
8988ralrimiv 2756 . . . . . . . 8  |-  ( (
ph  /\  x  e.  X )  ->  A. w  e.  K  ( abs `  ( w `  x
) )  <_  ( N `  ( T `  x ) ) )
90 breq2 4184 . . . . . . . . . 10  |-  ( z  =  ( N `  ( T `  x ) )  ->  ( ( abs `  ( w `  x ) )  <_ 
z  <->  ( abs `  (
w `  x )
)  <_  ( N `  ( T `  x
) ) ) )
9190ralbidv 2694 . . . . . . . . 9  |-  ( z  =  ( N `  ( T `  x ) )  ->  ( A. w  e.  K  ( abs `  ( w `  x ) )  <_ 
z  <->  A. w  e.  K  ( abs `  ( w `
 x ) )  <_  ( N `  ( T `  x ) ) ) )
9291rspcev 3020 . . . . . . . 8  |-  ( ( ( N `  ( T `  x )
)  e.  RR  /\  A. w  e.  K  ( abs `  ( w `
 x ) )  <_  ( N `  ( T `  x ) ) )  ->  E. z  e.  RR  A. w  e.  K  ( abs `  (
w `  x )
)  <_  z )
9312, 89, 92syl2anc 643 . . . . . . 7  |-  ( (
ph  /\  x  e.  X )  ->  E. z  e.  RR  A. w  e.  K  ( abs `  (
w `  x )
)  <_  z )
9493ralrimiva 2757 . . . . . 6  |-  ( ph  ->  A. x  e.  X  E. z  e.  RR  A. w  e.  K  ( abs `  ( w `
 x ) )  <_  z )
95 imassrn 5183 . . . . . . . . 9  |-  ( F
" { z  e.  X  |  ( N `
 z )  <_ 
1 } )  C_  ran  F
9628, 95eqsstri 3346 . . . . . . . 8  |-  K  C_  ran  F
97 frn 5564 . . . . . . . . 9  |-  ( F : X --> ( U 
BLnOp  W )  ->  ran  F 
C_  ( U  BLnOp  W ) )
9823, 97syl 16 . . . . . . . 8  |-  ( ph  ->  ran  F  C_  ( U  BLnOp  W ) )
9996, 98syl5ss 3327 . . . . . . 7  |-  ( ph  ->  K  C_  ( U  BLnOp  W ) )
100 hlobn 22351 . . . . . . . . 9  |-  ( U  e.  CHil OLD  ->  U  e. 
CBan )
1012, 100ax-mp 8 . . . . . . . 8  |-  U  e. 
CBan
10217cnnv 22129 . . . . . . . 8  |-  W  e.  NrmCVec
10317cnnvnm 22134 . . . . . . . . 9  |-  abs  =  ( normCV `  W )
104 eqid 2412 . . . . . . . . 9  |-  ( U
normOp OLD W )  =  ( U normOp OLD W
)
1054, 103, 104ubth 22336 . . . . . . . 8  |-  ( ( U  e.  CBan  /\  W  e.  NrmCVec  /\  K  C_  ( U  BLnOp  W ) )  ->  ( A. x  e.  X  E. z  e.  RR  A. w  e.  K  ( abs `  (
w `  x )
)  <_  z  <->  E. y  e.  RR  A. w  e.  K  ( ( U
normOp OLD W ) `  w )  <_  y
) )
106101, 102, 105mp3an12 1269 . . . . . . 7  |-  ( K 
C_  ( U  BLnOp  W )  ->  ( A. x  e.  X  E. z  e.  RR  A. w  e.  K  ( abs `  ( w `  x
) )  <_  z  <->  E. y  e.  RR  A. w  e.  K  (
( U normOp OLD W
) `  w )  <_  y ) )
10799, 106syl 16 . . . . . 6  |-  ( ph  ->  ( A. x  e.  X  E. z  e.  RR  A. w  e.  K  ( abs `  (
w `  x )
)  <_  z  <->  E. y  e.  RR  A. w  e.  K  ( ( U
normOp OLD W ) `  w )  <_  y
) )
10894, 107mpbid 202 . . . . 5  |-  ( ph  ->  E. y  e.  RR  A. w  e.  K  ( ( U normOp OLD W
) `  w )  <_  y )
109 simpr 448 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( N `  x )  <_  1 ) )  ->  ( x  e.  X  /\  ( N `
 x )  <_ 
1 ) )
110 fveq2 5695 . . . . . . . . . . . . . . . 16  |-  ( z  =  x  ->  ( N `  z )  =  ( N `  x ) )
111110breq1d 4190 . . . . . . . . . . . . . . 15  |-  ( z  =  x  ->  (
( N `  z
)  <_  1  <->  ( N `  x )  <_  1
) )
112111elrab 3060 . . . . . . . . . . . . . 14  |-  ( x  e.  { z  e.  X  |  ( N `
 z )  <_ 
1 }  <->  ( x  e.  X  /\  ( N `  x )  <_  1 ) )
113109, 112sylibr 204 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( N `  x )  <_  1 ) )  ->  x  e.  {
z  e.  X  | 
( N `  z
)  <_  1 }
)
114 fdm 5562 . . . . . . . . . . . . . . . . . 18  |-  ( F : X --> ( U 
BLnOp  W )  ->  dom  F  =  X )
11523, 114syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  F  =  X )
116115eleq2d 2479 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( x  e.  dom  F  <-> 
x  e.  X ) )
117116biimpar 472 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  X )  ->  x  e.  dom  F )
118 funfvima 5940 . . . . . . . . . . . . . . . 16  |-  ( ( Fun  F  /\  x  e.  dom  F )  -> 
( x  e.  {
z  e.  X  | 
( N `  z
)  <_  1 }  ->  ( F `  x
)  e.  ( F
" { z  e.  X  |  ( N `
 z )  <_ 
1 } ) ) )
11925, 118sylan 458 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  dom  F )  ->  (
x  e.  { z  e.  X  |  ( N `  z )  <_  1 }  ->  ( F `  x )  e.  ( F " { z  e.  X  |  ( N `  z )  <_  1 } ) ) )
120117, 119syldan 457 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  X )  ->  (
x  e.  { z  e.  X  |  ( N `  z )  <_  1 }  ->  ( F `  x )  e.  ( F " { z  e.  X  |  ( N `  z )  <_  1 } ) ) )
121120ad2ant2r 728 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( N `  x )  <_  1 ) )  ->  ( x  e. 
{ z  e.  X  |  ( N `  z )  <_  1 }  ->  ( F `  x )  e.  ( F " { z  e.  X  |  ( N `  z )  <_  1 } ) ) )
122113, 121mpd 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( N `  x )  <_  1 ) )  ->  ( F `  x )  e.  ( F " { z  e.  X  |  ( N `  z )  <_  1 } ) )
123122, 28syl6eleqr 2503 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( N `  x )  <_  1 ) )  ->  ( F `  x )  e.  K
)
124 fveq2 5695 . . . . . . . . . . . . 13  |-  ( w  =  ( F `  x )  ->  (
( U normOp OLD W
) `  w )  =  ( ( U
normOp OLD W ) `  ( F `  x ) ) )
125124breq1d 4190 . . . . . . . . . . . 12  |-  ( w  =  ( F `  x )  ->  (
( ( U normOp OLD W ) `  w
)  <_  y  <->  ( ( U normOp OLD W ) `  ( F `  x ) )  <_  y )
)
126125rspcv 3016 . . . . . . . . . . 11  |-  ( ( F `  x )  e.  K  ->  ( A. w  e.  K  ( ( U normOp OLD W ) `  w
)  <_  y  ->  ( ( U normOp OLD W
) `  ( F `  x ) )  <_ 
y ) )
127123, 126syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( N `  x )  <_  1 ) )  ->  ( A. w  e.  K  ( ( U normOp OLD W ) `  w )  <_  y  ->  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)
12812ad2ant2r 728 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( N `  ( T `  x
) )  e.  RR )
129128, 128remulcld 9080 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( ( N `  ( T `  x ) )  x.  ( N `  ( T `  x )
) )  e.  RR )
13023ffvelrnda 5837 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  X )  ->  ( F `  x )  e.  ( U  BLnOp  W ) )
13117cnnvba 22131 . . . . . . . . . . . . . . . . . . . 20  |-  CC  =  ( BaseSet `  W )
1324, 131, 104, 18nmblore 22248 . . . . . . . . . . . . . . . . . . 19  |-  ( ( U  e.  NrmCVec  /\  W  e.  NrmCVec  /\  ( F `  x )  e.  ( U  BLnOp  W )
)  ->  ( ( U normOp OLD W ) `  ( F `  x ) )  e.  RR )
1333, 102, 132mp3an12 1269 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  x )  e.  ( U  BLnOp  W )  ->  ( ( U normOp OLD W ) `  ( F `  x ) )  e.  RR )
134130, 133syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  X )  ->  (
( U normOp OLD W
) `  ( F `  x ) )  e.  RR )
135134ad2ant2r 728 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( ( U normOp OLD W ) `  ( F `  x ) )  e.  RR )
136135, 128remulcld 9080 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( (
( U normOp OLD W
) `  ( F `  x ) )  x.  ( N `  ( T `  x )
) )  e.  RR )
137 simplr 732 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  y  e.  RR )
138137, 128remulcld 9080 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( y  x.  ( N `  ( T `  x )
) )  e.  RR )
139 fveq2 5695 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  =  x  ->  ( T `  z )  =  ( T `  x ) )
140139oveq2d 6064 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  =  x  ->  (
w P ( T `
 z ) )  =  ( w P ( T `  x
) ) )
141140mpteq2dv 4264 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z  =  x  ->  (
w  e.  X  |->  ( w P ( T `
 z ) ) )  =  ( w  e.  X  |->  ( w P ( T `  x ) ) ) )
14239mptex 5933 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  e.  X  |->  ( w P ( T `  x ) ) )  e.  _V
143141, 22, 142fvmpt 5773 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  X  ->  ( F `  x )  =  ( w  e.  X  |->  ( w P ( T `  x
) ) ) )
144143adantl 453 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  X )  ->  ( F `  x )  =  ( w  e.  X  |->  ( w P ( T `  x
) ) ) )
145144fveq1d 5697 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  X )  ->  (
( F `  x
) `  ( T `  x ) )  =  ( ( w  e.  X  |->  ( w P ( T `  x
) ) ) `  ( T `  x ) ) )
146 oveq1 6055 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  =  ( T `  x )  ->  (
w P ( T `
 x ) )  =  ( ( T `
 x ) P ( T `  x
) ) )
147 eqid 2412 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  e.  X  |->  ( w P ( T `  x ) ) )  =  ( w  e.  X  |->  ( w P ( T `  x
) ) )
148 ovex 6073 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( T `  x ) P ( T `  x ) )  e. 
_V
149146, 147, 148fvmpt 5773 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( T `  x )  e.  X  ->  (
( w  e.  X  |->  ( w P ( T `  x ) ) ) `  ( T `  x )
)  =  ( ( T `  x ) P ( T `  x ) ) )
1509, 149syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  X )  ->  (
( w  e.  X  |->  ( w P ( T `  x ) ) ) `  ( T `  x )
)  =  ( ( T `  x ) P ( T `  x ) ) )
151145, 150eqtrd 2444 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  X )  ->  (
( F `  x
) `  ( T `  x ) )  =  ( ( T `  x ) P ( T `  x ) ) )
152151ad2ant2r 728 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( ( F `  x ) `  ( T `  x
) )  =  ( ( T `  x
) P ( T `
 x ) ) )
1539ad2ant2r 728 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( T `  x )  e.  X
)
1544, 10, 14ipidsq 22170 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( U  e.  NrmCVec  /\  ( T `  x )  e.  X )  ->  (
( T `  x
) P ( T `
 x ) )  =  ( ( N `
 ( T `  x ) ) ^
2 ) )
1553, 153, 154sylancr 645 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( ( T `  x ) P ( T `  x ) )  =  ( ( N `  ( T `  x ) ) ^ 2 ) )
156152, 155eqtrd 2444 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( ( F `  x ) `  ( T `  x
) )  =  ( ( N `  ( T `  x )
) ^ 2 ) )
157156fveq2d 5699 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( abs `  ( ( F `  x ) `  ( T `  x )
) )  =  ( abs `  ( ( N `  ( T `
 x ) ) ^ 2 ) ) )
158 resqcl 11412 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N `  ( T `
 x ) )  e.  RR  ->  (
( N `  ( T `  x )
) ^ 2 )  e.  RR )
159 sqge0 11421 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N `  ( T `
 x ) )  e.  RR  ->  0  <_  ( ( N `  ( T `  x ) ) ^ 2 ) )
160158, 159absidd 12188 . . . . . . . . . . . . . . . . . 18  |-  ( ( N `  ( T `
 x ) )  e.  RR  ->  ( abs `  ( ( N `
 ( T `  x ) ) ^
2 ) )  =  ( ( N `  ( T `  x ) ) ^ 2 ) )
161128, 160syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( abs `  ( ( N `  ( T `  x ) ) ^ 2 ) )  =  ( ( N `  ( T `
 x ) ) ^ 2 ) )
162128recnd 9078 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( N `  ( T `  x
) )  e.  CC )
163162sqvald 11483 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( ( N `  ( T `  x ) ) ^
2 )  =  ( ( N `  ( T `  x )
)  x.  ( N `
 ( T `  x ) ) ) )
164157, 161, 1633eqtrd 2448 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( abs `  ( ( F `  x ) `  ( T `  x )
) )  =  ( ( N `  ( T `  x )
)  x.  ( N `
 ( T `  x ) ) ) )
165130ad2ant2r 728 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( F `  x )  e.  ( U  BLnOp  W )
)
1664, 10, 103, 104, 18, 3, 102nmblolbi 22262 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  x
)  e.  ( U 
BLnOp  W )  /\  ( T `  x )  e.  X )  ->  ( abs `  ( ( F `
 x ) `  ( T `  x ) ) )  <_  (
( ( U normOp OLD W ) `  ( F `  x )
)  x.  ( N `
 ( T `  x ) ) ) )
167165, 153, 166syl2anc 643 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( abs `  ( ( F `  x ) `  ( T `  x )
) )  <_  (
( ( U normOp OLD W ) `  ( F `  x )
)  x.  ( N `
 ( T `  x ) ) ) )
168164, 167eqbrtrrd 4202 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( ( N `  ( T `  x ) )  x.  ( N `  ( T `  x )
) )  <_  (
( ( U normOp OLD W ) `  ( F `  x )
)  x.  ( N `
 ( T `  x ) ) ) )
1693, 153, 70sylancr 645 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  0  <_  ( N `  ( T `
 x ) ) )
170 simprr 734 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( ( U normOp OLD W ) `  ( F `  x ) )  <_  y )
171135, 137, 128, 169, 170lemul1ad 9914 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( (
( U normOp OLD W
) `  ( F `  x ) )  x.  ( N `  ( T `  x )
) )  <_  (
y  x.  ( N `
 ( T `  x ) ) ) )
172129, 136, 138, 168, 171letrd 9191 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( ( N `  ( T `  x ) )  x.  ( N `  ( T `  x )
) )  <_  (
y  x.  ( N `
 ( T `  x ) ) ) )
173 lemul1 9826 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N `  ( T `  x )
)  e.  RR  /\  y  e.  RR  /\  (
( N `  ( T `  x )
)  e.  RR  /\  0  <  ( N `  ( T `  x ) ) ) )  -> 
( ( N `  ( T `  x ) )  <_  y  <->  ( ( N `  ( T `  x ) )  x.  ( N `  ( T `  x )
) )  <_  (
y  x.  ( N `
 ( T `  x ) ) ) ) )
174173biimprd 215 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N `  ( T `  x )
)  e.  RR  /\  y  e.  RR  /\  (
( N `  ( T `  x )
)  e.  RR  /\  0  <  ( N `  ( T `  x ) ) ) )  -> 
( ( ( N `
 ( T `  x ) )  x.  ( N `  ( T `  x )
) )  <_  (
y  x.  ( N `
 ( T `  x ) ) )  ->  ( N `  ( T `  x ) )  <_  y )
)
1751743expia 1155 . . . . . . . . . . . . . . . 16  |-  ( ( ( N `  ( T `  x )
)  e.  RR  /\  y  e.  RR )  ->  ( ( ( N `
 ( T `  x ) )  e.  RR  /\  0  < 
( N `  ( T `  x )
) )  ->  (
( ( N `  ( T `  x ) )  x.  ( N `
 ( T `  x ) ) )  <_  ( y  x.  ( N `  ( T `  x )
) )  ->  ( N `  ( T `  x ) )  <_ 
y ) ) )
176175expdimp 427 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N `  ( T `  x ) )  e.  RR  /\  y  e.  RR )  /\  ( N `  ( T `  x )
)  e.  RR )  ->  ( 0  < 
( N `  ( T `  x )
)  ->  ( (
( N `  ( T `  x )
)  x.  ( N `
 ( T `  x ) ) )  <_  ( y  x.  ( N `  ( T `  x )
) )  ->  ( N `  ( T `  x ) )  <_ 
y ) ) )
177128, 137, 128, 176syl21anc 1183 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( 0  <  ( N `  ( T `  x ) )  ->  ( (
( N `  ( T `  x )
)  x.  ( N `
 ( T `  x ) ) )  <_  ( y  x.  ( N `  ( T `  x )
) )  ->  ( N `  ( T `  x ) )  <_ 
y ) ) )
178172, 177mpid 39 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( 0  <  ( N `  ( T `  x ) )  ->  ( N `  ( T `  x
) )  <_  y
) )
179 0re 9055 . . . . . . . . . . . . . . . 16  |-  0  e.  RR
180179a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  0  e.  RR )
1814, 131, 18blof 22247 . . . . . . . . . . . . . . . . . . 19  |-  ( ( U  e.  NrmCVec  /\  W  e.  NrmCVec  /\  ( F `  x )  e.  ( U  BLnOp  W )
)  ->  ( F `  x ) : X --> CC )
1823, 102, 181mp3an12 1269 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  x )  e.  ( U  BLnOp  W )  ->  ( F `  x ) : X --> CC )
183130, 182syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  X )  ->  ( F `  x ) : X --> CC )
184183ad2ant2r 728 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( F `  x ) : X --> CC )
1854, 131, 104nmooge0 22229 . . . . . . . . . . . . . . . . 17  |-  ( ( U  e.  NrmCVec  /\  W  e.  NrmCVec  /\  ( F `  x ) : X --> CC )  ->  0  <_ 
( ( U normOp OLD W ) `  ( F `  x )
) )
1863, 102, 185mp3an12 1269 . . . . . . . . . . . . . . . 16  |-  ( ( F `  x ) : X --> CC  ->  0  <_  ( ( U
normOp OLD W ) `  ( F `  x ) ) )
187184, 186syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  0  <_  ( ( U normOp OLD W
) `  ( F `  x ) ) )
188180, 135, 137, 187, 170letrd 9191 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  0  <_  y )
189 breq1 4183 . . . . . . . . . . . . . 14  |-  ( 0  =  ( N `  ( T `  x ) )  ->  ( 0  <_  y  <->  ( N `  ( T `  x
) )  <_  y
) )
190188, 189syl5ibcom 212 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( 0  =  ( N `  ( T `  x ) )  ->  ( N `  ( T `  x
) )  <_  y
) )
191 leloe 9125 . . . . . . . . . . . . . . 15  |-  ( ( 0  e.  RR  /\  ( N `  ( T `
 x ) )  e.  RR )  -> 
( 0  <_  ( N `  ( T `  x ) )  <->  ( 0  <  ( N `  ( T `  x ) )  \/  0  =  ( N `  ( T `  x )
) ) ) )
192179, 128, 191sylancr 645 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( 0  <_  ( N `  ( T `  x ) )  <->  ( 0  < 
( N `  ( T `  x )
)  \/  0  =  ( N `  ( T `  x )
) ) ) )
193169, 192mpbid 202 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( 0  <  ( N `  ( T `  x ) )  \/  0  =  ( N `  ( T `  x )
) ) )
194178, 190, 193mpjaod 371 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( ( U normOp OLD W ) `  ( F `  x )
)  <_  y )
)  ->  ( N `  ( T `  x
) )  <_  y
)
195194expr 599 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  RR )  /\  x  e.  X )  ->  (
( ( U normOp OLD W ) `  ( F `  x )
)  <_  y  ->  ( N `  ( T `
 x ) )  <_  y ) )
196195adantrr 698 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( N `  x )  <_  1 ) )  ->  ( ( ( U normOp OLD W ) `  ( F `  x ) )  <_  y  ->  ( N `  ( T `
 x ) )  <_  y ) )
197127, 196syld 42 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  RR )  /\  (
x  e.  X  /\  ( N `  x )  <_  1 ) )  ->  ( A. w  e.  K  ( ( U normOp OLD W ) `  w )  <_  y  ->  ( N `  ( T `  x )
)  <_  y )
)
198197expr 599 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  RR )  /\  x  e.  X )  ->  (
( N `  x
)  <_  1  ->  ( A. w  e.  K  ( ( U normOp OLD W ) `  w
)  <_  y  ->  ( N `  ( T `
 x ) )  <_  y ) ) )
199198com23 74 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  RR )  /\  x  e.  X )  ->  ( A. w  e.  K  ( ( U normOp OLD W ) `  w
)  <_  y  ->  ( ( N `  x
)  <_  1  ->  ( N `  ( T `
 x ) )  <_  y ) ) )
200199ralrimdva 2764 . . . . . 6  |-  ( (
ph  /\  y  e.  RR )  ->  ( A. w  e.  K  (
( U normOp OLD W
) `  w )  <_  y  ->  A. x  e.  X  ( ( N `  x )  <_  1  ->  ( N `  ( T `  x
) )  <_  y
) ) )
201200reximdva 2786 . . . . 5  |-  ( ph  ->  ( E. y  e.  RR  A. w  e.  K  ( ( U
normOp OLD W ) `  w )  <_  y  ->  E. y  e.  RR  A. x  e.  X  ( ( N `  x
)  <_  1  ->  ( N `  ( T `
 x ) )  <_  y ) ) )
202108, 201mpd 15 . . . 4  |-  ( ph  ->  E. y  e.  RR  A. x  e.  X  ( ( N `  x
)  <_  1  ->  ( N `  ( T `
 x ) )  <_  y ) )
203 eqid 2412 . . . . . 6  |-  ( U
normOp OLD U )  =  ( U normOp OLD U
)
2044, 4, 10, 10, 203, 3, 3nmobndi 22237 . . . . 5  |-  ( T : X --> X  -> 
( ( ( U
normOp OLD U ) `  T )  e.  RR  <->  E. y  e.  RR  A. x  e.  X  (
( N `  x
)  <_  1  ->  ( N `  ( T `
 x ) )  <_  y ) ) )
2058, 204syl 16 . . . 4  |-  ( ph  ->  ( ( ( U
normOp OLD U ) `  T )  e.  RR  <->  E. y  e.  RR  A. x  e.  X  (
( N `  x
)  <_  1  ->  ( N `  ( T `
 x ) )  <_  y ) ) )
206202, 205mpbird 224 . . 3  |-  ( ph  ->  ( ( U normOp OLD U ) `  T
)  e.  RR )
207 ltpnf 10685 . . 3  |-  ( ( ( U normOp OLD U
) `  T )  e.  RR  ->  ( ( U normOp OLD U ) `  T )  <  +oo )
208206, 207syl 16 . 2  |-  ( ph  ->  ( ( U normOp OLD U ) `  T
)  <  +oo )
209 htth.4 . . . 4  |-  B  =  ( U  BLnOp  U )
210203, 5, 209isblo 22244 . . 3  |-  ( ( U  e.  NrmCVec  /\  U  e.  NrmCVec )  ->  ( T  e.  B  <->  ( T  e.  L  /\  (
( U normOp OLD U
) `  T )  <  +oo ) ) )
2113, 3, 210mp2an 654 . 2  |-  ( T  e.  B  <->  ( T  e.  L  /\  (
( U normOp OLD U
) `  T )  <  +oo ) )
2121, 208, 211sylanbrc 646 1  |-  ( ph  ->  T  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359    /\ w3a 936    = wceq 1649    e. wcel 1721   A.wral 2674   E.wrex 2675   {crab 2678    C_ wss 3288   <.cop 3785   class class class wbr 4180    e. cmpt 4234   dom cdm 4845   ran crn 4846   "cima 4848   Fun wfun 5415   -->wf 5417   ` cfv 5421  (class class class)co 6048   CCcc 8952   RRcr 8953   0cc0 8954   1c1 8955    + caddc 8957    x. cmul 8959    +oocpnf 9081    < clt 9084    <_ cle 9085   2c2 10013   ^cexp 11345   abscabs 12002   NrmCVeccnv 22024   BaseSetcba 22026   normCVcnmcv 22030   .i OLDcdip 22157    LnOp clno 22202   normOp OLDcnmoo 22203    BLnOp cblo 22204   CPreHil OLDccphlo 22274   CBanccbn 22325   CHil
OLDchlo 22348
This theorem is referenced by:  htth  22382
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-rep 4288  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668  ax-inf2 7560  ax-dc 8290  ax-cnex 9010  ax-resscn 9011  ax-1cn 9012  ax-icn 9013  ax-addcl 9014  ax-addrcl 9015  ax-mulcl 9016  ax-mulrcl 9017  ax-mulcom 9018  ax-addass 9019  ax-mulass 9020  ax-distr 9021  ax-i2m1 9022  ax-1ne0 9023  ax-1rid 9024  ax-rnegex 9025  ax-rrecex 9026  ax-cnre 9027  ax-pre-lttri 9028  ax-pre-lttrn 9029  ax-pre-ltadd 9030  ax-pre-mulgt0 9031  ax-pre-sup 9032  ax-addf 9033  ax-mulf 9034
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-nel 2578  df-ral 2679  df-rex 2680  df-reu 2681  df-rmo 2682  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-pss 3304  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-tp 3790  df-op 3791  df-uni 3984  df-int 4019  df-iun 4063  df-iin 4064  df-br 4181  df-opab 4235  df-mpt 4236  df-tr 4271  df-eprel 4462  df-id 4466  df-po 4471  df-so 4472  df-fr 4509  df-se 4510  df-we 4511  df-ord 4552  df-on 4553  df-lim 4554  df-suc 4555  df-om 4813  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-isom 5430  df-ov 6051  df-oprab 6052  df-mpt2 6053  df-of 6272  df-1st 6316  df-2nd 6317  df-riota 6516  df-recs 6600  df-rdg 6635  df-1o 6691  df-2o 6692  df-oadd 6695  df-er 6872  df-map 6987  df-pm 6988  df-ixp 7031  df-en 7077  df-dom 7078  df-sdom 7079  df-fin 7080  df-fi 7382  df-sup 7412  df-oi 7443  df-card 7790  df-cda 8012  df-pnf 9086  df-mnf 9087  df-xr 9088  df-ltxr 9089  df-le 9090  df-sub 9257  df-neg 9258  df-div 9642  df-nn 9965  df-2 10022  df-3 10023  df-4 10024  df-5 10025  df-6 10026  df-7 10027  df-8 10028  df-9 10029  df-10 10030  df-n0 10186  df-z 10247  df-dec 10347  df-uz 10453  df-q 10539  df-rp 10577  df-xneg 10674  df-xadd 10675  df-xmul 10676  df-ioo 10884  df-ico 10886  df-icc 10887  df-fz 11008  df-fzo 11099  df-seq 11287  df-exp 11346  df-hash 11582  df-cj 11867  df-re 11868  df-im 11869  df-sqr 12003  df-abs 12004  df-clim 12245  df-sum 12443  df-struct 13434  df-ndx 13435  df-slot 13436  df-base 13437  df-sets 13438  df-ress 13439  df-plusg 13505  df-mulr 13506  df-starv 13507  df-sca 13508  df-vsca 13509  df-tset 13511  df-ple 13512  df-ds 13514  df-unif 13515  df-hom 13516  df-cco 13517  df-rest 13613  df-topn 13614  df-topgen 13630  df-pt 13631  df-prds 13634  df-xrs 13689  df-0g 13690  df-gsum 13691  df-qtop 13696  df-imas 13697  df-xps 13699  df-mre 13774  df-mrc 13775  df-acs 13777  df-mnd 14653  df-submnd 14702  df-mulg 14778  df-cntz 15079  df-cmn 15377  df-psmet 16657  df-xmet 16658  df-met 16659  df-bl 16660  df-mopn 16661  df-fbas 16662  df-fg 16663  df-cnfld 16667  df-top 16926  df-bases 16928  df-topon 16929  df-topsp 16930  df-cld 17046  df-ntr 17047  df-cls 17048  df-nei 17125  df-cn 17253  df-cnp 17254  df-lm 17255  df-t1 17340  df-haus 17341  df-cmp 17412  df-tx 17555  df-hmeo 17748  df-fil 17839  df-fm 17931  df-flim 17932  df-flf 17933  df-fcls 17934  df-xms 18311  df-ms 18312  df-tms 18313  df-cncf 18869  df-cfil 19169  df-cau 19170  df-cmet 19171  df-grpo 21740  df-gid 21741  df-ginv 21742  df-gdiv 21743  df-ablo 21831  df-vc 21986  df-nv 22032  df-va 22035  df-ba 22036  df-sm 22037  df-0v 22038  df-vs 22039  df-nmcv 22040  df-ims 22041  df-dip 22158  df-lno 22206  df-nmoo 22207  df-blo 22208  df-0o 22209  df-ph 22275  df-cbn 22326  df-hlo 22349
  Copyright terms: Public domain W3C validator