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

Metamath Proof Explorer

Theorem blocnilem

Description: Lemma for blocni and lnocni . If a linear operator is continuous at any point, it is bounded. (Contributed by NM, 17-Dec-2007) (Revised by Mario Carneiro, 10-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses blocni.8 
|- C = ( IndMet ` U )
blocni.d 
|- D = ( IndMet ` W )
blocni.j 
|- J = ( MetOpen ` C )
blocni.k 
|- K = ( MetOpen ` D )
blocni.4 
|- L = ( U LnOp W )
blocni.5 
|- B = ( U BLnOp W )
blocni.u 
|- U e. NrmCVec
blocni.w 
|- W e. NrmCVec
blocni.l 
|- T e. L
blocnilem.1 
|- X = ( BaseSet ` U )
Assertion blocnilem 
|- ( ( P e. X /\ T e. ( ( J CnP K ) ` P ) ) -> T e. B )

Proof

Step Hyp Ref Expression
1 blocni.8 
 |-  C = ( IndMet ` U )
2 blocni.d 
 |-  D = ( IndMet ` W )
3 blocni.j 
 |-  J = ( MetOpen ` C )
4 blocni.k 
 |-  K = ( MetOpen ` D )
5 blocni.4 
 |-  L = ( U LnOp W )
6 blocni.5 
 |-  B = ( U BLnOp W )
7 blocni.u 
 |-  U e. NrmCVec
8 blocni.w 
 |-  W e. NrmCVec
9 blocni.l 
 |-  T e. L
10 blocnilem.1 
 |-  X = ( BaseSet ` U )
11 10 1 imsxmet 
 |-  ( U e. NrmCVec -> C e. ( *Met ` X ) )
12 7 11 ax-mp 
 |-  C e. ( *Met ` X )
13 eqid 
 |-  ( BaseSet ` W ) = ( BaseSet ` W )
14 13 2 imsxmet 
 |-  ( W e. NrmCVec -> D e. ( *Met ` ( BaseSet ` W ) ) )
15 8 14 ax-mp 
 |-  D e. ( *Met ` ( BaseSet ` W ) )
16 1rp 
 |-  1 e. RR+
17 3 4 metcnpi3 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` ( BaseSet ` W ) ) ) /\ ( T e. ( ( J CnP K ) ` P ) /\ 1 e. RR+ ) ) -> E. y e. RR+ A. x e. X ( ( x C P ) <_ y -> ( ( T ` x ) D ( T ` P ) ) <_ 1 ) )
18 16 17 mpanr2 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` ( BaseSet ` W ) ) ) /\ T e. ( ( J CnP K ) ` P ) ) -> E. y e. RR+ A. x e. X ( ( x C P ) <_ y -> ( ( T ` x ) D ( T ` P ) ) <_ 1 ) )
19 12 15 18 mpanl12 
 |-  ( T e. ( ( J CnP K ) ` P ) -> E. y e. RR+ A. x e. X ( ( x C P ) <_ y -> ( ( T ` x ) D ( T ` P ) ) <_ 1 ) )
20 rpreccl 
 |-  ( y e. RR+ -> ( 1 / y ) e. RR+ )
21 20 rpred 
 |-  ( y e. RR+ -> ( 1 / y ) e. RR )
22 21 ad2antlr 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ A. x e. X ( ( x C P ) <_ y -> ( ( T ` x ) D ( T ` P ) ) <_ 1 ) ) -> ( 1 / y ) e. RR )
23 eqid 
 |-  ( -v ` U ) = ( -v ` U )
24 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
25 10 23 24 1 imsdval 
 |-  ( ( U e. NrmCVec /\ x e. X /\ P e. X ) -> ( x C P ) = ( ( normCV ` U ) ` ( x ( -v ` U ) P ) ) )
26 7 25 mp3an1 
 |-  ( ( x e. X /\ P e. X ) -> ( x C P ) = ( ( normCV ` U ) ` ( x ( -v ` U ) P ) ) )
