This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 fveq2 
 |-  ( z = x -> ( N ` z ) = ( N ` x ) )
104 103 breq1d 
 |-  ( z = x -> ( ( N ` z ) <_ 1 <-> ( N ` x ) <_ 1 ) )
105 104 elrab 
 |-  ( x e. { z e. X | ( N ` z ) <_ 1 } <-> ( x e. X /\ ( N ` x ) <_ 1 ) )
106 105 bilanri 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( N ` x ) <_ 1 ) ) -> x e. { z e. X | ( N ` z ) <_ 1 } )
107 10 25 dmmptd 
 |-  ( ph -> dom F = X )
108 107 eleq2d 
 |-  ( ph -> ( x e. dom F <-> x e. X ) )
109 108 biimpar 
 |-  ( ( ph /\ x e. X ) -> x e. dom F )
110 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 } ) ) )
111 27 110 sylan 
 |-  ( ( ph /\ x e. dom F ) -> ( x e. { z e. X | ( N ` z ) <_ 1 } -> ( F ` x ) e. ( F " { z e. X | ( N ` z ) <_ 1 } ) ) )
112 109 111 syldan 
 |-  ( ( ph /\ x e. X ) -> ( x e. { z e. X | ( N ` z ) <_ 1 } -> ( F ` x ) e. ( F " { z e. X | ( N ` z ) <_ 1 } ) ) )
113 112 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 } ) ) )
114 106 113 mpd 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( N ` x ) <_ 1 ) ) -> ( F ` x ) e. ( F " { z e. X | ( N ` z ) <_ 1 } ) )
115 114 11 eleqtrrdi 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( N ` x ) <_ 1 ) ) -> ( F ` x ) e. K )
116 fveq2 
 |-  ( w = ( F ` x ) -> ( ( U normOpOLD W ) ` w ) = ( ( U normOpOLD W ) ` ( F ` x ) ) )
117 116 breq1d 
 |-  ( w = ( F ` x ) -> ( ( ( U normOpOLD W ) ` w ) <_ y <-> ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) )
118 117 rspcv 
 |-  ( ( F ` x ) e. K -> ( A. w e. K ( ( U normOpOLD W ) ` w ) <_ y -> ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) )
119 115 118 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 ) )
120 18 ad2ant2r 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( N ` ( T ` x ) ) e. RR )
121 120 120 remulcld 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( ( N ` ( T ` x ) ) x. ( N ` ( T ` x ) ) ) e. RR )
122 26 ffvelcdmda 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) e. ( U BLnOp W ) )
123 7 cnnvba 
 |-  CC = ( BaseSet ` W )
124 1 123 98 22 nmblore 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ ( F ` x ) e. ( U BLnOp W ) ) -> ( ( U normOpOLD W ) ` ( F ` x ) ) e. RR )
125 12 96 124 mp3an12 
 |-  ( ( F ` x ) e. ( U BLnOp W ) -> ( ( U normOpOLD W ) ` ( F ` x ) ) e. RR )
126 122 125 syl 
 |-  ( ( ph /\ x e. X ) -> ( ( U normOpOLD W ) ` ( F ` x ) ) e. RR )
127 126 ad2ant2r 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( ( U normOpOLD W ) ` ( F ` x ) ) e. RR )
128 127 120 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 )
129 simplr 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> y e. RR )
130 129 120 remulcld 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( y x. ( N ` ( T ` x ) ) ) e. RR )
131 fveq2 
 |-  ( z = x -> ( T ` z ) = ( T ` x ) )
132 131 oveq2d 
 |-  ( z = x -> ( w P ( T ` z ) ) = ( w P ( T ` x ) ) )
133 132 mpteq2dv 
 |-  ( z = x -> ( w e. X |-> ( w P ( T ` z ) ) ) = ( w e. X |-> ( w P ( T ` x ) ) ) )
134 133 10 1 mptfvmpt 
 |-  ( x e. X -> ( F ` x ) = ( w e. X |-> ( w P ( T ` x ) ) ) )
135 134 adantl 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) = ( w e. X |-> ( w P ( T ` x ) ) ) )
136 135 fveq1d 
 |-  ( ( ph /\ x e. X ) -> ( ( F ` x ) ` ( T ` x ) ) = ( ( w e. X |-> ( w P ( T ` x ) ) ) ` ( T ` x ) ) )
137 oveq1 
 |-  ( w = ( T ` x ) -> ( w P ( T ` x ) ) = ( ( T ` x ) P ( T ` x ) ) )
138 eqid 
 |-  ( w e. X |-> ( w P ( T ` x ) ) ) = ( w e. X |-> ( w P ( T ` x ) ) )
139 ovex 
 |-  ( ( T ` x ) P ( T ` x ) ) e. _V
140 137 138 139 fvmpt 
 |-  ( ( T ` x ) e. X -> ( ( w e. X |-> ( w P ( T ` x ) ) ) ` ( T ` x ) ) = ( ( T ` x ) P ( T ` x ) ) )
