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 𝐶 = ( IndMet ‘ 𝑈 )
blocni.d 𝐷 = ( IndMet ‘ 𝑊 )
blocni.j 𝐽 = ( MetOpen ‘ 𝐶 )
blocni.k 𝐾 = ( MetOpen ‘ 𝐷 )
blocni.4 𝐿 = ( 𝑈 LnOp 𝑊 )
blocni.5 𝐵 = ( 𝑈 BLnOp 𝑊 )
blocni.u 𝑈 ∈ NrmCVec
blocni.w 𝑊 ∈ NrmCVec
blocni.l 𝑇𝐿
blocnilem.1 𝑋 = ( BaseSet ‘ 𝑈 )
Assertion blocnilem ( ( 𝑃𝑋𝑇 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝑇𝐵 )

Proof

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