27 26 breq1d 
 |-  ( ( x e. X /\ P e. X ) -> ( ( x C P ) <_ y <-> ( ( normCV ` U ) ` ( x ( -v ` U ) P ) ) <_ y ) )
28 10 13 5 lnof 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> T : X --> ( BaseSet ` W ) )
29 7 8 9 28 mp3an 
 |-  T : X --> ( BaseSet ` W )
30 29 ffvelcdmi 
 |-  ( x e. X -> ( T ` x ) e. ( BaseSet ` W ) )
31 29 ffvelcdmi 
 |-  ( P e. X -> ( T ` P ) e. ( BaseSet ` W ) )
32 eqid 
 |-  ( -v ` W ) = ( -v ` W )
33 eqid 
 |-  ( normCV ` W ) = ( normCV ` W )
34 13 32 33 2 imsdval 
 |-  ( ( W e. NrmCVec /\ ( T ` x ) e. ( BaseSet ` W ) /\ ( T ` P ) e. ( BaseSet ` W ) ) -> ( ( T ` x ) D ( T ` P ) ) = ( ( normCV ` W ) ` ( ( T ` x ) ( -v ` W ) ( T ` P ) ) ) )
35 8 34 mp3an1 
 |-  ( ( ( T ` x ) e. ( BaseSet ` W ) /\ ( T ` P ) e. ( BaseSet ` W ) ) -> ( ( T ` x ) D ( T ` P ) ) = ( ( normCV ` W ) ` ( ( T ` x ) ( -v ` W ) ( T ` P ) ) ) )
36 30 31 35 syl2an 
 |-  ( ( x e. X /\ P e. X ) -> ( ( T ` x ) D ( T ` P ) ) = ( ( normCV ` W ) ` ( ( T ` x ) ( -v ` W ) ( T ` P ) ) ) )
37 7 8 9 3pm3.2i 
 |-  ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L )
38 10 23 32 5 lnosub 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( x e. X /\ P e. X ) ) -> ( T ` ( x ( -v ` U ) P ) ) = ( ( T ` x ) ( -v ` W ) ( T ` P ) ) )
39 37 38 mpan 
 |-  ( ( x e. X /\ P e. X ) -> ( T ` ( x ( -v ` U ) P ) ) = ( ( T ` x ) ( -v ` W ) ( T ` P ) ) )
40 39 fveq2d 
 |-  ( ( x e. X /\ P e. X ) -> ( ( normCV ` W ) ` ( T ` ( x ( -v ` U ) P ) ) ) = ( ( normCV ` W ) ` ( ( T ` x ) ( -v ` W ) ( T ` P ) ) ) )
41 36 40 eqtr4d 
 |-  ( ( x e. X /\ P e. X ) -> ( ( T ` x ) D ( T ` P ) ) = ( ( normCV ` W ) ` ( T ` ( x ( -v ` U ) P ) ) ) )
42 41 breq1d 
 |-  ( ( x e. X /\ P e. X ) -> ( ( ( T ` x ) D ( T ` P ) ) <_ 1 <-> ( ( normCV ` W ) ` ( T ` ( x ( -v ` U ) P ) ) ) <_ 1 ) )
43 27 42 imbi12d 
 |-  ( ( x e. X /\ P e. X ) -> ( ( ( x C P ) <_ y -> ( ( T ` x ) D ( T ` P ) ) <_ 1 ) <-> ( ( ( normCV ` U ) ` ( x ( -v ` U ) P ) ) <_ y -> ( ( normCV ` W ) ` ( T ` ( x ( -v ` U ) P ) ) ) <_ 1 ) ) )
