Metamath Proof Explorer

Theorem htthlem

Description: Lemma for htth . 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 , so by the Uniform Boundedness theorem ubth , 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.)

Ref Expression
Hypotheses htth.1 
|- X = ( BaseSet ` U )
htth.2 
|- P = ( .iOLD ` U )
htth.3 
|- L = ( U LnOp U )
htth.4 
|- B = ( U BLnOp U )
htthlem.5 
|- N = ( normCV ` U )
htthlem.6 
|- U e. CHilOLD
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 htthlem 
|- ( ph -> T e. B )

Proof

Step Hyp Ref Expression
1 htth.1 
 |-  X = ( BaseSet ` U )
2 htth.2 
 |-  P = ( .iOLD ` U )
3 htth.3 
 |-  L = ( U LnOp U )
4 htth.4 
 |-  B = ( U BLnOp U )
5 htthlem.5 
 |-  N = ( normCV ` U )
6 htthlem.6 
 |-  U e. CHilOLD
7 htthlem.7 
 |-  W = <. <. + , x. >. , abs >.
8 htthlem.8 
 |-  ( ph -> T e. L )
9 htthlem.9 
 |-  ( ph -> A. x e. X A. y e. X ( x P ( T ` y ) ) = ( ( T ` x ) P y ) )
10 htthlem.10 
 |-  F = ( z e. X |-> ( w e. X |-> ( w P ( T ` z ) ) ) )
11 htthlem.11 
 |-  K = ( F " { z e. X | ( N ` z ) <_ 1 } )
12 6 hlnvi 
 |-  U e. NrmCVec
13 1 1 3 lnof 
 |-  ( ( U e. NrmCVec /\ U e. NrmCVec /\ T e. L ) -> T : X --> X )
14 12 12 13 mp3an12 
 |-  ( T e. L -> T : X --> X )
15 8 14 syl 
 |-  ( ph -> T : X --> X )
16 15 ffvelcdmda 
 |-  ( ( ph /\ x e. X ) -> ( T ` x ) e. X )
17 1 5 nvcl 
 |-  ( ( U e. NrmCVec /\ ( T ` x ) e. X ) -> ( N ` ( T ` x ) ) e. RR )
18 12 16 17 sylancr 
 |-  ( ( ph /\ x e. X ) -> ( N ` ( T ` x ) ) e. RR )