141 16 140 syl 
 |-  ( ( ph /\ x e. X ) -> ( ( w e. X |-> ( w P ( T ` x ) ) ) ` ( T ` x ) ) = ( ( T ` x ) P ( T ` x ) ) )
142 136 141 eqtrd 
 |-  ( ( ph /\ x e. X ) -> ( ( F ` x ) ` ( T ` x ) ) = ( ( T ` x ) P ( T ` x ) ) )
143 142 ad2ant2r 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( ( F ` x ) ` ( T ` x ) ) = ( ( T ` x ) P ( T ` x ) ) )
144 16 ad2ant2r 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( T ` x ) e. X )
145 1 5 2 ipidsq 
 |-  ( ( U e. NrmCVec /\ ( T ` x ) e. X ) -> ( ( T ` x ) P ( T ` x ) ) = ( ( N ` ( T ` x ) ) ^ 2 ) )
146 12 144 145 sylancr 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( ( T ` x ) P ( T ` x ) ) = ( ( N ` ( T ` x ) ) ^ 2 ) )
147 143 146 eqtrd 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( ( F ` x ) ` ( T ` x ) ) = ( ( N ` ( T ` x ) ) ^ 2 ) )
148 147 fveq2d 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( abs ` ( ( F ` x ) ` ( T ` x ) ) ) = ( abs ` ( ( N ` ( T ` x ) ) ^ 2 ) ) )
149 resqcl 
 |-  ( ( N ` ( T ` x ) ) e. RR -> ( ( N ` ( T ` x ) ) ^ 2 ) e. RR )
150 sqge0 
 |-  ( ( N ` ( T ` x ) ) e. RR -> 0 <_ ( ( N ` ( T ` x ) ) ^ 2 ) )
151 149 150 absidd 
 |-  ( ( N ` ( T ` x ) ) e. RR -> ( abs ` ( ( N ` ( T ` x ) ) ^ 2 ) ) = ( ( N ` ( T ` x ) ) ^ 2 ) )
152 120 151 syl 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( abs ` ( ( N ` ( T ` x ) ) ^ 2 ) ) = ( ( N ` ( T ` x ) ) ^ 2 ) )
153 120 recnd 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( N ` ( T ` x ) ) e. CC )
154 153 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 ) ) ) )
155 148 152 154 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 ) ) ) )
156 122 ad2ant2r 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( F ` x ) e. ( U BLnOp W ) )
157 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 ) ) ) )
158 156 144 157 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 ) ) ) )
159 155 158 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 ) ) ) )
160 12 144 67 sylancr 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> 0 <_ ( N ` ( T ` x ) ) )
161 simprr 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y )
162 127 129 120 160 161 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 ) ) ) )
163 121 128 130 159 162 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 ) ) ) )
164 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 ) ) ) ) )
165 164 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 ) )
166 165 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 ) ) )
167 166 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 ) ) )
168 120 129 120 167 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 ) ) )
169 163 168 mpid 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( 0 < ( N ` ( T ` x ) ) -> ( N ` ( T ` x ) ) <_ y ) )
170 0red 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> 0 e. RR )
171 1 123 22 blof 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ ( F ` x ) e. ( U BLnOp W ) ) -> ( F ` x ) : X --> CC )
172 12 96 171 mp3an12 
 |-  ( ( F ` x ) e. ( U BLnOp W ) -> ( F ` x ) : X --> CC )