44 43 ancoms 
 |-  ( ( P e. X /\ x e. X ) -> ( ( ( x C P ) <_ y -> ( ( T ` x ) D ( T ` P ) ) <_ 1 ) <-> ( ( ( normCV ` U ) ` ( x ( -v ` U ) P ) ) <_ y -> ( ( normCV ` W ) ` ( T ` ( x ( -v ` U ) P ) ) ) <_ 1 ) ) )
45 44 adantlr 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ x e. X ) -> ( ( ( x C P ) <_ y -> ( ( T ` x ) D ( T ` P ) ) <_ 1 ) <-> ( ( ( normCV ` U ) ` ( x ( -v ` U ) P ) ) <_ y -> ( ( normCV ` W ) ` ( T ` ( x ( -v ` U ) P ) ) ) <_ 1 ) ) )
46 45 ralbidva 
 |-  ( ( P e. X /\ y e. RR+ ) -> ( A. x e. X ( ( x C P ) <_ y -> ( ( T ` x ) D ( T ` P ) ) <_ 1 ) <-> A. x e. X ( ( ( normCV ` U ) ` ( x ( -v ` U ) P ) ) <_ y -> ( ( normCV ` W ) ` ( T ` ( x ( -v ` U ) P ) ) ) <_ 1 ) ) )
47 2fveq3 
 |-  ( z = ( 0vec ` U ) -> ( ( normCV ` W ) ` ( T ` z ) ) = ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) )
48 fveq2 
 |-  ( z = ( 0vec ` U ) -> ( ( normCV ` U ) ` z ) = ( ( normCV ` U ) ` ( 0vec ` U ) ) )
49 48 oveq2d 
 |-  ( z = ( 0vec ` U ) -> ( ( 1 / y ) x. ( ( normCV ` U ) ` z ) ) = ( ( 1 / y ) x. ( ( normCV ` U ) ` ( 0vec ` U ) ) ) )
50 47 49 breq12d 
 |-  ( z = ( 0vec ` U ) -> ( ( ( normCV ` W ) ` ( T ` z ) ) <_ ( ( 1 / y ) x. ( ( normCV ` U ) ` z ) ) <-> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) <_ ( ( 1 / y ) x. ( ( normCV ` U ) ` ( 0vec ` U ) ) ) ) )
51 7 a1i 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> U e. NrmCVec )
52 simpll 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> P e. X )
53 simpr 
 |-  ( ( P e. X /\ y e. RR+ ) -> y e. RR+ )
54 10 24 nvcl 
 |-  ( ( U e. NrmCVec /\ z e. X ) -> ( ( normCV ` U ) ` z ) e. RR )
55 7 54 mpan 
 |-  ( z e. X -> ( ( normCV ` U ) ` z ) e. RR )
56 55 adantr 
 |-  ( ( z e. X /\ z =/= ( 0vec ` U ) ) -> ( ( normCV ` U ) ` z ) e. RR )
57 eqid 
 |-  ( 0vec ` U ) = ( 0vec ` U )
58 10 57 24 nvgt0 
 |-  ( ( U e. NrmCVec /\ z e. X ) -> ( z =/= ( 0vec ` U ) <-> 0 < ( ( normCV ` U ) ` z ) ) )
59 7 58 mpan 
 |-  ( z e. X -> ( z =/= ( 0vec ` U ) <-> 0 < ( ( normCV ` U ) ` z ) ) )
60 59 biimpa 
 |-  ( ( z e. X /\ z =/= ( 0vec ` U ) ) -> 0 < ( ( normCV ` U ) ` z ) )
61 56 60 elrpd 
 |-  ( ( z e. X /\ z =/= ( 0vec ` U ) ) -> ( ( normCV ` U ) ` z ) e. RR+ )
62 rpdivcl 
 |-  ( ( y e. RR+ /\ ( ( normCV ` U ) ` z ) e. RR+ ) -> ( y / ( ( normCV ` U ) ` z ) ) e. RR+ )
63 53 61 62 syl2an 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( y / ( ( normCV ` U ) ` z ) ) e. RR+ )
64 63 rpcnd 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( y / ( ( normCV ` U ) ` z ) ) e. CC )
65 simprl 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> z e. X )
66 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
67 10 66 nvscl 
 |-  ( ( U e. NrmCVec /\ ( y / ( ( normCV ` U ) ` z ) ) e. CC /\ z e. X ) -> ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) e. X )
68 51 64 65 67 syl3anc 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) e. X )
69 eqid 
 |-  ( +v ` U ) = ( +v ` U )
70 10 69 23 nvpncan2 
 |-  ( ( U e. NrmCVec /\ P e. X /\ ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) e. X ) -> ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) = ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) )
71 51 52 68 70 syl3anc 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) = ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) )
72 71 fveq2d 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( ( normCV ` U ) ` ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) ) = ( ( normCV ` U ) ` ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) )
73 63 rprege0d 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( ( y / ( ( normCV ` U ) ` z ) ) e. RR /\ 0 <_ ( y / ( ( normCV ` U ) ` z ) ) ) )
74 10 66 24 nvsge0 
 |-  ( ( U e. NrmCVec /\ ( ( y / ( ( normCV ` U ) ` z ) ) e. RR /\ 0 <_ ( y / ( ( normCV ` U ) ` z ) ) ) /\ z e. X ) -> ( ( normCV ` U ) ` ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) = ( ( y / ( ( normCV ` U ) ` z ) ) x. ( ( normCV ` U ) ` z ) ) )
75 51 73 65 74 syl3anc 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( ( normCV ` U ) ` ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) = ( ( y / ( ( normCV ` U ) ` z ) ) x. ( ( normCV ` U ) ` z ) ) )
76 rpcn 
 |-  ( y e. RR+ -> y e. CC )
77 76 ad2antlr 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> y e. CC )
78 55 ad2antrl 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( ( normCV ` U ) ` z ) e. RR )
79 78 recnd 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( ( normCV ` U ) ` z ) e. CC )
80 10 57 24 nvz 
 |-  ( ( U e. NrmCVec /\ z e. X ) -> ( ( ( normCV ` U ) ` z ) = 0 <-> z = ( 0vec ` U ) ) )