19 15 ffvelcdmda 
 |-  ( ( ph /\ z e. X ) -> ( T ` z ) e. X )
20 hlph 
 |-  ( U e. CHilOLD -> U e. CPreHilOLD )
21 6 20 ax-mp 
 |-  U e. CPreHilOLD
22 eqid 
 |-  ( U BLnOp W ) = ( U BLnOp W )
23 eqid 
 |-  ( w e. X |-> ( w P ( T ` z ) ) ) = ( w e. X |-> ( w P ( T ` z ) ) )
24 1 2 21 7 22 23 ipblnfi 
 |-  ( ( T ` z ) e. X -> ( w e. X |-> ( w P ( T ` z ) ) ) e. ( U BLnOp W ) )
25 19 24 syl 
 |-  ( ( ph /\ z e. X ) -> ( w e. X |-> ( w P ( T ` z ) ) ) e. ( U BLnOp W ) )
26 25 10 fmptd 
 |-  ( ph -> F : X --> ( U BLnOp W ) )
27 26 ffund 
 |-  ( ph -> Fun F )
28 27 adantr 
 |-  ( ( ph /\ x e. X ) -> Fun F )
29 id 
 |-  ( w e. K -> w e. K )
30 29 11 eleqtrdi 
 |-  ( w e. K -> w e. ( F " { z e. X | ( N ` z ) <_ 1 } ) )
31 fvelima 
 |-  ( ( Fun F /\ w e. ( F " { z e. X | ( N ` z ) <_ 1 } ) ) -> E. y e. { z e. X | ( N ` z ) <_ 1 } ( F ` y ) = w )
32 28 30 31 syl2an 
 |-  ( ( ( ph /\ x e. X ) /\ w e. K ) -> E. y e. { z e. X | ( N ` z ) <_ 1 } ( F ` y ) = w )
33 32 ex 
 |-  ( ( ph /\ x e. X ) -> ( w e. K -> E. y e. { z e. X | ( N ` z ) <_ 1 } ( F ` y ) = w ) )
34 fveq2 
 |-  ( z = y -> ( N ` z ) = ( N ` y ) )
35 34 breq1d 
 |-  ( z = y -> ( ( N ` z ) <_ 1 <-> ( N ` y ) <_ 1 ) )
36 35 elrab 
 |-  ( y e. { z e. X | ( N ` z ) <_ 1 } <-> ( y e. X /\ ( N ` y ) <_ 1 ) )
37 fveq2 
 |-  ( z = y -> ( T ` z ) = ( T ` y ) )
38 37 oveq2d 
 |-  ( z = y -> ( w P ( T ` z ) ) = ( w P ( T ` y ) ) )
39 38 mpteq2dv 
 |-  ( z = y -> ( w e. X |-> ( w P ( T ` z ) ) ) = ( w e. X |-> ( w P ( T ` y ) ) ) )
40 39 10 1 mptfvmpt 
 |-  ( y e. X -> ( F ` y ) = ( w e. X |-> ( w P ( T ` y ) ) ) )
41 40 fveq1d 
 |-  ( y e. X -> ( ( F ` y ) ` x ) = ( ( w e. X |-> ( w P ( T ` y ) ) ) ` x ) )
42 oveq1 
 |-  ( w = x -> ( w P ( T ` y ) ) = ( x P ( T ` y ) ) )
43 eqid 
 |-  ( w e. X |-> ( w P ( T ` y ) ) ) = ( w e. X |-> ( w P ( T ` y ) ) )
44 ovex 
 |-  ( x P ( T ` y ) ) e. _V
45 42 43 44 fvmpt 
 |-  ( x e. X -> ( ( w e. X |-> ( w P ( T ` y ) ) ) ` x ) = ( x P ( T ` y ) ) )
46 41 45 sylan9eqr 
 |-  ( ( x e. X /\ y e. X ) -> ( ( F ` y ) ` x ) = ( x P ( T ` y ) ) )
47 46 ad2ant2lr 
 |-  ( ( ( ph /\ x e. X ) /\ ( y e. X /\ ( N ` y ) <_ 1 ) ) -> ( ( F ` y ) ` x ) = ( x P ( T ` y ) ) )
48 rsp2 
 |-  ( 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 ) ) )
49 9 48 syl 
 |-  ( ph -> ( ( x e. X /\ y e. X ) -> ( x P ( T ` y ) ) = ( ( T ` x ) P y ) ) )
50 49 impl 
 |-  ( ( ( ph /\ x e. X ) /\ y e. X ) -> ( x P ( T ` y ) ) = ( ( T ` x ) P y ) )
51 50 adantrr 
 |-  ( ( ( ph /\ x e. X ) /\ ( y e. X /\ ( N ` y ) <_ 1 ) ) -> ( x P ( T ` y ) ) = ( ( T ` x ) P y ) )
52 47 51 eqtrd 
 |-  ( ( ( ph /\ x e. X ) /\ ( y e. X /\ ( N ` y ) <_ 1 ) ) -> ( ( F ` y ) ` x ) = ( ( T ` x ) P y ) )
53 52 fveq2d 
 |-  ( ( ( ph /\ x e. X ) /\ ( y e. X /\ ( N ` y ) <_ 1 ) ) -> ( abs ` ( ( F ` y ) ` x ) ) = ( abs ` ( ( T ` x ) P y ) ) )
54 simpl 
 |-  ( ( y e. X /\ ( N ` y ) <_ 1 ) -> y e. X )
55 1 2 dipcl 
 |-  ( ( U e. NrmCVec /\ ( T ` x ) e. X /\ y e. X ) -> ( ( T ` x ) P y ) e. CC )
56 12 55 mp3an1 
 |-  ( ( ( T ` x ) e. X /\ y e. X ) -> ( ( T ` x ) P y ) e. CC )
57 16 54 56 syl2an 
 |-  ( ( ( ph /\ x e. X ) /\ ( y e. X /\ ( N ` y ) <_ 1 ) ) -> ( ( T ` x ) P y ) e. CC )
58 57 abscld 
 |-  ( ( ( ph /\ x e. X ) /\ ( y e. X /\ ( N ` y ) <_ 1 ) ) -> ( abs ` ( ( T ` x ) P y ) ) e. RR )
59 18 adantr 
 |-  ( ( ( ph /\ x e. X ) /\ ( y e. X /\ ( N ` y ) <_ 1 ) ) -> ( N ` ( T ` x ) ) e. RR )
60 1 5 nvcl 
 |-  ( ( U e. NrmCVec /\ y e. X ) -> ( N ` y ) e. RR )
61 12 60 mpan 
 |-  ( y e. X -> ( N ` y ) e. RR )
62 61 ad2antrl 
 |-  ( ( ( ph /\ x e. X ) /\ ( y e. X /\ ( N ` y ) <_ 1 ) ) -> ( N ` y ) e. RR )
63 59 62 remulcld 
 |-  ( ( ( ph /\ x e. X ) /\ ( y e. X /\ ( N ` y ) <_ 1 ) ) -> ( ( N ` ( T ` x ) ) x. ( N ` y ) ) e. RR )
64 1 5 2 21 sii 
 |-  ( ( ( T ` x ) e. X /\ y e. X ) -> ( abs ` ( ( T ` x ) P y ) ) <_ ( ( N ` ( T ` x ) ) x. ( N ` y ) ) )
65 16 54 64 syl2an 
 |-  ( ( ( ph /\ x e. X ) /\ ( y e. X /\ ( N ` y ) <_ 1 ) ) -> ( abs ` ( ( T ` x ) P y ) ) <_ ( ( N ` ( T ` x ) ) x. ( N ` y ) ) )
66 1red 
 |-  ( ( ( ph /\ x e. X ) /\ ( y e. X /\ ( N ` y ) <_ 1 ) ) -> 1 e. RR )
