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

Theorem blocnilem 30824
Description: Lemma for blocni 30825 and lnocni 30826. 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 30712 . . . . . 6 (𝑈 ∈ NrmCVec → 𝐶 ∈ (∞Met‘𝑋))
51, 4ax-mp 5 . . . . 5 𝐶 ∈ (∞Met‘𝑋)
6 blocni.w . . . . . 6 𝑊 ∈ NrmCVec
7 eqid 2736 . . . . . . 7 (BaseSet‘𝑊) = (BaseSet‘𝑊)
8 blocni.d . . . . . . 7 𝐷 = (IndMet‘𝑊)
97, 8imsxmet 30712 . . . . . 6 (𝑊 ∈ NrmCVec → 𝐷 ∈ (∞Met‘(BaseSet‘𝑊)))
106, 9ax-mp 5 . . . . 5 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))
11 1rp 13039 . . . . . 6 1 ∈ ℝ+
12 blocni.j . . . . . . 7 𝐽 = (MetOpen‘𝐶)
13 blocni.k . . . . . . 7 𝐾 = (MetOpen‘𝐷)
1412, 13metcnpi3 24560 . . . . . 6 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))) ∧ (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 1 ∈ ℝ+)) → ∃𝑦 ∈ ℝ+𝑥𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1))
1511, 14mpanr2 704 . . . . 5 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))) ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∃𝑦 ∈ ℝ+𝑥𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1))
165, 10, 15mpanl12 702 . . . 4 (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) → ∃𝑦 ∈ ℝ+𝑥𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1))
17 rpreccl 13062 . . . . . . . 8 (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℝ+)
1817rpred 13078 . . . . . . 7 (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℝ)
1918ad2antlr 727 . . . . . 6 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ ∀𝑥𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1)) → (1 / 𝑦) ∈ ℝ)
20 eqid 2736 . . . . . . . . . . . . . . 15 ( −𝑣𝑈) = ( −𝑣𝑈)
21 eqid 2736 . . . . . . . . . . . . . . 15 (normCV𝑈) = (normCV𝑈)
222, 20, 21, 3imsdval 30706 . . . . . . . . . . . . . 14 ((𝑈 ∈ NrmCVec ∧ 𝑥𝑋𝑃𝑋) → (𝑥𝐶𝑃) = ((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)))
231, 22mp3an1 1449 . . . . . . . . . . . . 13 ((𝑥𝑋𝑃𝑋) → (𝑥𝐶𝑃) = ((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)))
2423breq1d 5152 . . . . . . . . . . . 12 ((𝑥𝑋𝑃𝑋) → ((𝑥𝐶𝑃) ≤ 𝑦 ↔ ((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦))
25 blocni.l . . . . . . . . . . . . . . . . 17 𝑇𝐿
26 blocni.4 . . . . . . . . . . . . . . . . . 18 𝐿 = (𝑈 LnOp 𝑊)
272, 7, 26lnof 30775 . . . . . . . . . . . . . . . . 17 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇𝐿) → 𝑇:𝑋⟶(BaseSet‘𝑊))
281, 6, 25, 27mp3an 1462 . . . . . . . . . . . . . . . 16 𝑇:𝑋⟶(BaseSet‘𝑊)
2928ffvelcdmi 7102 . . . . . . . . . . . . . . 15 (𝑥𝑋 → (𝑇𝑥) ∈ (BaseSet‘𝑊))
3028ffvelcdmi 7102 . . . . . . . . . . . . . . 15 (𝑃𝑋 → (𝑇𝑃) ∈ (BaseSet‘𝑊))
31 eqid 2736 . . . . . . . . . . . . . . . . 17 ( −𝑣𝑊) = ( −𝑣𝑊)
32 eqid 2736 . . . . . . . . . . . . . . . . 17 (normCV𝑊) = (normCV𝑊)
337, 31, 32, 8imsdval 30706 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ NrmCVec ∧ (𝑇𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇𝑥)𝐷(𝑇𝑃)) = ((normCV𝑊)‘((𝑇𝑥)( −𝑣𝑊)(𝑇𝑃))))
346, 33mp3an1 1449 . . . . . . . . . . . . . . 15 (((𝑇𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇𝑥)𝐷(𝑇𝑃)) = ((normCV𝑊)‘((𝑇𝑥)( −𝑣𝑊)(𝑇𝑃))))
3529, 30, 34syl2an 596 . . . . . . . . . . . . . 14 ((𝑥𝑋𝑃𝑋) → ((𝑇𝑥)𝐷(𝑇𝑃)) = ((normCV𝑊)‘((𝑇𝑥)( −𝑣𝑊)(𝑇𝑃))))
361, 6, 253pm3.2i 1339 . . . . . . . . . . . . . . . 16 (𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇𝐿)
372, 20, 31, 26lnosub 30779 . . . . . . . . . . . . . . . 16 (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇𝐿) ∧ (𝑥𝑋𝑃𝑋)) → (𝑇‘(𝑥( −𝑣𝑈)𝑃)) = ((𝑇𝑥)( −𝑣𝑊)(𝑇𝑃)))
3836, 37mpan 690 . . . . . . . . . . . . . . 15 ((𝑥𝑋𝑃𝑋) → (𝑇‘(𝑥( −𝑣𝑈)𝑃)) = ((𝑇𝑥)( −𝑣𝑊)(𝑇𝑃)))
3938fveq2d 6909 . . . . . . . . . . . . . 14 ((𝑥𝑋𝑃𝑋) → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) = ((normCV𝑊)‘((𝑇𝑥)( −𝑣𝑊)(𝑇𝑃))))
4035, 39eqtr4d 2779 . . . . . . . . . . . . 13 ((𝑥𝑋𝑃𝑋) → ((𝑇𝑥)𝐷(𝑇𝑃)) = ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))))
4140breq1d 5152 . . . . . . . . . . . 12 ((𝑥𝑋𝑃𝑋) → (((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1 ↔ ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1))
4224, 41imbi12d 344 . . . . . . . . . . 11 ((𝑥𝑋𝑃𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1) ↔ (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1)))
4342ancoms 458 . . . . . . . . . 10 ((𝑃𝑋𝑥𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1) ↔ (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1)))
4443adantlr 715 . . . . . . . . 9 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ 𝑥𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1) ↔ (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1)))
4544ralbidva 3175 . . . . . . . 8 ((𝑃𝑋𝑦 ∈ ℝ+) → (∀𝑥𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1) ↔ ∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1)))
46 2fveq3 6910 . . . . . . . . . . . 12 (𝑧 = (0vec𝑈) → ((normCV𝑊)‘(𝑇𝑧)) = ((normCV𝑊)‘(𝑇‘(0vec𝑈))))
47 fveq2 6905 . . . . . . . . . . . . 13 (𝑧 = (0vec𝑈) → ((normCV𝑈)‘𝑧) = ((normCV𝑈)‘(0vec𝑈)))
4847oveq2d 7448 . . . . . . . . . . . 12 (𝑧 = (0vec𝑈) → ((1 / 𝑦) · ((normCV𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV𝑈)‘(0vec𝑈))))
4946, 48breq12d 5155 . . . . . . . . . . 11 (𝑧 = (0vec𝑈) → (((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧)) ↔ ((normCV𝑊)‘(𝑇‘(0vec𝑈))) ≤ ((1 / 𝑦) · ((normCV𝑈)‘(0vec𝑈)))))
501a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → 𝑈 ∈ NrmCVec)
51 simpll 766 . . . . . . . . . . . . . . . . . . . 20 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → 𝑃𝑋)
52 simpr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃𝑋𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ+)
532, 21nvcl 30681 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑈 ∈ NrmCVec ∧ 𝑧𝑋) → ((normCV𝑈)‘𝑧) ∈ ℝ)
541, 53mpan 690 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧𝑋 → ((normCV𝑈)‘𝑧) ∈ ℝ)
5554adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧𝑋𝑧 ≠ (0vec𝑈)) → ((normCV𝑈)‘𝑧) ∈ ℝ)
56 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (0vec𝑈) = (0vec𝑈)
572, 56, 21nvgt0 30694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑈 ∈ NrmCVec ∧ 𝑧𝑋) → (𝑧 ≠ (0vec𝑈) ↔ 0 < ((normCV𝑈)‘𝑧)))
581, 57mpan 690 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧𝑋 → (𝑧 ≠ (0vec𝑈) ↔ 0 < ((normCV𝑈)‘𝑧)))
5958biimpa 476 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧𝑋𝑧 ≠ (0vec𝑈)) → 0 < ((normCV𝑈)‘𝑧))
6055, 59elrpd 13075 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧𝑋𝑧 ≠ (0vec𝑈)) → ((normCV𝑈)‘𝑧) ∈ ℝ+)
61 rpdivcl 13061 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ ℝ+ ∧ ((normCV𝑈)‘𝑧) ∈ ℝ+) → (𝑦 / ((normCV𝑈)‘𝑧)) ∈ ℝ+)
6252, 60, 61syl2an 596 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (𝑦 / ((normCV𝑈)‘𝑧)) ∈ ℝ+)
6362rpcnd 13080 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (𝑦 / ((normCV𝑈)‘𝑧)) ∈ ℂ)
64 simprl 770 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → 𝑧𝑋)
65 eqid 2736 . . . . . . . . . . . . . . . . . . . . . 22 ( ·𝑠OLD𝑈) = ( ·𝑠OLD𝑈)
662, 65nvscl 30646 . . . . . . . . . . . . . . . . . . . . 21 ((𝑈 ∈ NrmCVec ∧ (𝑦 / ((normCV𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧𝑋) → ((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧) ∈ 𝑋)
6750, 63, 64, 66syl3anc 1372 . . . . . . . . . . . . . . . . . . . 20 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧) ∈ 𝑋)
68 eqid 2736 . . . . . . . . . . . . . . . . . . . . 21 ( +𝑣𝑈) = ( +𝑣𝑈)
692, 68, 20nvpncan2 30673 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∈ NrmCVec ∧ 𝑃𝑋 ∧ ((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧) ∈ 𝑋) → ((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃) = ((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))
7050, 51, 67, 69syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃) = ((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))
7170fveq2d 6909 . . . . . . . . . . . . . . . . . 18 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑈)‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)) = ((normCV𝑈)‘((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)))
7262rprege0d 13085 . . . . . . . . . . . . . . . . . . 19 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((𝑦 / ((normCV𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 / ((normCV𝑈)‘𝑧))))
732, 65, 21nvsge0 30684 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ NrmCVec ∧ ((𝑦 / ((normCV𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 / ((normCV𝑈)‘𝑧))) ∧ 𝑧𝑋) → ((normCV𝑈)‘((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) = ((𝑦 / ((normCV𝑈)‘𝑧)) · ((normCV𝑈)‘𝑧)))
7450, 72, 64, 73syl3anc 1372 . . . . . . . . . . . . . . . . . 18 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑈)‘((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) = ((𝑦 / ((normCV𝑈)‘𝑧)) · ((normCV𝑈)‘𝑧)))
75 rpcn 13046 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℝ+𝑦 ∈ ℂ)
7675ad2antlr 727 . . . . . . . . . . . . . . . . . . 19 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → 𝑦 ∈ ℂ)
7754ad2antrl 728 . . . . . . . . . . . . . . . . . . . 20 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑈)‘𝑧) ∈ ℝ)
7877recnd 11290 . . . . . . . . . . . . . . . . . . 19 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑈)‘𝑧) ∈ ℂ)
792, 56, 21nvz 30689 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑈 ∈ NrmCVec ∧ 𝑧𝑋) → (((normCV𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec𝑈)))
801, 79mpan 690 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧𝑋 → (((normCV𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec𝑈)))
8180necon3bid 2984 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑋 → (((normCV𝑈)‘𝑧) ≠ 0 ↔ 𝑧 ≠ (0vec𝑈)))
8281biimpar 477 . . . . . . . . . . . . . . . . . . . 20 ((𝑧𝑋𝑧 ≠ (0vec𝑈)) → ((normCV𝑈)‘𝑧) ≠ 0)
8382adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑈)‘𝑧) ≠ 0)
8476, 78, 83divcan1d 12045 . . . . . . . . . . . . . . . . . 18 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((𝑦 / ((normCV𝑈)‘𝑧)) · ((normCV𝑈)‘𝑧)) = 𝑦)
8571, 74, 843eqtrd 2780 . . . . . . . . . . . . . . . . 17 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑈)‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)) = 𝑦)
86 rpre 13044 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
8786leidd 11830 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℝ+𝑦𝑦)
8887ad2antlr 727 . . . . . . . . . . . . . . . . 17 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → 𝑦𝑦)
8985, 88eqbrtrd 5164 . . . . . . . . . . . . . . . 16 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑈)‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)) ≤ 𝑦)
902, 68nvgcl 30640 . . . . . . . . . . . . . . . . . 18 ((𝑈 ∈ NrmCVec ∧ 𝑃𝑋 ∧ ((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧) ∈ 𝑋) → (𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) ∈ 𝑋)
9150, 51, 67, 90syl3anc 1372 . . . . . . . . . . . . . . . . 17 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) ∈ 𝑋)
92 fvoveq1 7455 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) → ((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) = ((normCV𝑈)‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)))
9392breq1d 5152 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) → (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 ↔ ((normCV𝑈)‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)) ≤ 𝑦))
94 fvoveq1 7455 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = (𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) → (𝑇‘(𝑥( −𝑣𝑈)𝑃)) = (𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)))
9594fveq2d 6909 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) = ((normCV𝑊)‘(𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃))))
9695breq1d 5152 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) → (((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1 ↔ ((normCV𝑊)‘(𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃))) ≤ 1))
9793, 96imbi12d 344 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) → ((((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1) ↔ (((normCV𝑈)‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃))) ≤ 1)))
9897rspcv 3617 . . . . . . . . . . . . . . . . 17 ((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) ∈ 𝑋 → (∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1) → (((normCV𝑈)‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃))) ≤ 1)))
9991, 98syl 17 . . . . . . . . . . . . . . . 16 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1) → (((normCV𝑈)‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃))) ≤ 1)))
10089, 99mpid 44 . . . . . . . . . . . . . . 15 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1) → ((normCV𝑊)‘(𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃))) ≤ 1))
10128ffvelcdmi 7102 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑋 → (𝑇𝑧) ∈ (BaseSet‘𝑊))
1027, 32nvcl 30681 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ NrmCVec ∧ (𝑇𝑧) ∈ (BaseSet‘𝑊)) → ((normCV𝑊)‘(𝑇𝑧)) ∈ ℝ)
1036, 101, 102sylancr 587 . . . . . . . . . . . . . . . . . 18 (𝑧𝑋 → ((normCV𝑊)‘(𝑇𝑧)) ∈ ℝ)
104103ad2antrl 728 . . . . . . . . . . . . . . . . 17 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑊)‘(𝑇𝑧)) ∈ ℝ)
105 1red 11263 . . . . . . . . . . . . . . . . 17 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → 1 ∈ ℝ)
106104, 105, 62lemuldiv2d 13128 . . . . . . . . . . . . . . . 16 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (((𝑦 / ((normCV𝑈)‘𝑧)) · ((normCV𝑊)‘(𝑇𝑧))) ≤ 1 ↔ ((normCV𝑊)‘(𝑇𝑧)) ≤ (1 / (𝑦 / ((normCV𝑈)‘𝑧)))))
10770fveq2d 6909 . . . . . . . . . . . . . . . . . . . 20 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)) = (𝑇‘((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)))
108 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . 23 ( ·𝑠OLD𝑊) = ( ·𝑠OLD𝑊)
1092, 65, 108, 26lnomul 30780 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇𝐿) ∧ ((𝑦 / ((normCV𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧𝑋)) → (𝑇‘((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) = ((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑊)(𝑇𝑧)))
11036, 109mpan 690 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦 / ((normCV𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧𝑋) → (𝑇‘((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) = ((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑊)(𝑇𝑧)))
11163, 64, 110syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (𝑇‘((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧)) = ((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑊)(𝑇𝑧)))
112107, 111eqtrd 2776 . . . . . . . . . . . . . . . . . . 19 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃)) = ((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑊)(𝑇𝑧)))
113112fveq2d 6909 . . . . . . . . . . . . . . . . . 18 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑊)‘(𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃))) = ((normCV𝑊)‘((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑊)(𝑇𝑧))))
1146a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → 𝑊 ∈ NrmCVec)
115101ad2antrl 728 . . . . . . . . . . . . . . . . . . 19 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (𝑇𝑧) ∈ (BaseSet‘𝑊))
1167, 108, 32nvsge0 30684 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ NrmCVec ∧ ((𝑦 / ((normCV𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 / ((normCV𝑈)‘𝑧))) ∧ (𝑇𝑧) ∈ (BaseSet‘𝑊)) → ((normCV𝑊)‘((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑊)(𝑇𝑧))) = ((𝑦 / ((normCV𝑈)‘𝑧)) · ((normCV𝑊)‘(𝑇𝑧))))
117114, 72, 115, 116syl3anc 1372 . . . . . . . . . . . . . . . . . 18 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑊)‘((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑊)(𝑇𝑧))) = ((𝑦 / ((normCV𝑈)‘𝑧)) · ((normCV𝑊)‘(𝑇𝑧))))
118113, 117eqtrd 2776 . . . . . . . . . . . . . . . . 17 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((normCV𝑊)‘(𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃))) = ((𝑦 / ((normCV𝑈)‘𝑧)) · ((normCV𝑊)‘(𝑇𝑧))))
119118breq1d 5152 . . . . . . . . . . . . . . . 16 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (((normCV𝑊)‘(𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃))) ≤ 1 ↔ ((𝑦 / ((normCV𝑈)‘𝑧)) · ((normCV𝑊)‘(𝑇𝑧))) ≤ 1))
120 rpcnne0 13054 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℝ+ → (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0))
121 rpcnne0 13054 . . . . . . . . . . . . . . . . . . . 20 (((normCV𝑈)‘𝑧) ∈ ℝ+ → (((normCV𝑈)‘𝑧) ∈ ℂ ∧ ((normCV𝑈)‘𝑧) ≠ 0))
122 recdiv 11974 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) ∧ (((normCV𝑈)‘𝑧) ∈ ℂ ∧ ((normCV𝑈)‘𝑧) ≠ 0)) → (1 / (𝑦 / ((normCV𝑈)‘𝑧))) = (((normCV𝑈)‘𝑧) / 𝑦))
123120, 121, 122syl2an 596 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℝ+ ∧ ((normCV𝑈)‘𝑧) ∈ ℝ+) → (1 / (𝑦 / ((normCV𝑈)‘𝑧))) = (((normCV𝑈)‘𝑧) / 𝑦))
12452, 60, 123syl2an 596 . . . . . . . . . . . . . . . . . 18 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (1 / (𝑦 / ((normCV𝑈)‘𝑧))) = (((normCV𝑈)‘𝑧) / 𝑦))
125 rpne0 13052 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℝ+𝑦 ≠ 0)
126125ad2antlr 727 . . . . . . . . . . . . . . . . . . 19 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → 𝑦 ≠ 0)
12778, 76, 126divrec2d 12048 . . . . . . . . . . . . . . . . . 18 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (((normCV𝑈)‘𝑧) / 𝑦) = ((1 / 𝑦) · ((normCV𝑈)‘𝑧)))
128124, 127eqtr2d 2777 . . . . . . . . . . . . . . . . 17 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → ((1 / 𝑦) · ((normCV𝑈)‘𝑧)) = (1 / (𝑦 / ((normCV𝑈)‘𝑧))))
129128breq2d 5154 . . . . . . . . . . . . . . . 16 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧)) ↔ ((normCV𝑊)‘(𝑇𝑧)) ≤ (1 / (𝑦 / ((normCV𝑈)‘𝑧)))))
130106, 119, 1293bitr4d 311 . . . . . . . . . . . . . . 15 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (((normCV𝑊)‘(𝑇‘((𝑃( +𝑣𝑈)((𝑦 / ((normCV𝑈)‘𝑧))( ·𝑠OLD𝑈)𝑧))( −𝑣𝑈)𝑃))) ≤ 1 ↔ ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧))))
131100, 130sylibd 239 . . . . . . . . . . . . . 14 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ (𝑧𝑋𝑧 ≠ (0vec𝑈))) → (∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1) → ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧))))
132131anassrs 467 . . . . . . . . . . . . 13 ((((𝑃𝑋𝑦 ∈ ℝ+) ∧ 𝑧𝑋) ∧ 𝑧 ≠ (0vec𝑈)) → (∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1) → ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧))))
133132imp 406 . . . . . . . . . . . 12 (((((𝑃𝑋𝑦 ∈ ℝ+) ∧ 𝑧𝑋) ∧ 𝑧 ≠ (0vec𝑈)) ∧ ∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1)) → ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧)))
134133an32s 652 . . . . . . . . . . 11 (((((𝑃𝑋𝑦 ∈ ℝ+) ∧ 𝑧𝑋) ∧ ∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1)) ∧ 𝑧 ≠ (0vec𝑈)) → ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧)))
135 eqid 2736 . . . . . . . . . . . . . . . . . 18 (0vec𝑊) = (0vec𝑊)
1362, 7, 56, 135, 26lno0 30776 . . . . . . . . . . . . . . . . 17 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇𝐿) → (𝑇‘(0vec𝑈)) = (0vec𝑊))
1371, 6, 25, 136mp3an 1462 . . . . . . . . . . . . . . . 16 (𝑇‘(0vec𝑈)) = (0vec𝑊)
138137fveq2i 6908 . . . . . . . . . . . . . . 15 ((normCV𝑊)‘(𝑇‘(0vec𝑈))) = ((normCV𝑊)‘(0vec𝑊))
139135, 32nvz0 30688 . . . . . . . . . . . . . . . 16 (𝑊 ∈ NrmCVec → ((normCV𝑊)‘(0vec𝑊)) = 0)
1406, 139ax-mp 5 . . . . . . . . . . . . . . 15 ((normCV𝑊)‘(0vec𝑊)) = 0
141138, 140eqtri 2764 . . . . . . . . . . . . . 14 ((normCV𝑊)‘(𝑇‘(0vec𝑈))) = 0
142 0le0 12368 . . . . . . . . . . . . . 14 0 ≤ 0
143141, 142eqbrtri 5163 . . . . . . . . . . . . 13 ((normCV𝑊)‘(𝑇‘(0vec𝑈))) ≤ 0
14417rpcnd 13080 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ+ → (1 / 𝑦) ∈ ℂ)
14556, 21nvz0 30688 . . . . . . . . . . . . . . . . 17 (𝑈 ∈ NrmCVec → ((normCV𝑈)‘(0vec𝑈)) = 0)
1461, 145ax-mp 5 . . . . . . . . . . . . . . . 16 ((normCV𝑈)‘(0vec𝑈)) = 0
147146oveq2i 7443 . . . . . . . . . . . . . . 15 ((1 / 𝑦) · ((normCV𝑈)‘(0vec𝑈))) = ((1 / 𝑦) · 0)
148 mul01 11441 . . . . . . . . . . . . . . 15 ((1 / 𝑦) ∈ ℂ → ((1 / 𝑦) · 0) = 0)
149147, 148eqtrid 2788 . . . . . . . . . . . . . 14 ((1 / 𝑦) ∈ ℂ → ((1 / 𝑦) · ((normCV𝑈)‘(0vec𝑈))) = 0)
150144, 149syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ+ → ((1 / 𝑦) · ((normCV𝑈)‘(0vec𝑈))) = 0)
151143, 150breqtrrid 5180 . . . . . . . . . . . 12 (𝑦 ∈ ℝ+ → ((normCV𝑊)‘(𝑇‘(0vec𝑈))) ≤ ((1 / 𝑦) · ((normCV𝑈)‘(0vec𝑈))))
152151ad3antlr 731 . . . . . . . . . . 11 ((((𝑃𝑋𝑦 ∈ ℝ+) ∧ 𝑧𝑋) ∧ ∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1)) → ((normCV𝑊)‘(𝑇‘(0vec𝑈))) ≤ ((1 / 𝑦) · ((normCV𝑈)‘(0vec𝑈))))
15349, 134, 152pm2.61ne 3026 . . . . . . . . . 10 ((((𝑃𝑋𝑦 ∈ ℝ+) ∧ 𝑧𝑋) ∧ ∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1)) → ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧)))
154153ex 412 . . . . . . . . 9 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ 𝑧𝑋) → (∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1) → ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧))))
155154ralrimdva 3153 . . . . . . . 8 ((𝑃𝑋𝑦 ∈ ℝ+) → (∀𝑥𝑋 (((normCV𝑈)‘(𝑥( −𝑣𝑈)𝑃)) ≤ 𝑦 → ((normCV𝑊)‘(𝑇‘(𝑥( −𝑣𝑈)𝑃))) ≤ 1) → ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧))))
15645, 155sylbid 240 . . . . . . 7 ((𝑃𝑋𝑦 ∈ ℝ+) → (∀𝑥𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1) → ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧))))
157156imp 406 . . . . . 6 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ ∀𝑥𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1)) → ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧)))
158 oveq1 7439 . . . . . . . . 9 (𝑥 = (1 / 𝑦) → (𝑥 · ((normCV𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV𝑈)‘𝑧)))
159158breq2d 5154 . . . . . . . 8 (𝑥 = (1 / 𝑦) → (((normCV𝑊)‘(𝑇𝑧)) ≤ (𝑥 · ((normCV𝑈)‘𝑧)) ↔ ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧))))
160159ralbidv 3177 . . . . . . 7 (𝑥 = (1 / 𝑦) → (∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ (𝑥 · ((normCV𝑈)‘𝑧)) ↔ ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧))))
161160rspcev 3621 . . . . . 6 (((1 / 𝑦) ∈ ℝ ∧ ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ ((1 / 𝑦) · ((normCV𝑈)‘𝑧))) → ∃𝑥 ∈ ℝ ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ (𝑥 · ((normCV𝑈)‘𝑧)))
16219, 157, 161syl2anc 584 . . . . 5 (((𝑃𝑋𝑦 ∈ ℝ+) ∧ ∀𝑥𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1)) → ∃𝑥 ∈ ℝ ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ (𝑥 · ((normCV𝑈)‘𝑧)))
163162rexlimdva2 3156 . . . 4 (𝑃𝑋 → (∃𝑦 ∈ ℝ+𝑥𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑃)) ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ (𝑥 · ((normCV𝑈)‘𝑧))))
16416, 163syl5 34 . . 3 (𝑃𝑋 → (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) → ∃𝑥 ∈ ℝ ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ (𝑥 · ((normCV𝑈)‘𝑧))))
165164imp 406 . 2 ((𝑃𝑋𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∃𝑥 ∈ ℝ ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ (𝑥 · ((normCV𝑈)‘𝑧)))
166 blocni.5 . . . 4 𝐵 = (𝑈 BLnOp 𝑊)
1672, 21, 32, 26, 166, 1, 6isblo3i 30821 . . 3 (𝑇𝐵 ↔ (𝑇𝐿 ∧ ∃𝑥 ∈ ℝ ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ (𝑥 · ((normCV𝑈)‘𝑧))))
16825, 167mpbiran 709 . 2 (𝑇𝐵 ↔ ∃𝑥 ∈ ℝ ∀𝑧𝑋 ((normCV𝑊)‘(𝑇𝑧)) ≤ (𝑥 · ((normCV𝑈)‘𝑧)))
169165, 168sylibr 234 1 ((𝑃𝑋𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑇𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1539  wcel 2107  wne 2939  wral 3060  wrex 3069   class class class wbr 5142  wf 6556  cfv 6560  (class class class)co 7432  cc 11154  cr 11155  0cc0 11156  1c1 11157   · cmul 11161   < clt 11296  cle 11297   / cdiv 11921  +crp 13035  ∞Metcxmet 21350  MetOpencmopn 21355   CnP ccnp 23234  NrmCVeccnv 30604   +𝑣 cpv 30605  BaseSetcba 30606   ·𝑠OLD cns 30607  0veccn0v 30608  𝑣 cnsb 30609  normCVcnmcv 30610  IndMetcims 30611   LnOp clno 30760   BLnOp cblo 30762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233  ax-pre-sup 11234  ax-addf 11235  ax-mulf 11236
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-1st 8015  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-er 8746  df-map 8869  df-en 8987  df-dom 8988  df-sdom 8989  df-sup 9483  df-inf 9484  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-div 11922  df-nn 12268  df-2 12330  df-3 12331  df-n0 12529  df-z 12616  df-uz 12880  df-q 12992  df-rp 13036  df-xneg 13155  df-xadd 13156  df-xmul 13157  df-seq 14044  df-exp 14104  df-cj 15139  df-re 15140  df-im 15141  df-sqrt 15275  df-abs 15276  df-topgen 17489  df-psmet 21357  df-xmet 21358  df-met 21359  df-bl 21360  df-mopn 21361  df-top 22901  df-topon 22918  df-bases 22954  df-cnp 23237  df-grpo 30513  df-gid 30514  df-ginv 30515  df-gdiv 30516  df-ablo 30565  df-vc 30579  df-nv 30612  df-va 30615  df-ba 30616  df-sm 30617  df-0v 30618  df-vs 30619  df-nmcv 30620  df-ims 30621  df-lno 30764  df-nmoo 30765  df-blo 30766  df-0o 30767
This theorem is referenced by:  blocni  30825  lnocni  30826
  Copyright terms: Public domain W3C validator