81 7 80 mpan 
 |-  ( z e. X -> ( ( ( normCV ` U ) ` z ) = 0 <-> z = ( 0vec ` U ) ) )
82 81 necon3bid 
 |-  ( z e. X -> ( ( ( normCV ` U ) ` z ) =/= 0 <-> z =/= ( 0vec ` U ) ) )
83 82 biimpar 
 |-  ( ( z e. X /\ z =/= ( 0vec ` U ) ) -> ( ( normCV ` U ) ` z ) =/= 0 )
84 83 adantl 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( ( normCV ` U ) ` z ) =/= 0 )
85 77 79 84 divcan1d 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( ( y / ( ( normCV ` U ) ` z ) ) x. ( ( normCV ` U ) ` z ) ) = y )
86 72 75 85 3eqtrd 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( ( normCV ` U ) ` ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) ) = y )
87 rpre 
 |-  ( y e. RR+ -> y e. RR )
88 87 leidd 
 |-  ( y e. RR+ -> y <_ y )
89 88 ad2antlr 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> y <_ y )
90 86 89 eqbrtrd 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( ( normCV ` U ) ` ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) ) <_ y )
91 10 69 nvgcl 
 |-  ( ( U e. NrmCVec /\ P e. X /\ ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) e. X ) -> ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) e. X )
92 51 52 68 91 syl3anc 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) e. X )
93 fvoveq1 
 |-  ( x = ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) -> ( ( normCV ` U ) ` ( x ( -v ` U ) P ) ) = ( ( normCV ` U ) ` ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) ) )
94 93 breq1d 
 |-  ( x = ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) -> ( ( ( normCV ` U ) ` ( x ( -v ` U ) P ) ) <_ y <-> ( ( normCV ` U ) ` ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) ) <_ y ) )
95 fvoveq1 
 |-  ( x = ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) -> ( T ` ( x ( -v ` U ) P ) ) = ( T ` ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) ) )
96 95 fveq2d 
 |-  ( x = ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) -> ( ( normCV ` W ) ` ( T ` ( x ( -v ` U ) P ) ) ) = ( ( normCV ` W ) ` ( T ` ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) ) ) )
97 96 breq1d 
 |-  ( x = ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) -> ( ( ( normCV ` W ) ` ( T ` ( x ( -v ` U ) P ) ) ) <_ 1 <-> ( ( normCV ` W ) ` ( T ` ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) ) ) <_ 1 ) )
98 94 97 imbi12d 
 |-  ( x = ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) -> ( ( ( ( normCV ` U ) ` ( x ( -v ` U ) P ) ) <_ y -> ( ( normCV ` W ) ` ( T ` ( x ( -v ` U ) P ) ) ) <_ 1 ) <-> ( ( ( normCV ` U ) ` ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) ) <_ y -> ( ( normCV ` W ) ` ( T ` ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) ) ) <_ 1 ) ) )
99 98 rspcv 
 |-  ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) e. X -> ( A. x e. X ( ( ( normCV ` U ) ` ( x ( -v ` U ) P ) ) <_ y -> ( ( normCV ` W ) ` ( T ` ( x ( -v ` U ) P ) ) ) <_ 1 ) -> ( ( ( normCV ` U ) ` ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) ) <_ y -> ( ( normCV ` W ) ` ( T ` ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) ) ) <_ 1 ) ) )