67 1 5 nvge0 
 |-  ( ( U e. NrmCVec /\ ( T ` x ) e. X ) -> 0 <_ ( N ` ( T ` x ) ) )
68 12 16 67 sylancr 
 |-  ( ( ph /\ x e. X ) -> 0 <_ ( N ` ( T ` x ) ) )
69 18 68 jca 
 |-  ( ( ph /\ x e. X ) -> ( ( N ` ( T ` x ) ) e. RR /\ 0 <_ ( N ` ( T ` x ) ) ) )
70 69 adantr 
 |-  ( ( ( ph /\ x e. X ) /\ ( y e. X /\ ( N ` y ) <_ 1 ) ) -> ( ( N ` ( T ` x ) ) e. RR /\ 0 <_ ( N ` ( T ` x ) ) ) )
71 simprr 
 |-  ( ( ( ph /\ x e. X ) /\ ( y e. X /\ ( N ` y ) <_ 1 ) ) -> ( N ` y ) <_ 1 )
72 lemul2a 
 |-  ( ( ( ( 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 ) )
73 62 66 70 71 72 syl31anc 
 |-  ( ( ( ph /\ x e. X ) /\ ( y e. X /\ ( N ` y ) <_ 1 ) ) -> ( ( N ` ( T ` x ) ) x. ( N ` y ) ) <_ ( ( N ` ( T ` x ) ) x. 1 ) )
74 59 recnd 
 |-  ( ( ( ph /\ x e. X ) /\ ( y e. X /\ ( N ` y ) <_ 1 ) ) -> ( N ` ( T ` x ) ) e. CC )
75 74 mulridd 
 |-  ( ( ( ph /\ x e. X ) /\ ( y e. X /\ ( N ` y ) <_ 1 ) ) -> ( ( N ` ( T ` x ) ) x. 1 ) = ( N ` ( T ` x ) ) )
76 73 75 breqtrd 
 |-  ( ( ( ph /\ x e. X ) /\ ( y e. X /\ ( N ` y ) <_ 1 ) ) -> ( ( N ` ( T ` x ) ) x. ( N ` y ) ) <_ ( N ` ( T ` x ) ) )
77 58 63 59 65 76 letrd 
 |-  ( ( ( ph /\ x e. X ) /\ ( y e. X /\ ( N ` y ) <_ 1 ) ) -> ( abs ` ( ( T ` x ) P y ) ) <_ ( N ` ( T ` x ) ) )
78 53 77 eqbrtrd 
 |-  ( ( ( ph /\ x e. X ) /\ ( y e. X /\ ( N ` y ) <_ 1 ) ) -> ( abs ` ( ( F ` y ) ` x ) ) <_ ( N ` ( T ` x ) ) )
79 36 78 sylan2b 
 |-  ( ( ( ph /\ x e. X ) /\ y e. { z e. X | ( N ` z ) <_ 1 } ) -> ( abs ` ( ( F ` y ) ` x ) ) <_ ( N ` ( T ` x ) ) )
80 fveq1 
 |-  ( ( F ` y ) = w -> ( ( F ` y ) ` x ) = ( w ` x ) )
81 80 fveq2d 
 |-  ( ( F ` y ) = w -> ( abs ` ( ( F ` y ) ` x ) ) = ( abs ` ( w ` x ) ) )
82 81 breq1d 
 |-  ( ( F ` y ) = w -> ( ( abs ` ( ( F ` y ) ` x ) ) <_ ( N ` ( T ` x ) ) <-> ( abs ` ( w ` x ) ) <_ ( N ` ( T ` x ) ) ) )
83 79 82 syl5ibcom 
 |-  ( ( ( ph /\ x e. X ) /\ y e. { z e. X | ( N ` z ) <_ 1 } ) -> ( ( F ` y ) = w -> ( abs ` ( w ` x ) ) <_ ( N ` ( T ` x ) ) ) )
84 83 rexlimdva 
 |-  ( ( ph /\ x e. X ) -> ( E. y e. { z e. X | ( N ` z ) <_ 1 } ( F ` y ) = w -> ( abs ` ( w ` x ) ) <_ ( N ` ( T ` x ) ) ) )
85 33 84 syld 
 |-  ( ( ph /\ x e. X ) -> ( w e. K -> ( abs ` ( w ` x ) ) <_ ( N ` ( T ` x ) ) ) )
86 85 ralrimiv 
 |-  ( ( ph /\ x e. X ) -> A. w e. K ( abs ` ( w ` x ) ) <_ ( N ` ( T ` x ) ) )
87 brralrspcev 
 |-  ( ( ( 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 )
88 18 86 87 syl2anc 
 |-  ( ( ph /\ x e. X ) -> E. z e. RR A. w e. K ( abs ` ( w ` x ) ) <_ z )
89 88 ralrimiva 
 |-  ( ph -> A. x e. X E. z e. RR A. w e. K ( abs ` ( w ` x ) ) <_ z )
90 imassrn 
 |-  ( F " { z e. X | ( N ` z ) <_ 1 } ) C_ ran F
91 11 90 eqsstri 
 |-  K C_ ran F
92 26 frnd 
 |-  ( ph -> ran F C_ ( U BLnOp W ) )
93 91 92 sstrid 
 |-  ( ph -> K C_ ( U BLnOp W ) )
94 hlobn 
 |-  ( U e. CHilOLD -> U e. CBan )
95 6 94 ax-mp 
 |-  U e. CBan
96 7 cnnv 
 |-  W e. NrmCVec
97 7 cnnvnm 
 |-  abs = ( normCV ` W )
98 eqid 
 |-  ( U normOpOLD W ) = ( U normOpOLD W )
99 1 97 98 ubth 
 |-  ( ( 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 normOpOLD W ) ` w ) <_ y ) )
100 95 96 99 mp3an12 
 |-  ( 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 normOpOLD W ) ` w ) <_ y ) )
101 93 100 syl 
 |-  ( 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 normOpOLD W ) ` w ) <_ y ) )
102 89 101 mpbid 
 |-  ( ph -> E. y e. RR A. w e. K ( ( U normOpOLD W ) ` w ) <_ y )
103 simpr 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( N ` x ) <_ 1 ) ) -> ( x e. X /\ ( N ` x ) <_ 1 ) )
104 fveq2 
 |-  ( z = x -> ( N ` z ) = ( N ` x ) )
105 104 breq1d 
 |-  ( z = x -> ( ( N ` z ) <_ 1 <-> ( N ` x ) <_ 1 ) )
106 105 elrab 
 |-  ( x e. { z e. X | ( N ` z ) <_ 1 } <-> ( x e. X /\ ( N ` x ) <_ 1 ) )
107 103 106 sylibr 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( N ` x ) <_ 1 ) ) -> x e. { z e. X | ( N ` z ) <_ 1 } )
108 10 25 dmmptd 
 |-  ( ph -> dom F = X )
109 108 eleq2d 
 |-  ( ph -> ( x e. dom F <-> x e. X ) )
110 109 biimpar 
 |-  ( ( ph /\ x e. X ) -> x e. dom F )
111 funfvima 
 |-  ( ( Fun F /\ x e. dom F ) -> ( x e. { z e. X | ( N ` z ) <_ 1 } -> ( F ` x ) e. ( F " { z e. X | ( N ` z ) <_ 1 } ) ) )
112 27 111 sylan 
 |-  ( ( ph /\ x e. dom F ) -> ( x e. { z e. X | ( N ` z ) <_ 1 } -> ( F ` x ) e. ( F " { z e. X | ( N ` z ) <_ 1 } ) ) )
113 110 112 syldan 
 |-  ( ( ph /\ x e. X ) -> ( x e. { z e. X | ( N ` z ) <_ 1 } -> ( F ` x ) e. ( F " { z e. X | ( N ` z ) <_ 1 } ) ) )
114 113 ad2ant2r 
 |-  ( ( ( 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 } ) ) )
115 107 114 mpd 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( N ` x ) <_ 1 ) ) -> ( F ` x ) e. ( F " { z e. X | ( N ` z ) <_ 1 } ) )
116 115 11 eleqtrrdi 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( N ` x ) <_ 1 ) ) -> ( F ` x ) e. K )
117 fveq2 
 |-  ( w = ( F ` x ) -> ( ( U normOpOLD W ) ` w ) = ( ( U normOpOLD W ) ` ( F ` x ) ) )
118 117 breq1d 
 |-  ( w = ( F ` x ) -> ( ( ( U normOpOLD W ) ` w ) <_ y <-> ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) )
119 118 rspcv 
 |-  ( ( F ` x ) e. K -> ( A. w e. K ( ( U normOpOLD W ) ` w ) <_ y -> ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) )
120 116 119 syl 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( N ` x ) <_ 1 ) ) -> ( A. w e. K ( ( U normOpOLD W ) ` w ) <_ y -> ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) )
121 18 ad2ant2r 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( N ` ( T ` x ) ) e. RR )
122 121 121 remulcld 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( ( N ` ( T ` x ) ) x. ( N ` ( T ` x ) ) ) e. RR )
123 26 ffvelcdmda 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) e. ( U BLnOp W ) )
124 7 cnnvba 
 |-  CC = ( BaseSet ` W )
125 1 124 98 22 nmblore 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ ( F ` x ) e. ( U BLnOp W ) ) -> ( ( U normOpOLD W ) ` ( F ` x ) ) e. RR )
126 12 96 125 mp3an12 
 |-  ( ( F ` x ) e. ( U BLnOp W ) -> ( ( U normOpOLD W ) ` ( F ` x ) ) e. RR )
127 123 126 syl 
 |-  ( ( ph /\ x e. X ) -> ( ( U normOpOLD W ) ` ( F ` x ) ) e. RR )
128 127 ad2ant2r 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( ( U normOpOLD W ) ` ( F ` x ) ) e. RR )
129 128 121 remulcld 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( ( ( U normOpOLD W ) ` ( F ` x ) ) x. ( N ` ( T ` x ) ) ) e. RR )
130 simplr 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> y e. RR )
131 130 121 remulcld 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( y x. ( N ` ( T ` x ) ) ) e. RR )
132 fveq2 
 |-  ( z = x -> ( T ` z ) = ( T ` x ) )
133 132 oveq2d 
 |-  ( z = x -> ( w P ( T ` z ) ) = ( w P ( T ` x ) ) )
134 133 mpteq2dv 
 |-  ( z = x -> ( w e. X |-> ( w P ( T ` z ) ) ) = ( w e. X |-> ( w P ( T ` x ) ) ) )
135 134 10 1 mptfvmpt 
 |-  ( x e. X -> ( F ` x ) = ( w e. X |-> ( w P ( T ` x ) ) ) )
136 135 adantl 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) = ( w e. X |-> ( w P ( T ` x ) ) ) )
137 136 fveq1d 
 |-  ( ( ph /\ x e. X ) -> ( ( F ` x ) ` ( T ` x ) ) = ( ( w e. X |-> ( w P ( T ` x ) ) ) ` ( T ` x ) ) )
138 oveq1 
 |-  ( w = ( T ` x ) -> ( w P ( T ` x ) ) = ( ( T ` x ) P ( T ` x ) ) )
139 eqid 
 |-  ( w e. X |-> ( w P ( T ` x ) ) ) = ( w e. X |-> ( w P ( T ` x ) ) )
140 ovex 
 |-  ( ( T ` x ) P ( T ` x ) ) e. _V
141 138 139 140 fvmpt 
 |-  ( ( T ` x ) e. X -> ( ( w e. X |-> ( w P ( T ` x ) ) ) ` ( T ` x ) ) = ( ( T ` x ) P ( T ` x ) ) )
