MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  blocnilem Structured version   Visualization version   GIF version
Theorem blocnilem 30057
Description: Lemma for blocni 30058 and lnocni 30059. 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 29945 . . . . . 6 (π‘ˆ ∈ NrmCVec β†’ 𝐢 ∈ (∞Metβ€˜π‘‹))
51, 4ax-mp 5 . . . . 5 𝐢 ∈ (∞Metβ€˜π‘‹)
6 blocni.w . . . . . 6 π‘Š ∈ NrmCVec
7 eqid 2733 . . . . . . 7 (BaseSetβ€˜π‘Š) = (BaseSetβ€˜π‘Š)
8 blocni.d . . . . . . 7 𝐷 = (IndMetβ€˜π‘Š)
97, 8imsxmet 29945 . . . . . 6 (π‘Š ∈ NrmCVec β†’ 𝐷 ∈ (∞Metβ€˜(BaseSetβ€˜π‘Š)))
106, 9ax-mp 5 . . . . 5 𝐷 ∈ (∞Metβ€˜(BaseSetβ€˜π‘Š))
11 1rp 12978 . . . . . 6 1 ∈ ℝ+
12 blocni.j . . . . . . 7 𝐽 = (MetOpenβ€˜πΆ)
13 blocni.k . . . . . . 7 𝐾 = (MetOpenβ€˜π·)
1412, 13metcnpi3 24055 . . . . . 6 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝐷 ∈ (∞Metβ€˜(BaseSetβ€˜π‘Š))) ∧ (𝑇 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 1 ∈ ℝ+)) β†’ βˆƒπ‘¦ ∈ ℝ+ βˆ€π‘₯ ∈ 𝑋 ((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1))
1511, 14mpanr2 703 . . . . 5 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝐷 ∈ (∞Metβ€˜(BaseSetβ€˜π‘Š))) ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ)) β†’ βˆƒπ‘¦ ∈ ℝ+ βˆ€π‘₯ ∈ 𝑋 ((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1))
165, 10, 15mpanl12 701 . . . 4 (𝑇 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) β†’ βˆƒπ‘¦ ∈ ℝ+ βˆ€π‘₯ ∈ 𝑋 ((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1))
17 rpreccl 13000 . . . . . . . 8 (𝑦 ∈ ℝ+ β†’ (1 / 𝑦) ∈ ℝ+)
1817rpred 13016 . . . . . . 7 (𝑦 ∈ ℝ+ β†’ (1 / 𝑦) ∈ ℝ)
1918ad2antlr 726 . . . . . 6 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ βˆ€π‘₯ ∈ 𝑋 ((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1)) β†’ (1 / 𝑦) ∈ ℝ)
20 eqid 2733 . . . . . . . . . . . . . . 15 ( βˆ’π‘£ β€˜π‘ˆ) = ( βˆ’π‘£ β€˜π‘ˆ)
21 eqid 2733 . . . . . . . . . . . . . . 15 (normCVβ€˜π‘ˆ) = (normCVβ€˜π‘ˆ)
222, 20, 21, 3imsdval 29939 . . . . . . . . . . . . . 14 ((π‘ˆ ∈ NrmCVec ∧ π‘₯ ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ (π‘₯𝐢𝑃) = ((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)))
231, 22mp3an1 1449 . . . . . . . . . . . . 13 ((π‘₯ ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ (π‘₯𝐢𝑃) = ((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)))
2423breq1d 5159 . . . . . . . . . . . 12 ((π‘₯ ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ ((π‘₯𝐢𝑃) ≀ 𝑦 ↔ ((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦))
25 blocni.l . . . . . . . . . . . . . . . . 17 𝑇 ∈ 𝐿
26 blocni.4 . . . . . . . . . . . . . . . . . 18 𝐿 = (π‘ˆ LnOp π‘Š)
272, 7, 26lnof 30008 . . . . . . . . . . . . . . . . 17 ((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) β†’ 𝑇:π‘‹βŸΆ(BaseSetβ€˜π‘Š))
281, 6, 25, 27mp3an 1462 . . . . . . . . . . . . . . . 16 𝑇:π‘‹βŸΆ(BaseSetβ€˜π‘Š)
2928ffvelcdmi 7086 . . . . . . . . . . . . . . 15 (π‘₯ ∈ 𝑋 β†’ (π‘‡β€˜π‘₯) ∈ (BaseSetβ€˜π‘Š))
3028ffvelcdmi 7086 . . . . . . . . . . . . . . 15 (𝑃 ∈ 𝑋 β†’ (π‘‡β€˜π‘ƒ) ∈ (BaseSetβ€˜π‘Š))
31 eqid 2733 . . . . . . . . . . . . . . . . 17 ( βˆ’π‘£ β€˜π‘Š) = ( βˆ’π‘£ β€˜π‘Š)
32 eqid 2733 . . . . . . . . . . . . . . . . 17 (normCVβ€˜π‘Š) = (normCVβ€˜π‘Š)
337, 31, 32, 8imsdval 29939 . . . . . . . . . . . . . . . 16 ((π‘Š ∈ NrmCVec ∧ (π‘‡β€˜π‘₯) ∈ (BaseSetβ€˜π‘Š) ∧ (π‘‡β€˜π‘ƒ) ∈ (BaseSetβ€˜π‘Š)) β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) = ((normCVβ€˜π‘Š)β€˜((π‘‡β€˜π‘₯)( βˆ’π‘£ β€˜π‘Š)(π‘‡β€˜π‘ƒ))))
346, 33mp3an1 1449 . . . . . . . . . . . . . . 15 (((π‘‡β€˜π‘₯) ∈ (BaseSetβ€˜π‘Š) ∧ (π‘‡β€˜π‘ƒ) ∈ (BaseSetβ€˜π‘Š)) β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) = ((normCVβ€˜π‘Š)β€˜((π‘‡β€˜π‘₯)( βˆ’π‘£ β€˜π‘Š)(π‘‡β€˜π‘ƒ))))
3529, 30, 34syl2an 597 . . . . . . . . . . . . . 14 ((π‘₯ ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) = ((normCVβ€˜π‘Š)β€˜((π‘‡β€˜π‘₯)( βˆ’π‘£ β€˜π‘Š)(π‘‡β€˜π‘ƒ))))
361, 6, 253pm3.2i 1340 . . . . . . . . . . . . . . . 16 (π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ NrmCVec ∧ 𝑇 ∈ 𝐿)
372, 20, 31, 26lnosub 30012 . . . . . . . . . . . . . . . 16 (((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑃 ∈ 𝑋)) β†’ (π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) = ((π‘‡β€˜π‘₯)( βˆ’π‘£ β€˜π‘Š)(π‘‡β€˜π‘ƒ)))
3836, 37mpan 689 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ (π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) = ((π‘‡β€˜π‘₯)( βˆ’π‘£ β€˜π‘Š)(π‘‡β€˜π‘ƒ)))
3938fveq2d 6896 . . . . . . . . . . . . . 14 ((π‘₯ ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) = ((normCVβ€˜π‘Š)β€˜((π‘‡β€˜π‘₯)( βˆ’π‘£ β€˜π‘Š)(π‘‡β€˜π‘ƒ))))
4035, 39eqtr4d 2776 . . . . . . . . . . . . 13 ((π‘₯ ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) = ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))))
4140breq1d 5159 . . . . . . . . . . . 12 ((π‘₯ ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ (((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1 ↔ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1))
4224, 41imbi12d 345 . . . . . . . . . . 11 ((π‘₯ ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ (((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1) ↔ (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1)))
4342ancoms 460 . . . . . . . . . 10 ((𝑃 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋) β†’ (((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1) ↔ (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1)))
4443adantlr 714 . . . . . . . . 9 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ π‘₯ ∈ 𝑋) β†’ (((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1) ↔ (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1)))
4544ralbidva 3176 . . . . . . . 8 ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) β†’ (βˆ€π‘₯ ∈ 𝑋 ((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1) ↔ βˆ€π‘₯ ∈ 𝑋 (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1)))
46 2fveq3 6897 . . . . . . . . . . . 12 (𝑧 = (0vecβ€˜π‘ˆ) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) = ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(0vecβ€˜π‘ˆ))))
47 fveq2 6892 . . . . . . . . . . . . 13 (𝑧 = (0vecβ€˜π‘ˆ) β†’ ((normCVβ€˜π‘ˆ)β€˜π‘§) = ((normCVβ€˜π‘ˆ)β€˜(0vecβ€˜π‘ˆ)))
4847oveq2d 7425 . . . . . . . . . . . 12 (𝑧 = (0vecβ€˜π‘ˆ) β†’ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)) = ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜(0vecβ€˜π‘ˆ))))
4946, 48breq12d 5162 . . . . . . . . . . 11 (𝑧 = (0vecβ€˜π‘ˆ) β†’ (((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)) ↔ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(0vecβ€˜π‘ˆ))) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜(0vecβ€˜π‘ˆ)))))
501a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ π‘ˆ ∈ NrmCVec)
51 simpll 766 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ 𝑃 ∈ 𝑋)
52 simpr 486 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) β†’ 𝑦 ∈ ℝ+)
532, 21nvcl 29914 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘ˆ ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) β†’ ((normCVβ€˜π‘ˆ)β€˜π‘§) ∈ ℝ)
541, 53mpan 689 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ 𝑋 β†’ ((normCVβ€˜π‘ˆ)β€˜π‘§) ∈ ℝ)
5554adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ)) β†’ ((normCVβ€˜π‘ˆ)β€˜π‘§) ∈ ℝ)
56 eqid 2733 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (0vecβ€˜π‘ˆ) = (0vecβ€˜π‘ˆ)
572, 56, 21nvgt0 29927 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘ˆ ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) β†’ (𝑧 β‰  (0vecβ€˜π‘ˆ) ↔ 0 < ((normCVβ€˜π‘ˆ)β€˜π‘§)))
581, 57mpan 689 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ 𝑋 β†’ (𝑧 β‰  (0vecβ€˜π‘ˆ) ↔ 0 < ((normCVβ€˜π‘ˆ)β€˜π‘§)))
5958biimpa 478 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ)) β†’ 0 < ((normCVβ€˜π‘ˆ)β€˜π‘§))
6055, 59elrpd 13013 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ)) β†’ ((normCVβ€˜π‘ˆ)β€˜π‘§) ∈ ℝ+)
61 rpdivcl 12999 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ ℝ+ ∧ ((normCVβ€˜π‘ˆ)β€˜π‘§) ∈ ℝ+) β†’ (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) ∈ ℝ+)
6252, 60, 61syl2an 597 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) ∈ ℝ+)
6362rpcnd 13018 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) ∈ β„‚)
64 simprl 770 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ 𝑧 ∈ 𝑋)
65 eqid 2733 . . . . . . . . . . . . . . . . . . . . . 22 ( ·𝑠OLD β€˜π‘ˆ) = ( ·𝑠OLD β€˜π‘ˆ)
662, 65nvscl 29879 . . . . . . . . . . . . . . . . . . . . 21 ((π‘ˆ ∈ NrmCVec ∧ (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) ∈ β„‚ ∧ 𝑧 ∈ 𝑋) β†’ ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧) ∈ 𝑋)
6750, 63, 64, 66syl3anc 1372 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧) ∈ 𝑋)
68 eqid 2733 . . . . . . . . . . . . . . . . . . . . 21 ( +𝑣 β€˜π‘ˆ) = ( +𝑣 β€˜π‘ˆ)
692, 68, 20nvpncan2 29906 . . . . . . . . . . . . . . . . . . . 20 ((π‘ˆ ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧) ∈ 𝑋) β†’ ((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃) = ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))
7050, 51, 67, 69syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃) = ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))
7170fveq2d 6896 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((normCVβ€˜π‘ˆ)β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃)) = ((normCVβ€˜π‘ˆ)β€˜((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)))
7262rprege0d 13023 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) ∈ ℝ ∧ 0 ≀ (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))))
732, 65, 21nvsge0 29917 . . . . . . . . . . . . . . . . . . 19 ((π‘ˆ ∈ NrmCVec ∧ ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) ∈ ℝ ∧ 0 ≀ (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))) ∧ 𝑧 ∈ 𝑋) β†’ ((normCVβ€˜π‘ˆ)β€˜((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) = ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
7450, 72, 64, 73syl3anc 1372 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((normCVβ€˜π‘ˆ)β€˜((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) = ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
75 rpcn 12984 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℝ+ β†’ 𝑦 ∈ β„‚)
7675ad2antlr 726 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ 𝑦 ∈ β„‚)
7754ad2antrl 727 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((normCVβ€˜π‘ˆ)β€˜π‘§) ∈ ℝ)
7877recnd 11242 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((normCVβ€˜π‘ˆ)β€˜π‘§) ∈ β„‚)
792, 56, 21nvz 29922 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘ˆ ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) β†’ (((normCVβ€˜π‘ˆ)β€˜π‘§) = 0 ↔ 𝑧 = (0vecβ€˜π‘ˆ)))
801, 79mpan 689 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ 𝑋 β†’ (((normCVβ€˜π‘ˆ)β€˜π‘§) = 0 ↔ 𝑧 = (0vecβ€˜π‘ˆ)))
8180necon3bid 2986 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ 𝑋 β†’ (((normCVβ€˜π‘ˆ)β€˜π‘§) β‰  0 ↔ 𝑧 β‰  (0vecβ€˜π‘ˆ)))
8281biimpar 479 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ)) β†’ ((normCVβ€˜π‘ˆ)β€˜π‘§) β‰  0)
8382adantl 483 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((normCVβ€˜π‘ˆ)β€˜π‘§) β‰  0)
8476, 78, 83divcan1d 11991 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)) = 𝑦)
8571, 74, 843eqtrd 2777 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((normCVβ€˜π‘ˆ)β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃)) = 𝑦)
86 rpre 12982 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ+ β†’ 𝑦 ∈ ℝ)
8786leidd 11780 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℝ+ β†’ 𝑦 ≀ 𝑦)
8887ad2antlr 726 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ 𝑦 ≀ 𝑦)
8985, 88eqbrtrd 5171 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((normCVβ€˜π‘ˆ)β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦)
902, 68nvgcl 29873 . . . . . . . . . . . . . . . . . 18 ((π‘ˆ ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧) ∈ 𝑋) β†’ (𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) ∈ 𝑋)
9150, 51, 67, 90syl3anc 1372 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) ∈ 𝑋)
92 fvoveq1 7432 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = (𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) β†’ ((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) = ((normCVβ€˜π‘ˆ)β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃)))
9392breq1d 5159 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = (𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) β†’ (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 ↔ ((normCVβ€˜π‘ˆ)β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦))
94 fvoveq1 7432 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = (𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) β†’ (π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) = (π‘‡β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃)))
9594fveq2d 6896 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = (𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) = ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃))))
9695breq1d 5159 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = (𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) β†’ (((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1 ↔ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1))
9793, 96imbi12d 345 . . . . . . . . . . . . . . . . . 18 (π‘₯ = (𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) β†’ ((((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1) ↔ (((normCVβ€˜π‘ˆ)β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1)))
9897rspcv 3609 . . . . . . . . . . . . . . . . 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 7086 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ 𝑋 β†’ (π‘‡β€˜π‘§) ∈ (BaseSetβ€˜π‘Š))
1027, 32nvcl 29914 . . . . . . . . . . . . . . . . . . 19 ((π‘Š ∈ NrmCVec ∧ (π‘‡β€˜π‘§) ∈ (BaseSetβ€˜π‘Š)) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ∈ ℝ)
1036, 101, 102sylancr 588 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ 𝑋 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ∈ ℝ)
104103ad2antrl 727 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ∈ ℝ)
105 1red 11215 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ 1 ∈ ℝ)
106104, 105, 62lemuldiv2d 13066 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) Β· ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§))) ≀ 1 ↔ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (1 / (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)))))
10770fveq2d 6896 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (π‘‡β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃)) = (π‘‡β€˜((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)))
108 eqid 2733 . . . . . . . . . . . . . . . . . . . . . . 23 ( ·𝑠OLD β€˜π‘Š) = ( ·𝑠OLD β€˜π‘Š)
1092, 65, 108, 26lnomul 30013 . . . . . . . . . . . . . . . . . . . . . 22 (((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) ∈ β„‚ ∧ 𝑧 ∈ 𝑋)) β†’ (π‘‡β€˜((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) = ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘Š)(π‘‡β€˜π‘§)))
11036, 109mpan 689 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) ∈ β„‚ ∧ 𝑧 ∈ 𝑋) β†’ (π‘‡β€˜((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) = ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘Š)(π‘‡β€˜π‘§)))
11163, 64, 110syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (π‘‡β€˜((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) = ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘Š)(π‘‡β€˜π‘§)))
112107, 111eqtrd 2773 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (π‘‡β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃)) = ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘Š)(π‘‡β€˜π‘§)))
113112fveq2d 6896 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃))) = ((normCVβ€˜π‘Š)β€˜((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘Š)(π‘‡β€˜π‘§))))
1146a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ π‘Š ∈ NrmCVec)
115101ad2antrl 727 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (π‘‡β€˜π‘§) ∈ (BaseSetβ€˜π‘Š))
1167, 108, 32nvsge0 29917 . . . . . . . . . . . . . . . . . . 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 2773 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃))) = ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) Β· ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§))))
119118breq1d 5159 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (((normCVβ€˜π‘Š)β€˜(π‘‡β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1 ↔ ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) Β· ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§))) ≀ 1))
120 rpcnne0 12992 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℝ+ β†’ (𝑦 ∈ β„‚ ∧ 𝑦 β‰  0))
121 rpcnne0 12992 . . . . . . . . . . . . . . . . . . . 20 (((normCVβ€˜π‘ˆ)β€˜π‘§) ∈ ℝ+ β†’ (((normCVβ€˜π‘ˆ)β€˜π‘§) ∈ β„‚ ∧ ((normCVβ€˜π‘ˆ)β€˜π‘§) β‰  0))
122 recdiv 11920 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 ∈ β„‚ ∧ 𝑦 β‰  0) ∧ (((normCVβ€˜π‘ˆ)β€˜π‘§) ∈ β„‚ ∧ ((normCVβ€˜π‘ˆ)β€˜π‘§) β‰  0)) β†’ (1 / (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))) = (((normCVβ€˜π‘ˆ)β€˜π‘§) / 𝑦))
123120, 121, 122syl2an 597 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℝ+ ∧ ((normCVβ€˜π‘ˆ)β€˜π‘§) ∈ ℝ+) β†’ (1 / (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))) = (((normCVβ€˜π‘ˆ)β€˜π‘§) / 𝑦))
12452, 60, 123syl2an 597 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (1 / (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))) = (((normCVβ€˜π‘ˆ)β€˜π‘§) / 𝑦))
125 rpne0 12990 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℝ+ β†’ 𝑦 β‰  0)
126125ad2antlr 726 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ 𝑦 β‰  0)
12778, 76, 126divrec2d 11994 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (((normCVβ€˜π‘ˆ)β€˜π‘§) / 𝑦) = ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
128124, 127eqtr2d 2774 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)) = (1 / (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))))
129128breq2d 5161 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)) ↔ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (1 / (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)))))
130106, 119, 1293bitr4d 311 . . . . . . . . . . . . . . 15 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (((normCVβ€˜π‘Š)β€˜(π‘‡β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1 ↔ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
131100, 130sylibd 238 . . . . . . . . . . . . . 14 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (βˆ€π‘₯ ∈ 𝑋 (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
132131anassrs 469 . . . . . . . . . . . . 13 ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ)) β†’ (βˆ€π‘₯ ∈ 𝑋 (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
133132imp 408 . . . . . . . . . . . 12 (((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ)) ∧ βˆ€π‘₯ ∈ 𝑋 (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1)) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
134133an32s 651 . . . . . . . . . . 11 (((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ βˆ€π‘₯ ∈ 𝑋 (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1)) ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ)) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
135 eqid 2733 . . . . . . . . . . . . . . . . . 18 (0vecβ€˜π‘Š) = (0vecβ€˜π‘Š)
1362, 7, 56, 135, 26lno0 30009 . . . . . . . . . . . . . . . . 17 ((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) β†’ (π‘‡β€˜(0vecβ€˜π‘ˆ)) = (0vecβ€˜π‘Š))
1371, 6, 25, 136mp3an 1462 . . . . . . . . . . . . . . . 16 (π‘‡β€˜(0vecβ€˜π‘ˆ)) = (0vecβ€˜π‘Š)
138137fveq2i 6895 . . . . . . . . . . . . . . 15 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(0vecβ€˜π‘ˆ))) = ((normCVβ€˜π‘Š)β€˜(0vecβ€˜π‘Š))
139135, 32nvz0 29921 . . . . . . . . . . . . . . . 16 (π‘Š ∈ NrmCVec β†’ ((normCVβ€˜π‘Š)β€˜(0vecβ€˜π‘Š)) = 0)
1406, 139ax-mp 5 . . . . . . . . . . . . . . 15 ((normCVβ€˜π‘Š)β€˜(0vecβ€˜π‘Š)) = 0
141138, 140eqtri 2761 . . . . . . . . . . . . . 14 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(0vecβ€˜π‘ˆ))) = 0
142 0le0 12313 . . . . . . . . . . . . . 14 0 ≀ 0
143141, 142eqbrtri 5170 . . . . . . . . . . . . 13 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(0vecβ€˜π‘ˆ))) ≀ 0
14417rpcnd 13018 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ+ β†’ (1 / 𝑦) ∈ β„‚)
14556, 21nvz0 29921 . . . . . . . . . . . . . . . . 17 (π‘ˆ ∈ NrmCVec β†’ ((normCVβ€˜π‘ˆ)β€˜(0vecβ€˜π‘ˆ)) = 0)
1461, 145ax-mp 5 . . . . . . . . . . . . . . . 16 ((normCVβ€˜π‘ˆ)β€˜(0vecβ€˜π‘ˆ)) = 0
147146oveq2i 7420 . . . . . . . . . . . . . . 15 ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜(0vecβ€˜π‘ˆ))) = ((1 / 𝑦) Β· 0)
148 mul01 11393 . . . . . . . . . . . . . . 15 ((1 / 𝑦) ∈ β„‚ β†’ ((1 / 𝑦) Β· 0) = 0)
149147, 148eqtrid 2785 . . . . . . . . . . . . . 14 ((1 / 𝑦) ∈ β„‚ β†’ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜(0vecβ€˜π‘ˆ))) = 0)
150144, 149syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ+ β†’ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜(0vecβ€˜π‘ˆ))) = 0)
151143, 150breqtrrid 5187 . . . . . . . . . . . 12 (𝑦 ∈ ℝ+ β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(0vecβ€˜π‘ˆ))) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜(0vecβ€˜π‘ˆ))))
152151ad3antlr 730 . . . . . . . . . . 11 ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ βˆ€π‘₯ ∈ 𝑋 (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1)) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(0vecβ€˜π‘ˆ))) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜(0vecβ€˜π‘ˆ))))
15349, 134, 152pm2.61ne 3028 . . . . . . . . . 10 ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ βˆ€π‘₯ ∈ 𝑋 (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1)) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
154153ex 414 . . . . . . . . 9 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) β†’ (βˆ€π‘₯ ∈ 𝑋 (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
155154ralrimdva 3155 . . . . . . . 8 ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) β†’ (βˆ€π‘₯ ∈ 𝑋 (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1) β†’ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
15645, 155sylbid 239 . . . . . . 7 ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) β†’ (βˆ€π‘₯ ∈ 𝑋 ((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1) β†’ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
157156imp 408 . . . . . 6 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ βˆ€π‘₯ ∈ 𝑋 ((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1)) β†’ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
158 oveq1 7416 . . . . . . . . 9 (π‘₯ = (1 / 𝑦) β†’ (π‘₯ Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)) = ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
159158breq2d 5161 . . . . . . . 8 (π‘₯ = (1 / 𝑦) β†’ (((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (π‘₯ Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)) ↔ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
160159ralbidv 3178 . . . . . . 7 (π‘₯ = (1 / 𝑦) β†’ (βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (π‘₯ Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)) ↔ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
161160rspcev 3613 . . . . . 6 (((1 / 𝑦) ∈ ℝ ∧ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (π‘₯ Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
16219, 157, 161syl2anc 585 . . . . 5 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ βˆ€π‘₯ ∈ 𝑋 ((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1)) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (π‘₯ Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
163162rexlimdva2 3158 . . . 4 (𝑃 ∈ 𝑋 β†’ (βˆƒπ‘¦ ∈ ℝ+ βˆ€π‘₯ ∈ 𝑋 ((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (π‘₯ Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
16416, 163syl5 34 . . 3 (𝑃 ∈ 𝑋 β†’ (𝑇 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (π‘₯ Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
165164imp 408 . 2 ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ)) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (π‘₯ Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
166 blocni.5 . . . 4 𝐡 = (π‘ˆ BLnOp π‘Š)
1672, 21, 32, 26, 166, 1, 6isblo3i 30054 . . 3 (𝑇 ∈ 𝐡 ↔ (𝑇 ∈ 𝐿 ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (π‘₯ Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
16825, 167mpbiran 708 . 2 (𝑇 ∈ 𝐡 ↔ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (π‘₯ Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
169165, 168sylibr 233 1 ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ)) β†’ 𝑇 ∈ 𝐡)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071   class class class wbr 5149  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409  β„‚cc 11108  β„cr 11109  0cc0 11110  1c1 11111   Β· cmul 11115   < clt 11248   ≀ cle 11249   / cdiv 11871  β„+crp 12974  βˆžMetcxmet 20929  MetOpencmopn 20934   CnP ccnp 22729  NrmCVeccnv 29837   +𝑣 cpv 29838  BaseSetcba 29839   ·𝑠OLD cns 29840  0veccn0v 29841   βˆ’π‘£ cnsb 29842  normCVcnmcv 29843  IndMetcims 29844   LnOp clno 29993   BLnOp cblo 29995
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188  ax-addf 11189  ax-mulf 11190
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-er 8703  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-sup 9437  df-inf 9438  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-n0 12473  df-z 12559  df-uz 12823  df-q 12933  df-rp 12975  df-xneg 13092  df-xadd 13093  df-xmul 13094  df-seq 13967  df-exp 14028  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-topgen 17389  df-psmet 20936  df-xmet 20937  df-met 20938  df-bl 20939  df-mopn 20940  df-top 22396  df-topon 22413  df-bases 22449  df-cnp 22732  df-grpo 29746  df-gid 29747  df-ginv 29748  df-gdiv 29749  df-ablo 29798  df-vc 29812  df-nv 29845  df-va 29848  df-ba 29849  df-sm 29850  df-0v 29851  df-vs 29852  df-nmcv 29853  df-ims 29854  df-lno 29997  df-nmoo 29998  df-blo 29999  df-0o 30000
This theorem is referenced by:  blocni  30058  lnocni  30059
  Copyright terms: Public domain W3C validator