100 92 99 syl 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( A. x e. X ( ( ( normCV ` U ) ` ( x ( -v ` U ) P ) ) <_ y -> ( ( normCV ` W ) ` ( T ` ( x ( -v ` U ) P ) ) ) <_ 1 ) -> ( ( ( normCV ` U ) ` ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) ) <_ y -> ( ( normCV ` W ) ` ( T ` ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) ) ) <_ 1 ) ) )
101 90 100 mpid 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( A. x e. X ( ( ( normCV ` U ) ` ( x ( -v ` U ) P ) ) <_ y -> ( ( normCV ` W ) ` ( T ` ( x ( -v ` U ) P ) ) ) <_ 1 ) -> ( ( normCV ` W ) ` ( T ` ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) ) ) <_ 1 ) )
102 29 ffvelcdmi 
 |-  ( z e. X -> ( T ` z ) e. ( BaseSet ` W ) )
103 13 33 nvcl 
 |-  ( ( W e. NrmCVec /\ ( T ` z ) e. ( BaseSet ` W ) ) -> ( ( normCV ` W ) ` ( T ` z ) ) e. RR )
104 8 102 103 sylancr 
 |-  ( z e. X -> ( ( normCV ` W ) ` ( T ` z ) ) e. RR )
105 104 ad2antrl 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( ( normCV ` W ) ` ( T ` z ) ) e. RR )
106 1red 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> 1 e. RR )
107 105 106 63 lemuldiv2d 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( ( ( y / ( ( normCV ` U ) ` z ) ) x. ( ( normCV ` W ) ` ( T ` z ) ) ) <_ 1 <-> ( ( normCV ` W ) ` ( T ` z ) ) <_ ( 1 / ( y / ( ( normCV ` U ) ` z ) ) ) ) )
108 71 fveq2d 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( T ` ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) ) = ( T ` ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) )
109 eqid 
 |-  ( .sOLD ` W ) = ( .sOLD ` W )
110 10 66 109 5 lnomul 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( ( y / ( ( normCV ` U ) ` z ) ) e. CC /\ z e. X ) ) -> ( T ` ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) = ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` W ) ( T ` z ) ) )
111 37 110 mpan 
 |-  ( ( ( y / ( ( normCV ` U ) ` z ) ) e. CC /\ z e. X ) -> ( T ` ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) = ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` W ) ( T ` z ) ) )
112 64 65 111 syl2anc 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( T ` ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) = ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` W ) ( T ` z ) ) )
113 108 112 eqtrd 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( T ` ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) ) = ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` W ) ( T ` z ) ) )
114 113 fveq2d 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( ( normCV ` W ) ` ( T ` ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) ) ) = ( ( normCV ` W ) ` ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` W ) ( T ` z ) ) ) )
115 8 a1i 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> W e. NrmCVec )
116 102 ad2antrl 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( T ` z ) e. ( BaseSet ` W ) )
117 13 109 33 nvsge0 
 |-  ( ( W e. NrmCVec /\ ( ( y / ( ( normCV ` U ) ` z ) ) e. RR /\ 0 <_ ( y / ( ( normCV ` U ) ` z ) ) ) /\ ( T ` z ) e. ( BaseSet ` W ) ) -> ( ( normCV ` W ) ` ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` W ) ( T ` z ) ) ) = ( ( y / ( ( normCV ` U ) ` z ) ) x. ( ( normCV ` W ) ` ( T ` z ) ) ) )
118 115 73 116 117 syl3anc 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( ( normCV ` W ) ` ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` W ) ( T ` z ) ) ) = ( ( y / ( ( normCV ` U ) ` z ) ) x. ( ( normCV ` W ) ` ( T ` z ) ) ) )
119 114 118 eqtrd 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( ( normCV ` W ) ` ( T ` ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) ) ) = ( ( y / ( ( normCV ` U ) ` z ) ) x. ( ( normCV ` W ) ` ( T ` z ) ) ) )
120 119 breq1d 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( ( ( normCV ` W ) ` ( T ` ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) ) ) <_ 1 <-> ( ( y / ( ( normCV ` U ) ` z ) ) x. ( ( normCV ` W ) ` ( T ` z ) ) ) <_ 1 ) )
121 rpcnne0 
 |-  ( y e. RR+ -> ( y e. CC /\ y =/= 0 ) )