142 16 141 syl 
 |-  ( ( ph /\ x e. X ) -> ( ( w e. X |-> ( w P ( T ` x ) ) ) ` ( T ` x ) ) = ( ( T ` x ) P ( T ` x ) ) )
143 137 142 eqtrd 
 |-  ( ( ph /\ x e. X ) -> ( ( F ` x ) ` ( T ` x ) ) = ( ( T ` x ) P ( T ` x ) ) )
144 143 ad2ant2r 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( ( F ` x ) ` ( T ` x ) ) = ( ( T ` x ) P ( T ` x ) ) )
145 16 ad2ant2r 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( T ` x ) e. X )
146 1 5 2 ipidsq 
 |-  ( ( U e. NrmCVec /\ ( T ` x ) e. X ) -> ( ( T ` x ) P ( T ` x ) ) = ( ( N ` ( T ` x ) ) ^ 2 ) )
147 12 145 146 sylancr 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( ( T ` x ) P ( T ` x ) ) = ( ( N ` ( T ` x ) ) ^ 2 ) )
148 144 147 eqtrd 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( ( F ` x ) ` ( T ` x ) ) = ( ( N ` ( T ` x ) ) ^ 2 ) )
149 148 fveq2d 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( abs ` ( ( F ` x ) ` ( T ` x ) ) ) = ( abs ` ( ( N ` ( T ` x ) ) ^ 2 ) ) )
150 resqcl 
 |-  ( ( N ` ( T ` x ) ) e. RR -> ( ( N ` ( T ` x ) ) ^ 2 ) e. RR )
151 sqge0 
 |-  ( ( N ` ( T ` x ) ) e. RR -> 0 <_ ( ( N ` ( T ` x ) ) ^ 2 ) )
152 150 151 absidd 
 |-  ( ( N ` ( T ` x ) ) e. RR -> ( abs ` ( ( N ` ( T ` x ) ) ^ 2 ) ) = ( ( N ` ( T ` x ) ) ^ 2 ) )
153 121 152 syl 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( abs ` ( ( N ` ( T ` x ) ) ^ 2 ) ) = ( ( N ` ( T ` x ) ) ^ 2 ) )
154 121 recnd 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( N ` ( T ` x ) ) e. CC )
155 154 sqvald 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( ( N ` ( T ` x ) ) ^ 2 ) = ( ( N ` ( T ` x ) ) x. ( N ` ( T ` x ) ) ) )
156 149 153 155 3eqtrd 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( abs ` ( ( F ` x ) ` ( T ` x ) ) ) = ( ( N ` ( T ` x ) ) x. ( N ` ( T ` x ) ) ) )
157 123 ad2ant2r 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( F ` x ) e. ( U BLnOp W ) )
158 1 5 97 98 22 12 96 nmblolbi 
 |-  ( ( ( F ` x ) e. ( U BLnOp W ) /\ ( T ` x ) e. X ) -> ( abs ` ( ( F ` x ) ` ( T ` x ) ) ) <_ ( ( ( U normOpOLD W ) ` ( F ` x ) ) x. ( N ` ( T ` x ) ) ) )
159 157 145 158 syl2anc 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( abs ` ( ( F ` x ) ` ( T ` x ) ) ) <_ ( ( ( U normOpOLD W ) ` ( F ` x ) ) x. ( N ` ( T ` x ) ) ) )
160 156 159 eqbrtrrd 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( ( N ` ( T ` x ) ) x. ( N ` ( T ` x ) ) ) <_ ( ( ( U normOpOLD W ) ` ( F ` x ) ) x. ( N ` ( T ` x ) ) ) )
161 12 145 67 sylancr 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> 0 <_ ( N ` ( T ` x ) ) )
162 simprr 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y )
163 128 130 121 161 162 lemul1ad 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( ( ( U normOpOLD W ) ` ( F ` x ) ) x. ( N ` ( T ` x ) ) ) <_ ( y x. ( N ` ( T ` x ) ) ) )
164 122 129 131 160 163 letrd 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( ( N ` ( T ` x ) ) x. ( N ` ( T ` x ) ) ) <_ ( y x. ( N ` ( T ` x ) ) ) )
165 lemul1 
 |-  ( ( ( 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 ) ) ) ) )
