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 ⊢ 𝐶 = ( 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 ffvelcdmi ⊢ ( 𝑥 ∈ 𝑋 → ( 𝑇 ‘ 𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) )
31 29 ffvelcdmi ⊢ ( 𝑃 ∈ 𝑋 → ( 𝑇 ‘ 𝑃 ) ∈ ( 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 ffvelcdmi ⊢ ( 𝑧 ∈ 𝑋 → ( 𝑇 ‘ 𝑧 ) ∈ ( 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 𝐾 ) ‘ 𝑃 ) ) → 𝑇 ∈ 𝐵 )