122 rpcnne0 
 |-  ( ( ( normCV ` U ) ` z ) e. RR+ -> ( ( ( normCV ` U ) ` z ) e. CC /\ ( ( normCV ` U ) ` z ) =/= 0 ) )
123 recdiv 
 |-  ( ( ( y e. CC /\ y =/= 0 ) /\ ( ( ( normCV ` U ) ` z ) e. CC /\ ( ( normCV ` U ) ` z ) =/= 0 ) ) -> ( 1 / ( y / ( ( normCV ` U ) ` z ) ) ) = ( ( ( normCV ` U ) ` z ) / y ) )
124 121 122 123 syl2an 
 |-  ( ( y e. RR+ /\ ( ( normCV ` U ) ` z ) e. RR+ ) -> ( 1 / ( y / ( ( normCV ` U ) ` z ) ) ) = ( ( ( normCV ` U ) ` z ) / y ) )
125 53 61 124 syl2an 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( 1 / ( y / ( ( normCV ` U ) ` z ) ) ) = ( ( ( normCV ` U ) ` z ) / y ) )
126 rpne0 
 |-  ( y e. RR+ -> y =/= 0 )
127 126 ad2antlr 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> y =/= 0 )
128 79 77 127 divrec2d 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( ( ( normCV ` U ) ` z ) / y ) = ( ( 1 / y ) x. ( ( normCV ` U ) ` z ) ) )
129 125 128 eqtr2d 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( ( 1 / y ) x. ( ( normCV ` U ) ` z ) ) = ( 1 / ( y / ( ( normCV ` U ) ` z ) ) ) )
130 129 breq2d 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( ( ( normCV ` W ) ` ( T ` z ) ) <_ ( ( 1 / y ) x. ( ( normCV ` U ) ` z ) ) <-> ( ( normCV ` W ) ` ( T ` z ) ) <_ ( 1 / ( y / ( ( normCV ` U ) ` z ) ) ) ) )
131 107 120 130 3bitr4d 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( ( ( normCV ` W ) ` ( T ` ( ( P ( +v ` U ) ( ( y / ( ( normCV ` U ) ` z ) ) ( .sOLD ` U ) z ) ) ( -v ` U ) P ) ) ) <_ 1 <-> ( ( normCV ` W ) ` ( T ` z ) ) <_ ( ( 1 / y ) x. ( ( normCV ` U ) ` z ) ) ) )
132 101 131 sylibd 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ ( z e. X /\ z =/= ( 0vec ` U ) ) ) -> ( A. x e. X ( ( ( normCV ` U ) ` ( x ( -v ` U ) P ) ) <_ y -> ( ( normCV ` W ) ` ( T ` ( x ( -v ` U ) P ) ) ) <_ 1 ) -> ( ( normCV ` W ) ` ( T ` z ) ) <_ ( ( 1 / y ) x. ( ( normCV ` U ) ` z ) ) ) )
133 132 anassrs 
 |-  ( ( ( ( P e. X /\ y e. RR+ ) /\ z e. X ) /\ z =/= ( 0vec ` U ) ) -> ( A. x e. X ( ( ( normCV ` U ) ` ( x ( -v ` U ) P ) ) <_ y -> ( ( normCV ` W ) ` ( T ` ( x ( -v ` U ) P ) ) ) <_ 1 ) -> ( ( normCV ` W ) ` ( T ` z ) ) <_ ( ( 1 / y ) x. ( ( normCV ` U ) ` z ) ) ) )
134 133 imp 
 |-  ( ( ( ( ( P e. X /\ y e. RR+ ) /\ z e. X ) /\ z =/= ( 0vec ` U ) ) /\ A. x e. X ( ( ( normCV ` U ) ` ( x ( -v ` U ) P ) ) <_ y -> ( ( normCV ` W ) ` ( T ` ( x ( -v ` U ) P ) ) ) <_ 1 ) ) -> ( ( normCV ` W ) ` ( T ` z ) ) <_ ( ( 1 / y ) x. ( ( normCV ` U ) ` z ) ) )
135 134 an32s 
 |-  ( ( ( ( ( P e. X /\ y e. RR+ ) /\ z e. X ) /\ A. x e. X ( ( ( normCV ` U ) ` ( x ( -v ` U ) P ) ) <_ y -> ( ( normCV ` W ) ` ( T ` ( x ( -v ` U ) P ) ) ) <_ 1 ) ) /\ z =/= ( 0vec ` U ) ) -> ( ( normCV ` W ) ` ( T ` z ) ) <_ ( ( 1 / y ) x. ( ( normCV ` U ) ` z ) ) )
136 eqid 
 |-  ( 0vec ` W ) = ( 0vec ` W )
137 10 13 57 136 5 lno0 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( T ` ( 0vec ` U ) ) = ( 0vec ` W ) )
138 7 8 9 137 mp3an 
 |-  ( T ` ( 0vec ` U ) ) = ( 0vec ` W )
139 138 fveq2i 
 |-  ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) = ( ( normCV ` W ) ` ( 0vec ` W ) )
140 136 33 nvz0 
 |-  ( W e. NrmCVec -> ( ( normCV ` W ) ` ( 0vec ` W ) ) = 0 )
141 8 140 ax-mp 
 |-  ( ( normCV ` W ) ` ( 0vec ` W ) ) = 0
142 139 141 eqtri 
 |-  ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) = 0
143 0le0 
 |-  0 <_ 0
144 142 143 eqbrtri 
 |-  ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) <_ 0
145 20 rpcnd 
 |-  ( y e. RR+ -> ( 1 / y ) e. CC )
146 57 24 nvz0 
 |-  ( U e. NrmCVec -> ( ( normCV ` U ) ` ( 0vec ` U ) ) = 0 )
147 7 146 ax-mp 
 |-  ( ( normCV ` U ) ` ( 0vec ` U ) ) = 0
148 147 oveq2i 
 |-  ( ( 1 / y ) x. ( ( normCV ` U ) ` ( 0vec ` U ) ) ) = ( ( 1 / y ) x. 0 )
149 mul01 
 |-  ( ( 1 / y ) e. CC -> ( ( 1 / y ) x. 0 ) = 0 )
150 148 149 eqtrid 
 |-  ( ( 1 / y ) e. CC -> ( ( 1 / y ) x. ( ( normCV ` U ) ` ( 0vec ` U ) ) ) = 0 )
151 145 150 syl 
 |-  ( y e. RR+ -> ( ( 1 / y ) x. ( ( normCV ` U ) ` ( 0vec ` U ) ) ) = 0 )
152 144 151 breqtrrid 
 |-  ( y e. RR+ -> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) <_ ( ( 1 / y ) x. ( ( normCV ` U ) ` ( 0vec ` U ) ) ) )
153 152 ad3antlr 
 |-  ( ( ( ( P e. X /\ y e. RR+ ) /\ z e. X ) /\ A. x e. X ( ( ( normCV ` U ) ` ( x ( -v ` U ) P ) ) <_ y -> ( ( normCV ` W ) ` ( T ` ( x ( -v ` U ) P ) ) ) <_ 1 ) ) -> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) <_ ( ( 1 / y ) x. ( ( normCV ` U ) ` ( 0vec ` U ) ) ) )
154 50 135 153 pm2.61ne 
 |-  ( ( ( ( P e. X /\ y e. RR+ ) /\ z e. X ) /\ A. x e. X ( ( ( normCV ` U ) ` ( x ( -v ` U ) P ) ) <_ y -> ( ( normCV ` W ) ` ( T ` ( x ( -v ` U ) P ) ) ) <_ 1 ) ) -> ( ( normCV ` W ) ` ( T ` z ) ) <_ ( ( 1 / y ) x. ( ( normCV ` U ) ` z ) ) )
155 154 ex 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ z e. X ) -> ( A. x e. X ( ( ( normCV ` U ) ` ( x ( -v ` U ) P ) ) <_ y -> ( ( normCV ` W ) ` ( T ` ( x ( -v ` U ) P ) ) ) <_ 1 ) -> ( ( normCV ` W ) ` ( T ` z ) ) <_ ( ( 1 / y ) x. ( ( normCV ` U ) ` z ) ) ) )
156 155 ralrimdva 
 |-  ( ( P e. X /\ y e. RR+ ) -> ( A. x e. X ( ( ( normCV ` U ) ` ( x ( -v ` U ) P ) ) <_ y -> ( ( normCV ` W ) ` ( T ` ( x ( -v ` U ) P ) ) ) <_ 1 ) -> A. z e. X ( ( normCV ` W ) ` ( T ` z ) ) <_ ( ( 1 / y ) x. ( ( normCV ` U ) ` z ) ) ) )
157 46 156 sylbid 
 |-  ( ( P e. X /\ y e. RR+ ) -> ( A. x e. X ( ( x C P ) <_ y -> ( ( T ` x ) D ( T ` P ) ) <_ 1 ) -> A. z e. X ( ( normCV ` W ) ` ( T ` z ) ) <_ ( ( 1 / y ) x. ( ( normCV ` U ) ` z ) ) ) )
158 157 imp 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ A. x e. X ( ( x C P ) <_ y -> ( ( T ` x ) D ( T ` P ) ) <_ 1 ) ) -> A. z e. X ( ( normCV ` W ) ` ( T ` z ) ) <_ ( ( 1 / y ) x. ( ( normCV ` U ) ` z ) ) )
159 oveq1 
 |-  ( x = ( 1 / y ) -> ( x x. ( ( normCV ` U ) ` z ) ) = ( ( 1 / y ) x. ( ( normCV ` U ) ` z ) ) )
160 159 breq2d 
 |-  ( x = ( 1 / y ) -> ( ( ( normCV ` W ) ` ( T ` z ) ) <_ ( x x. ( ( normCV ` U ) ` z ) ) <-> ( ( normCV ` W ) ` ( T ` z ) ) <_ ( ( 1 / y ) x. ( ( normCV ` U ) ` z ) ) ) )
161 160 ralbidv 
 |-  ( x = ( 1 / y ) -> ( A. z e. X ( ( normCV ` W ) ` ( T ` z ) ) <_ ( x x. ( ( normCV ` U ) ` z ) ) <-> A. z e. X ( ( normCV ` W ) ` ( T ` z ) ) <_ ( ( 1 / y ) x. ( ( normCV ` U ) ` z ) ) ) )
162 161 rspcev 
 |-  ( ( ( 1 / y ) e. RR /\ A. z e. X ( ( normCV ` W ) ` ( T ` z ) ) <_ ( ( 1 / y ) x. ( ( normCV ` U ) ` z ) ) ) -> E. x e. RR A. z e. X ( ( normCV ` W ) ` ( T ` z ) ) <_ ( x x. ( ( normCV ` U ) ` z ) ) )
163 22 158 162 syl2anc 
 |-  ( ( ( P e. X /\ y e. RR+ ) /\ A. x e. X ( ( x C P ) <_ y -> ( ( T ` x ) D ( T ` P ) ) <_ 1 ) ) -> E. x e. RR A. z e. X ( ( normCV ` W ) ` ( T ` z ) ) <_ ( x x. ( ( normCV ` U ) ` z ) ) )
164 163 rexlimdva2 
 |-  ( P e. X -> ( E. y e. RR+ A. x e. X ( ( x C P ) <_ y -> ( ( T ` x ) D ( T ` P ) ) <_ 1 ) -> E. x e. RR A. z e. X ( ( normCV ` W ) ` ( T ` z ) ) <_ ( x x. ( ( normCV ` U ) ` z ) ) ) )
165 19 164 syl5 
 |-  ( P e. X -> ( T e. ( ( J CnP K ) ` P ) -> E. x e. RR A. z e. X ( ( normCV ` W ) ` ( T ` z ) ) <_ ( x x. ( ( normCV ` U ) ` z ) ) ) )
166 165 imp 
 |-  ( ( P e. X /\ T e. ( ( J CnP K ) ` P ) ) -> E. x e. RR A. z e. X ( ( normCV ` W ) ` ( T ` z ) ) <_ ( x x. ( ( normCV ` U ) ` z ) ) )
167 10 24 33 5 6 7 8 isblo3i 
 |-  ( T e. B <-> ( T e. L /\ E. x e. RR A. z e. X ( ( normCV ` W ) ` ( T ` z ) ) <_ ( x x. ( ( normCV ` U ) ` z ) ) ) )
168 9 167 mpbiran 
 |-  ( T e. B <-> E. x e. RR A. z e. X ( ( normCV ` W ) ` ( T ` z ) ) <_ ( x x. ( ( normCV ` U ) ` z ) ) )
169 166 168 sylibr 
 |-  ( ( P e. X /\ T e. ( ( J CnP K ) ` P ) ) -> T e. B )