173 122 172 syl 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) : X --> CC )
174 173 ad2ant2r 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( F ` x ) : X --> CC )
175 1 123 98 nmooge0 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ ( F ` x ) : X --> CC ) -> 0 <_ ( ( U normOpOLD W ) ` ( F ` x ) ) )
176 12 96 175 mp3an12 
 |-  ( ( F ` x ) : X --> CC -> 0 <_ ( ( U normOpOLD W ) ` ( F ` x ) ) )
177 174 176 syl 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> 0 <_ ( ( U normOpOLD W ) ` ( F ` x ) ) )
178 170 127 129 177 161 letrd 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> 0 <_ y )
179 breq1 
 |-  ( 0 = ( N ` ( T ` x ) ) -> ( 0 <_ y <-> ( N ` ( T ` x ) ) <_ y ) )
180 178 179 syl5ibcom 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( 0 = ( N ` ( T ` x ) ) -> ( N ` ( T ` x ) ) <_ y ) )
181 0re 
 |-  0 e. RR
182 leloe 
 |-  ( ( 0 e. RR /\ ( N ` ( T ` x ) ) e. RR ) -> ( 0 <_ ( N ` ( T ` x ) ) <-> ( 0 < ( N ` ( T ` x ) ) \/ 0 = ( N ` ( T ` x ) ) ) ) )
183 181 120 182 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 ) ) ) ) )
184 160 183 mpbid 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( 0 < ( N ` ( T ` x ) ) \/ 0 = ( N ` ( T ` x ) ) ) )
185 169 180 184 mpjaod 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y ) ) -> ( N ` ( T ` x ) ) <_ y )
186 185 expr 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. X ) -> ( ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y -> ( N ` ( T ` x ) ) <_ y ) )
187 186 adantrr 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( N ` x ) <_ 1 ) ) -> ( ( ( U normOpOLD W ) ` ( F ` x ) ) <_ y -> ( N ` ( T ` x ) ) <_ y ) )
188 119 187 syld 
 |-  ( ( ( ph /\ y e. RR ) /\ ( x e. X /\ ( N ` x ) <_ 1 ) ) -> ( A. w e. K ( ( U normOpOLD W ) ` w ) <_ y -> ( N ` ( T ` x ) ) <_ y ) )
189 188 expr 
 |-  ( ( ( 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 com23 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. X ) -> ( A. w e. K ( ( U normOpOLD W ) ` w ) <_ y -> ( ( N ` x ) <_ 1 -> ( N ` ( T ` x ) ) <_ y ) ) )
191 190 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 ) ) )
192 191 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 ) ) )
193 102 192 mpd 
 |-  ( ph -> E. y e. RR A. x e. X ( ( N ` x ) <_ 1 -> ( N ` ( T ` x ) ) <_ y ) )
194 eqid 
 |-  ( U normOpOLD U ) = ( U normOpOLD U )
195 1 1 5 5 194 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 ) ) )
196 15 195 syl 
 |-  ( ph -> ( ( ( U normOpOLD U ) ` T ) e. RR <-> E. y e. RR A. x e. X ( ( N ` x ) <_ 1 -> ( N ` ( T ` x ) ) <_ y ) ) )
197 193 196 mpbird 
 |-  ( ph -> ( ( U normOpOLD U ) ` T ) e. RR )
198 ltpnf 
 |-  ( ( ( U normOpOLD U ) ` T ) e. RR -> ( ( U normOpOLD U ) ` T ) < +oo )
199 197 198 syl 
 |-  ( ph -> ( ( U normOpOLD U ) ` T ) < +oo )
200 194 3 4 isblo 
 |-  ( ( U e. NrmCVec /\ U e. NrmCVec ) -> ( T e. B <-> ( T e. L /\ ( ( U normOpOLD U ) ` T ) < +oo ) ) )
201 12 12 200 mp2an 
 |-  ( T e. B <-> ( T e. L /\ ( ( U normOpOLD U ) ` T ) < +oo ) )
202 8 199 201 sylanbrc 
 |-  ( ph -> T e. B )