MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  blocnilem Structured version   Visualization version   GIF version

Theorem blocnilem 28136
Description: Lemma for blocni 28137 and lnocni 28138. 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.)
Hypotheses
Ref Expression
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
Ref Expression
blocnilem ((𝑃𝑋𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑇𝐵)

Proof of Theorem blocnilem
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 blocni.u . . . . . 6 𝑈 ∈ NrmCVec
2 blocnilem.1 . . . . . . 7 𝑋 = (BaseSet‘𝑈)
3 blocni.8 . . . . . . 7 𝐶 = (IndMet‘𝑈)
42, 3imsxmet 28024 . . . . . 6 (𝑈 ∈ NrmCVec → 𝐶 ∈ (∞Met‘𝑋))
51, 4ax-mp 5 . . . . 5 𝐶 ∈ (∞Met‘𝑋)
6 blocni.w . . . . . 6 𝑊 ∈ NrmCVec
7 eqid 2765 . . . . . . 7 (BaseSet‘𝑊) = (BaseSet‘𝑊)
8 blocni.d . . . . . . 7 𝐷 = (IndMet‘𝑊)
97, 8imsxmet 28024 . . . . . 6 (𝑊 ∈ NrmCVec → 𝐷 ∈ (∞Met‘(BaseSet‘𝑊)))
106, 9ax-mp 5 . . . . 5 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))
11 1rp 12037 . . . . . 6 1 ∈ ℝ+
12 blocni.j . . . . . . 7 𝐽 = (MetOpen‘𝐶)
13 blocni.k . . . . . . 7 𝐾 = (MetOpen‘𝐷)
1412, 13metcnpi3 22644 . . . . . 6 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))) ∧ (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 1 ∈ ℝ+)) → ∃𝑦 ∈ ℝ+𝑥𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1))
1511, 14mpanr2 695 . . . . 5 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))) ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∃𝑦 ∈ ℝ+𝑥𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1))
165, 10, 15mpanl12 693 . . . 4 (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) → ∃𝑦 ∈ ℝ+𝑥𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1))
17 rpreccl 12060 . . . . . . . . 9 (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℝ+)
1817rpred 12075 . . . . . . . 8 (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℝ)
1918ad2antlr 718 . . . . . . 7 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ ∀𝑥𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1)) → (1 / 𝑦) ∈ ℝ)
20 eqid 2765 . . . . . . . . . . . . . . . 16 ( −𝑣𝑈) = ( −𝑣𝑈)
21 eqid 2765 . . . . . . . . . . . . . . . 16 (normCV𝑈) = (normCV𝑈)
222, 20, 21, 3imsdval 28018 . . . . . . . . . . . . . . 15 ((𝑈 ∈ NrmCVec ∧ 𝑥𝑋𝑃𝑋) → (𝑥𝐶𝑃) = ((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)))
231, 22mp3an1 1572 . . . . . . . . . . . . . 14 ((𝑥𝑋𝑃𝑋) → (𝑥𝐶𝑃) = ((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)))
2423breq1d 4821 . . . . . . . . . . . . 13 ((𝑥𝑋𝑃𝑋) → ((𝑥𝐶𝑃) ≤ 𝑦 ↔ ((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦))
25 blocni.l . . . . . . . . . . . . . . . . . 18 𝑇𝐿
26 blocni.4 . . . . . . . . . . . . . . . . . . 19 𝐿 = (𝑈 LnOp 𝑊)
272, 7, 26lnof 28087 . . . . . . . . . . . . . . . . . 18 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇𝐿) → 𝑇:𝑋⟶(BaseSet‘𝑊))
281, 6, 25, 27mp3an 1585 . . . . . . . . . . . . . . . . 17 𝑇:𝑋⟶(BaseSet‘𝑊)
2928ffvelrni 6552 . . . . . . . . . . . . . . . 16 (𝑥𝑋 → (𝑇𝑥) ∈ (BaseSet‘𝑊))
3028ffvelrni 6552 . . . . . . . . . . . . . . . 16 (𝑃𝑋 → (𝑇𝑃) ∈ (BaseSet‘𝑊))
31 eqid 2765 . . . . . . . . . . . . . . . . . 18 ( −𝑣𝑊) = ( −𝑣𝑊)
32 eqid 2765 . . . . . . . . . . . . . . . . . 18 (normCV𝑊) = (normCV𝑊)
337, 31, 32, 8imsdval 28018 . . . . . . . . . . . . . . . . 17 ((𝑊 ∈ NrmCVec ∧ (𝑇𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇𝑥)𝐷(𝑇𝑃)) = ((normCV𝑊)‘((𝑇𝑥)( −𝑣𝑊)(𝑇𝑃))))
346, 33mp3an1 1572 . . . . . . . . . . . . . . . 16 (((𝑇𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇𝑥)𝐷(𝑇𝑃)) = ((normCV𝑊)‘((𝑇𝑥)( −𝑣𝑊)(𝑇𝑃))))
3529, 30, 34syl2an 589 . . . . . . . . . . . . . . 15 ((𝑥𝑋𝑃𝑋) → ((𝑇𝑥)𝐷(𝑇𝑃)) = ((normCV𝑊)‘((𝑇𝑥)( −𝑣𝑊)(𝑇𝑃))))
361, 6, 253pm3.2i 1438 . . . . . . . . . . . . . . . . 17 (𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇𝐿)
372, 20, 31, 26lnosub 28091 . . . . . . . . . . . . . . . . 17 (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇𝐿) ∧ (𝑥𝑋𝑃𝑋)) → (𝑇‘(𝑥( −𝑣𝑈)𝑃)) = ((𝑇𝑥)( −𝑣𝑊)(𝑇𝑃)))
3836, 37mpan 681 . . . . . . . . . . . . . . . 16 ((𝑥𝑋𝑃𝑋) → (𝑇‘(𝑥( −𝑣𝑈)𝑃)) = ((𝑇𝑥)( −𝑣𝑊)(𝑇𝑃)))
3938fveq2d 6383 . . . . . . . . . . . . . . 15 ((𝑥𝑋𝑃𝑋) → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) = ((normCV𝑊)‘((𝑇𝑥)( −𝑣𝑊)(𝑇𝑃))))
4035, 39eqtr4d 2802 . . . . . . . . . . . . . 14 ((𝑥𝑋𝑃𝑋) → ((𝑇𝑥)𝐷(𝑇𝑃)) = ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))))
4140breq1d 4821 . . . . . . . . . . . . 13 ((𝑥𝑋𝑃𝑋) → (((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1 ↔ ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1))
4224, 41imbi12d 335 . . . . . . . . . . . 12 ((𝑥𝑋𝑃𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1) ↔ (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1)))
4342ancoms 450 . . . . . . . . . . 11 ((𝑃𝑋𝑥𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1) ↔ (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1)))
4443adantlr 706 . . . . . . . . . 10 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ 𝑥𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1) ↔ (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1)))
4544ralbidva 3132 . . . . . . . . 9 ((𝑃𝑋𝑦 ∈ ℝ+) → (∀𝑥𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1) ↔ ∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1)))
46 2fveq3 6384 . . . . . . . . . . . . 13 (𝑧 = (0vec𝑈) → ((normCV𝑊)‘(𝑇𝑧)) = ((normCV𝑊)‘(𝑇‘(0vec𝑈))))
47 fveq2 6379 . . . . . . . . . . . . . 14 (𝑧 = (0vec𝑈) → ((normCV𝑈)‘𝑧) = ((normCV𝑈)‘(0vec𝑈)))
4847oveq2d 6862 . . . . . . . . . . . . 13 (𝑧 = (0vec𝑈) → ((1 / 𝑦) · ((normCV𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV𝑈)‘(0vec𝑈))))
4946, 48breq12d 4824 . . . . . . . . . . . 12 (𝑧 = (0vec𝑈) → (((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧)) ↔ ((normCV𝑊)‘(𝑇‘(0vec𝑈))) ≤ ((1 / 𝑦) · ((normCV𝑈)‘(0vec𝑈)))))
501a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → 𝑈 ∈ NrmCVec)
51 simpll 783 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → 𝑃𝑋)
52 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑃𝑋𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
532, 21nvcl 27993 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑈 ∈ NrmCVec ∧ 𝑧𝑋) → ((normCV𝑈)‘𝑧) ∈ ℝ)
541, 53mpan 681 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧𝑋 → ((normCV𝑈)‘𝑧) ∈ ℝ)
5554adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑧𝑋𝑧 ≠ (0vec𝑈)) → ((normCV𝑈)‘𝑧) ∈ ℝ)
56 eqid 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (0vec𝑈) = (0vec𝑈)
572, 56, 21nvgt0 28006 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑈 ∈ NrmCVec ∧ 𝑧𝑋) → (𝑧 ≠ (0vec𝑈) ↔ 0 < ((normCV𝑈)‘𝑧)))
581, 57mpan 681 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧𝑋 → (𝑧 ≠ (0vec𝑈) ↔ 0 < ((normCV𝑈)‘𝑧)))
5958biimpa 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑧𝑋𝑧 ≠ (0vec𝑈)) → 0 < ((normCV𝑈)‘𝑧))
6055, 59elrpd 12072 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧𝑋𝑧 ≠ (0vec𝑈)) → ((normCV𝑈)‘𝑧) ∈ ℝ+)
61 rpdivcl 12059 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ ℝ+ ∧ ((normCV𝑈)‘𝑧) ∈ ℝ+) → (𝑦 / ((normCV𝑈)‘𝑧)) ∈ ℝ+)
6252, 60, 61syl2an 589 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (𝑦 / ((normCV𝑈)‘𝑧)) ∈ ℝ+)
6362rpcnd 12077 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (𝑦 / ((normCV𝑈)‘𝑧)) ∈ ℂ)
64 simprl 787 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → 𝑧𝑋)
65 eqid 2765 . . . . . . . . . . . . . . . . . . . . . . 23 ( ·𝑠OLD𝑈) = ( ·𝑠OLD𝑈)
662, 65nvscl 27958 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑈 ∈ NrmCVec ∧ (𝑦 / ((normCV𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧𝑋) → ((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧) ∈ 𝑋)
6750, 63, 64, 66syl3anc 1490 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧) ∈ 𝑋)
68 eqid 2765 . . . . . . . . . . . . . . . . . . . . . 22 ( +𝑣𝑈) = ( +𝑣𝑈)
692, 68, 20nvpncan2 27985 . . . . . . . . . . . . . . . . . . . . 21 ((𝑈 ∈ NrmCVec ∧ 𝑃𝑋 ∧ ((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧) ∈ 𝑋) → ((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃) = ((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))
7050, 51, 67, 69syl3anc 1490 . . . . . . . . . . . . . . . . . . . 20 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃) = ((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))
7170fveq2d 6383 . . . . . . . . . . . . . . . . . . 19 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑈)‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)) = ((normCV𝑈)‘((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)))
7262rprege0d 12082 . . . . . . . . . . . . . . . . . . . 20 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((𝑦 / ((normCV𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 / ((normCV𝑈)‘𝑧))))
732, 65, 21nvsge0 27996 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∈ NrmCVec ∧ ((𝑦 / ((normCV𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 / ((normCV𝑈)‘𝑧))) ∧ 𝑧𝑋) → ((normCV𝑈)‘((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) = ((𝑦 / ((normCV𝑈)‘𝑧)) · ((normCV𝑈)‘𝑧)))
7450, 72, 64, 73syl3anc 1490 . . . . . . . . . . . . . . . . . . 19 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑈)‘((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) = ((𝑦 / ((normCV𝑈)‘𝑧)) · ((normCV𝑈)‘𝑧)))
75 rpcn 12045 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℝ+𝑦 ∈ ℂ)
7675ad2antlr 718 . . . . . . . . . . . . . . . . . . . 20 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → 𝑦 ∈ ℂ)
7754ad2antrl 719 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑈)‘𝑧) ∈ ℝ)
7877recnd 10326 . . . . . . . . . . . . . . . . . . . 20 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑈)‘𝑧) ∈ ℂ)
792, 56, 21nvz 28001 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑈 ∈ NrmCVec ∧ 𝑧𝑋) → (((normCV𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec𝑈)))
801, 79mpan 681 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝑋 → (((normCV𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec𝑈)))
8180necon3bid 2981 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑋 → (((normCV𝑈)‘𝑧) ≠ 0 ↔ 𝑧 ≠ (0vec𝑈)))
8281biimpar 469 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧𝑋𝑧 ≠ (0vec𝑈)) → ((normCV𝑈)‘𝑧) ≠ 0)
8382adantl 473 . . . . . . . . . . . . . . . . . . . 20 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑈)‘𝑧) ≠ 0)
8476, 78, 83divcan1d 11060 . . . . . . . . . . . . . . . . . . 19 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((𝑦 / ((normCV𝑈)‘𝑧)) · ((normCV𝑈)‘𝑧)) = 𝑦)
8571, 74, 843eqtrd 2803 . . . . . . . . . . . . . . . . . 18 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑈)‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)) = 𝑦)
86 rpre 12041 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
8786leidd 10852 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ+𝑦𝑦)
8887ad2antlr 718 . . . . . . . . . . . . . . . . . 18 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → 𝑦𝑦)
8985, 88eqbrtrd 4833 . . . . . . . . . . . . . . . . 17 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑈)‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)) ≤ 𝑦)
902, 68nvgcl 27952 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ NrmCVec ∧ 𝑃𝑋 ∧ ((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧) ∈ 𝑋) → (𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) ∈ 𝑋)
9150, 51, 67, 90syl3anc 1490 . . . . . . . . . . . . . . . . . 18 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) ∈ 𝑋)
92 fvoveq1 6869 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = (𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) → ((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) = ((normCV𝑈)‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)))
9392breq1d 4821 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) → (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 ↔ ((normCV𝑈)‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)) ≤ 𝑦))
94 fvoveq1 6869 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) → (𝑇‘(𝑥( −𝑣𝑈)𝑃)) = (𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)))
9594fveq2d 6383 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = (𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) = ((normCV𝑊)‘(𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃))))
9695breq1d 4821 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) → (((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1 ↔ ((normCV𝑊)‘(𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃))) ≤ 1))
9793, 96imbi12d 335 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) → ((((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1) ↔ (((normCV𝑈)‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃))) ≤ 1)))
9897rspcv 3458 . . . . . . . . . . . . . . . . . 18 ((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) ∈ 𝑋 → (∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1) → (((normCV𝑈)‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃))) ≤ 1)))
9991, 98syl 17 . . . . . . . . . . . . . . . . 17 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1) → (((normCV𝑈)‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃))) ≤ 1)))
10089, 99mpid 44 . . . . . . . . . . . . . . . 16 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1) → ((normCV𝑊)‘(𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃))) ≤ 1))
10128ffvelrni 6552 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝑋 → (𝑇𝑧) ∈ (BaseSet‘𝑊))
1027, 32nvcl 27993 . . . . . . . . . . . . . . . . . . . 20 ((𝑊 ∈ NrmCVec ∧ (𝑇𝑧) ∈ (BaseSet‘𝑊)) → ((normCV𝑊)‘(𝑇𝑧)) ∈ ℝ)
1036, 101, 102sylancr 581 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑋 → ((normCV𝑊)‘(𝑇𝑧)) ∈ ℝ)
104103ad2antrl 719 . . . . . . . . . . . . . . . . . 18 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑊)‘(𝑇𝑧)) ∈ ℝ)
105 1red 10298 . . . . . . . . . . . . . . . . . 18 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → 1 ∈ ℝ)
106104, 105, 62lemuldiv2d 12125 . . . . . . . . . . . . . . . . 17 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (((𝑦 / ((normCV𝑈)‘𝑧)) · ((normCV𝑊)‘(𝑇𝑧))) ≤ 1 ↔ ((normCV𝑊)‘(𝑇𝑧)) ≤ (1 / (𝑦 / ((normCV𝑈)‘𝑧)))))
10770fveq2d 6383 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)) = (𝑇‘((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)))
108 eqid 2765 . . . . . . . . . . . . . . . . . . . . . . . 24 ( ·𝑠OLD𝑊) = ( ·𝑠OLD𝑊)
1092, 65, 108, 26lnomul 28092 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇𝐿) ∧ ((𝑦 / ((normCV𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧𝑋)) → (𝑇‘((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) = ((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑊)(𝑇𝑧)))
11036, 109mpan 681 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦 / ((normCV𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧𝑋) → (𝑇‘((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) = ((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑊)(𝑇𝑧)))
11163, 64, 110syl2anc 579 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (𝑇‘((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) = ((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑊)(𝑇𝑧)))
112107, 111eqtrd 2799 . . . . . . . . . . . . . . . . . . . 20 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)) = ((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑊)(𝑇𝑧)))
113112fveq2d 6383 . . . . . . . . . . . . . . . . . . 19 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑊)‘(𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃))) = ((normCV𝑊)‘((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑊)(𝑇𝑧))))
1146a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → 𝑊 ∈ NrmCVec)
115101ad2antrl 719 . . . . . . . . . . . . . . . . . . . 20 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (𝑇𝑧) ∈ (BaseSet‘𝑊))
1167, 108, 32nvsge0 27996 . . . . . . . . . . . . . . . . . . . 20 ((𝑊 ∈ NrmCVec ∧ ((𝑦 / ((normCV𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 / ((normCV𝑈)‘𝑧))) ∧ (𝑇𝑧) ∈ (BaseSet‘𝑊)) → ((normCV𝑊)‘((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑊)(𝑇𝑧))) = ((𝑦 / ((normCV𝑈)‘𝑧)) · ((normCV𝑊)‘(𝑇𝑧))))
117114, 72, 115, 116syl3anc 1490 . . . . . . . . . . . . . . . . . . 19 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑊)‘((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑊)(𝑇𝑧))) = ((𝑦 / ((normCV𝑈)‘𝑧)) · ((normCV𝑊)‘(𝑇𝑧))))
118113, 117eqtrd 2799 . . . . . . . . . . . . . . . . . 18 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑊)‘(𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃))) = ((𝑦 / ((normCV𝑈)‘𝑧)) · ((normCV𝑊)‘(𝑇𝑧))))
119118breq1d 4821 . . . . . . . . . . . . . . . . 17 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (((normCV𝑊)‘(𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃))) ≤ 1 ↔ ((𝑦 / ((normCV𝑈)‘𝑧)) · ((normCV𝑊)‘(𝑇𝑧))) ≤ 1))
120 rpcnne0 12053 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℝ+ → (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0))
121 rpcnne0 12053 . . . . . . . . . . . . . . . . . . . . 21 (((normCV𝑈)‘𝑧) ∈ ℝ+ → (((normCV𝑈)‘𝑧) ∈ ℂ ∧ ((normCV𝑈)‘𝑧) ≠ 0))
122 recdiv 10989 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) ∧ (((normCV𝑈)‘𝑧) ∈ ℂ ∧ ((normCV𝑈)‘𝑧) ≠ 0)) → (1 / (𝑦 / ((normCV𝑈)‘𝑧))) = (((normCV𝑈)‘𝑧) / 𝑦))
123120, 121, 122syl2an 589 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ ℝ+ ∧ ((normCV𝑈)‘𝑧) ∈ ℝ+) → (1 / (𝑦 / ((normCV𝑈)‘𝑧))) = (((normCV𝑈)‘𝑧) / 𝑦))
12452, 60, 123syl2an 589 . . . . . . . . . . . . . . . . . . 19 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (1 / (𝑦 / ((normCV𝑈)‘𝑧))) = (((normCV𝑈)‘𝑧) / 𝑦))
125 rpne0 12051 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℝ+𝑦 ≠ 0)
126125ad2antlr 718 . . . . . . . . . . . . . . . . . . . 20 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → 𝑦 ≠ 0)
12778, 76, 126divrec2d 11063 . . . . . . . . . . . . . . . . . . 19 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (((normCV𝑈)‘𝑧) / 𝑦) = ((1 / 𝑦) · ((normCV𝑈)‘𝑧)))
128124, 127eqtr2d 2800 . . . . . . . . . . . . . . . . . 18 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((1 / 𝑦) · ((normCV𝑈)‘𝑧)) = (1 / (𝑦 / ((normCV𝑈)‘𝑧))))
129128breq2d 4823 . . . . . . . . . . . . . . . . 17 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧)) ↔ ((normCV𝑊)‘(𝑇𝑧)) ≤ (1 / (𝑦 / ((normCV𝑈)‘𝑧)))))
130106, 119, 1293bitr4d 302 . . . . . . . . . . . . . . . 16 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (((normCV𝑊)‘(𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃))) ≤ 1 ↔ ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧))))
131100, 130sylibd 230 . . . . . . . . . . . . . . 15 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1) → ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧))))
132131anassrs 459 . . . . . . . . . . . . . 14 ((((𝑃𝑋𝑦 ∈ ℝ+) ∧ 𝑧𝑋) ∧ 𝑧 ≠ (0vec𝑈)) → (∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1) → ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧))))
133132imp 395 . . . . . . . . . . . . 13 (((((𝑃𝑋𝑦 ∈ ℝ+) ∧ 𝑧𝑋) ∧ 𝑧 ≠ (0vec𝑈)) ∧ ∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1)) → ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧)))
134133an32s 642 . . . . . . . . . . . 12 (((((𝑃𝑋𝑦 ∈ ℝ+) ∧ 𝑧𝑋) ∧ ∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1)) ∧ 𝑧 ≠ (0vec𝑈)) → ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧)))
135 eqid 2765 . . . . . . . . . . . . . . . . . . 19 (0vec𝑊) = (0vec𝑊)
1362, 7, 56, 135, 26lno0 28088 . . . . . . . . . . . . . . . . . 18 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇𝐿) → (𝑇‘(0vec𝑈)) = (0vec𝑊))
1371, 6, 25, 136mp3an 1585 . . . . . . . . . . . . . . . . 17 (𝑇‘(0vec𝑈)) = (0vec𝑊)
138137fveq2i 6382 . . . . . . . . . . . . . . . 16 ((normCV𝑊)‘(𝑇‘(0vec𝑈))) = ((normCV𝑊)‘(0vec𝑊))
139135, 32nvz0 28000 . . . . . . . . . . . . . . . . 17 (𝑊 ∈ NrmCVec → ((normCV𝑊)‘(0vec𝑊)) = 0)
1406, 139ax-mp 5 . . . . . . . . . . . . . . . 16 ((normCV𝑊)‘(0vec𝑊)) = 0
141138, 140eqtri 2787 . . . . . . . . . . . . . . 15 ((normCV𝑊)‘(𝑇‘(0vec𝑈))) = 0
142 0le0 11384 . . . . . . . . . . . . . . 15 0 ≤ 0
143141, 142eqbrtri 4832 . . . . . . . . . . . . . 14 ((normCV𝑊)‘(𝑇‘(0vec𝑈))) ≤ 0
14417rpcnd 12077 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℂ)
14556, 21nvz0 28000 . . . . . . . . . . . . . . . . . 18 (𝑈 ∈ NrmCVec → ((normCV𝑈)‘(0vec𝑈)) = 0)
1461, 145ax-mp 5 . . . . . . . . . . . . . . . . 17 ((normCV𝑈)‘(0vec𝑈)) = 0
147146oveq2i 6857 . . . . . . . . . . . . . . . 16 ((1 / 𝑦) · ((normCV𝑈)‘(0vec𝑈))) = ((1 / 𝑦) · 0)
148 mul01 10473 . . . . . . . . . . . . . . . 16 ((1 / 𝑦) ∈ ℂ → ((1 / 𝑦) · 0) = 0)
149147, 148syl5eq 2811 . . . . . . . . . . . . . . 15 ((1 / 𝑦) ∈ ℂ → ((1 / 𝑦) · ((normCV𝑈)‘(0vec𝑈))) = 0)
150144, 149syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ+ → ((1 / 𝑦) · ((normCV𝑈)‘(0vec𝑈))) = 0)
151143, 150syl5breqr 4849 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ+ → ((normCV𝑊)‘(𝑇‘(0vec𝑈))) ≤ ((1 / 𝑦) · ((normCV𝑈)‘(0vec𝑈))))
152151ad3antlr 722 . . . . . . . . . . . 12 ((((𝑃𝑋𝑦 ∈ ℝ+) ∧ 𝑧𝑋) ∧ ∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1)) → ((normCV𝑊)‘(𝑇‘(0vec𝑈))) ≤ ((1 / 𝑦) · ((normCV𝑈)‘(0vec𝑈))))
15349, 134, 152pm2.61ne 3022 . . . . . . . . . . 11 ((((𝑃𝑋𝑦 ∈ ℝ+) ∧ 𝑧𝑋) ∧ ∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1)) → ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧)))
154153ex 401 . . . . . . . . . 10 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ 𝑧𝑋) → (∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1) → ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧))))
155154ralrimdva 3116 . . . . . . . . 9 ((𝑃𝑋𝑦 ∈ ℝ+) → (∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1) → ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧))))
15645, 155sylbid 231 . . . . . . . 8 ((𝑃𝑋𝑦 ∈ ℝ+) → (∀𝑥𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1) → ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧))))
157156imp 395 . . . . . . 7 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ ∀𝑥𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1)) → ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧)))
158 oveq1 6853 . . . . . . . . . 10 (𝑥 = (1 / 𝑦) → (𝑥 · ((normCV𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV𝑈)‘𝑧)))
159158breq2d 4823 . . . . . . . . 9 (𝑥 = (1 / 𝑦) → (((normCV𝑊)‘(𝑇𝑧)) ≤ (𝑥 · ((normCV𝑈)‘𝑧)) ↔ ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧))))
160159ralbidv 3133 . . . . . . . 8 (𝑥 = (1 / 𝑦) → (∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ (𝑥 · ((normCV𝑈)‘𝑧)) ↔ ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧))))
161160rspcev 3462 . . . . . . 7 (((1 / 𝑦) ∈ ℝ ∧ ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧))) → ∃𝑥 ∈ ℝ ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ (𝑥 · ((normCV𝑈)‘𝑧)))
16219, 157, 161syl2anc 579 . . . . . 6 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ ∀𝑥𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1)) → ∃𝑥 ∈ ℝ ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ (𝑥 · ((normCV𝑈)‘𝑧)))
163162ex 401 . . . . 5 ((𝑃𝑋𝑦 ∈ ℝ+) → (∀𝑥𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ (𝑥 · ((normCV𝑈)‘𝑧))))
164163rexlimdva 3178 . . . 4 (𝑃𝑋 → (∃𝑦 ∈ ℝ+𝑥𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ (𝑥 · ((normCV𝑈)‘𝑧))))
16516, 164syl5 34 . . 3 (𝑃𝑋 → (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) → ∃𝑥 ∈ ℝ ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ (𝑥 · ((normCV𝑈)‘𝑧))))
166165imp 395 . 2 ((𝑃𝑋𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∃𝑥 ∈ ℝ ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ (𝑥 · ((normCV𝑈)‘𝑧)))
167 blocni.5 . . . 4 𝐵 = (𝑈 BLnOp 𝑊)
1682, 21, 32, 26, 167, 1, 6isblo3i 28133 . . 3 (𝑇𝐵 ↔ (𝑇𝐿 ∧ ∃𝑥 ∈ ℝ ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ (𝑥 · ((normCV𝑈)‘𝑧))))
16925, 168mpbiran 700 . 2 (𝑇𝐵 ↔ ∃𝑥 ∈ ℝ ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ (𝑥 · ((normCV𝑈)‘𝑧)))
170166, 169sylibr 225 1 ((𝑃𝑋𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑇𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056   class class class wbr 4811  wf 6066  cfv 6070  (class class class)co 6846  cc 10191  cr 10192  0cc0 10193  1c1 10194   · cmul 10198   < clt 10332  cle 10333   / cdiv 10942  +crp 12033  ∞Metcxmet 20018  MetOpencmopn 20023   CnP ccnp 21323  NrmCVeccnv 27916   +𝑣 cpv 27917  BaseSetcba 27918   ·𝑠OLD cns 27919  0veccn0v 27920  𝑣 cnsb 27921  normCVcnmcv 27922  IndMetcims 27923   LnOp clno 28072   BLnOp cblo 28074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-cnex 10249  ax-resscn 10250  ax-1cn 10251  ax-icn 10252  ax-addcl 10253  ax-addrcl 10254  ax-mulcl 10255  ax-mulrcl 10256  ax-mulcom 10257  ax-addass 10258  ax-mulass 10259  ax-distr 10260  ax-i2m1 10261  ax-1ne0 10262  ax-1rid 10263  ax-rnegex 10264  ax-rrecex 10265  ax-cnre 10266  ax-pre-lttri 10267  ax-pre-lttrn 10268  ax-pre-ltadd 10269  ax-pre-mulgt0 10270  ax-pre-sup 10271  ax-addf 10272  ax-mulf 10273
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-om 7268  df-1st 7370  df-2nd 7371  df-wrecs 7614  df-recs 7676  df-rdg 7714  df-er 7951  df-map 8066  df-en 8165  df-dom 8166  df-sdom 8167  df-sup 8559  df-inf 8560  df-pnf 10334  df-mnf 10335  df-xr 10336  df-ltxr 10337  df-le 10338  df-sub 10526  df-neg 10527  df-div 10943  df-nn 11279  df-2 11339  df-3 11340  df-n0 11543  df-z 11629  df-uz 11892  df-q 11995  df-rp 12034  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-seq 13014  df-exp 13073  df-cj 14138  df-re 14139  df-im 14140  df-sqrt 14274  df-abs 14275  df-topgen 16384  df-psmet 20025  df-xmet 20026  df-met 20027  df-bl 20028  df-mopn 20029  df-top 20992  df-topon 21009  df-bases 21044  df-cnp 21326  df-grpo 27825  df-gid 27826  df-ginv 27827  df-gdiv 27828  df-ablo 27877  df-vc 27891  df-nv 27924  df-va 27927  df-ba 27928  df-sm 27929  df-0v 27930  df-vs 27931  df-nmcv 27932  df-ims 27933  df-lno 28076  df-nmoo 28077  df-blo 28078  df-0o 28079
This theorem is referenced by:  blocni  28137  lnocni  28138
  Copyright terms: Public domain W3C validator