166 165 biimprd 
 |-  ( ( ( 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 ) )
167 166 3expia 
 |-  ( ( ( 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 ) ) )
168 167 expdimp 
 |-  ( ( ( ( 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 ) ) )
169 121 130 121 168 syl21anc 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( 0 < ( N ` ( T ` x ) ) -> ( ( ( N ` ( T ` x ) ) x. ( N ` ( T ` x ) ) ) <_ ( y x. ( N ` ( T ` x ) ) ) -> ( N ` ( T ` x ) ) <_ y ) ) )
170 164 169 mpid 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( 0 < ( N ` ( T ` x ) ) -> ( N ` ( T ` x ) ) <_ y ) )
171 0red 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> 0 e. RR )
172 1 124 22 blof 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ ( F ` x ) e. ( U BLnOp W ) ) -> ( F ` x ) : X --> CC )
173 12 96 172 mp3an12 
 |-  ( ( F ` x ) e. ( U BLnOp W ) -> ( F ` x ) : X --> CC )
174 123 173 syl 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) : X --> CC )
175 174 ad2ant2r 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( F ` x ) : X --> CC )
176 1 124 98 nmooge0 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ ( F ` x ) : X --> CC ) -> 0 <_ ( ( U normOpOLD W ) ` ( F ` x ) ) )
177 12 96 176 mp3an12 
 |-  ( ( F ` x ) : X --> CC -> 0 <_ ( ( U normOpOLD W ) ` ( F ` x ) ) )
178 175 177 syl 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> 0 <_ ( ( U normOpOLD W ) ` ( F ` x ) ) )
179 171 128 130 178 162 letrd 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> 0 <_ y )
180 breq1 
 |-  ( 0 = ( N ` ( T ` x ) ) -> ( 0 <_ y <-> ( N ` ( T ` x ) ) <_ y ) )
181 179 180 syl5ibcom 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( 0 = ( N ` ( T ` x ) ) -> ( N ` ( T ` x ) ) <_ y ) )
182 0re 
 |-  0 e. RR
183 leloe 
 |-  ( ( 0 e. RR /\ ( N ` ( T ` x ) ) e. RR ) -> ( 0 <_ ( N ` ( T ` x ) ) <-> ( 0 < ( N ` ( T ` x ) ) \/ 0 = ( N ` ( T ` x ) ) ) ) )
184 182 121 183 sylancr 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( 0 <_ ( N ` ( T ` x ) ) <-> ( 0 < ( N ` ( T ` x ) ) \/ 0 = ( N ` ( T ` x ) ) ) ) )
185 161 184 mpbid 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( 0 < ( N ` ( T ` x ) ) \/ 0 = ( N ` ( T ` x ) ) ) )
186 170 181 185 mpjaod 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( N ` ( T ` x ) ) <_ y )
187 186 expr 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. X ) -> ( ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y -> ( N ` ( T ` x ) ) <_ y ) )
188 187 adantrr 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( N ` x ) <_ 1 ) ) -> ( ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y -> ( N ` ( T ` x ) ) <_ y ) )
189 120 188 syld 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( N ` x ) <_ 1 ) ) -> ( A. w e. K ( ( U normOpOLD W ) ` w ) <_ y -> ( N ` ( T ` x ) ) <_ y ) )
190 189 expr 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. X ) -> ( ( N ` x ) <_ 1 -> ( A. w e. K ( ( U normOpOLD W ) ` w ) <_ y -> ( N ` ( T ` x ) ) <_ y ) ) )
191 190 com23 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. X ) -> ( A. w e. K ( ( U normOpOLD W ) ` w ) <_ y -> ( ( N ` x ) <_ 1 -> ( N ` ( T ` x ) ) <_ y ) ) )
192 191 ralrimdva 
 |-  ( ( ph /\ y e. RR ) -> ( A. w e. K ( ( U normOpOLD W ) ` w ) <_ y -> A. x e. X ( ( N ` x ) <_ 1 -> ( N ` ( T ` x ) ) <_ y ) ) )
193 192 reximdva 
 |-  ( ph -> ( E. y e. RR A. w e. K ( ( U normOpOLD W ) ` w ) <_ y -> E. y e. RR A. x e. X ( ( N ` x ) <_ 1 -> ( N ` ( T ` x ) ) <_ y ) ) )
194 102 193 mpd 
 |-  ( ph -> E. y e. RR A. x e. X ( ( N ` x ) <_ 1 -> ( N ` ( T ` x ) ) <_ y ) )
195 eqid 
 |-  ( U normOpOLD U ) = ( U normOpOLD U )
196 1 1 5 5 195 12 12 nmobndi 
 |-  ( T : X --> X -> ( ( ( U normOpOLD U ) ` T ) e. RR <-> E. y e. RR A. x e. X ( ( N ` x ) <_ 1 -> ( N ` ( T ` x ) ) <_ y ) ) )
197 15 196 syl 
 |-  ( ph -> ( ( ( U normOpOLD U ) ` T ) e. RR <-> E. y e. RR A. x e. X ( ( N ` x ) <_ 1 -> ( N ` ( T ` x ) ) <_ y ) ) )
198 194 197 mpbird 
 |-  ( ph -> ( ( U normOpOLD U ) ` T ) e. RR )
199 ltpnf 
 |-  ( ( ( U normOpOLD U ) ` T ) e. RR -> ( ( U normOpOLD U ) ` T ) < +oo )
200 198 199 syl 
 |-  ( ph -> ( ( U normOpOLD U ) ` T ) < +oo )
201 195 3 4 isblo 
 |-  ( ( U e. NrmCVec /\ U e. NrmCVec ) -> ( T e. B <-> ( T e. L /\ ( ( U normOpOLD U ) ` T ) < +oo ) ) )
202 12 12 201 mp2an 
 |-  ( T e. B <-> ( T e. L /\ ( ( U normOpOLD U ) ` T ) < +oo ) )
203 8 200 202 sylanbrc 
 |-  ( ph -> T e. B )