MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  blocnilem Structured version   Visualization version   GIF version
Theorem blocnilem 30095
Description: Lemma for blocni 30096 and lnocni 30097. 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 29983 . . . . . 6 (π‘ˆ ∈ NrmCVec β†’ 𝐢 ∈ (∞Metβ€˜π‘‹))
51, 4ax-mp 5 . . . . 5 𝐢 ∈ (∞Metβ€˜π‘‹)
6 blocni.w . . . . . 6 π‘Š ∈ NrmCVec
7 eqid 2732 . . . . . . 7 (BaseSetβ€˜π‘Š) = (BaseSetβ€˜π‘Š)
8 blocni.d . . . . . . 7 𝐷 = (IndMetβ€˜π‘Š)
97, 8imsxmet 29983 . . . . . 6 (π‘Š ∈ NrmCVec β†’ 𝐷 ∈ (∞Metβ€˜(BaseSetβ€˜π‘Š)))
106, 9ax-mp 5 . . . . 5 𝐷 ∈ (∞Metβ€˜(BaseSetβ€˜π‘Š))
11 1rp 12980 . . . . . 6 1 ∈ ℝ+
12 blocni.j . . . . . . 7 𝐽 = (MetOpenβ€˜πΆ)
13 blocni.k . . . . . . 7 𝐾 = (MetOpenβ€˜π·)
1412, 13metcnpi3 24062 . . . . . 6 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝐷 ∈ (∞Metβ€˜(BaseSetβ€˜π‘Š))) ∧ (𝑇 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 1 ∈ ℝ+)) β†’ βˆƒπ‘¦ ∈ ℝ+ βˆ€π‘₯ ∈ 𝑋 ((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1))
1511, 14mpanr2 702 . . . . 5 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝐷 ∈ (∞Metβ€˜(BaseSetβ€˜π‘Š))) ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ)) β†’ βˆƒπ‘¦ ∈ ℝ+ βˆ€π‘₯ ∈ 𝑋 ((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1))
165, 10, 15mpanl12 700 . . . 4 (𝑇 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) β†’ βˆƒπ‘¦ ∈ ℝ+ βˆ€π‘₯ ∈ 𝑋 ((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1))
17 rpreccl 13002 . . . . . . . 8 (𝑦 ∈ ℝ+ β†’ (1 / 𝑦) ∈ ℝ+)
1817rpred 13018 . . . . . . 7 (𝑦 ∈ ℝ+ β†’ (1 / 𝑦) ∈ ℝ)
1918ad2antlr 725 . . . . . 6 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ βˆ€π‘₯ ∈ 𝑋 ((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1)) β†’ (1 / 𝑦) ∈ ℝ)
20 eqid 2732 . . . . . . . . . . . . . . 15 ( βˆ’π‘£ β€˜π‘ˆ) = ( βˆ’π‘£ β€˜π‘ˆ)
21 eqid 2732 . . . . . . . . . . . . . . 15 (normCVβ€˜π‘ˆ) = (normCVβ€˜π‘ˆ)
222, 20, 21, 3imsdval 29977 . . . . . . . . . . . . . 14 ((π‘ˆ ∈ NrmCVec ∧ π‘₯ ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ (π‘₯𝐢𝑃) = ((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)))
231, 22mp3an1 1448 . . . . . . . . . . . . 13 ((π‘₯ ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ (π‘₯𝐢𝑃) = ((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)))
2423breq1d 5158 . . . . . . . . . . . 12 ((π‘₯ ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ ((π‘₯𝐢𝑃) ≀ 𝑦 ↔ ((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦))
25 blocni.l . . . . . . . . . . . . . . . . 17 𝑇 ∈ 𝐿
26 blocni.4 . . . . . . . . . . . . . . . . . 18 𝐿 = (π‘ˆ LnOp π‘Š)
272, 7, 26lnof 30046 . . . . . . . . . . . . . . . . 17 ((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) β†’ 𝑇:π‘‹βŸΆ(BaseSetβ€˜π‘Š))
281, 6, 25, 27mp3an 1461 . . . . . . . . . . . . . . . 16 𝑇:π‘‹βŸΆ(BaseSetβ€˜π‘Š)
2928ffvelcdmi 7085 . . . . . . . . . . . . . . 15 (π‘₯ ∈ 𝑋 β†’ (π‘‡β€˜π‘₯) ∈ (BaseSetβ€˜π‘Š))
3028ffvelcdmi 7085 . . . . . . . . . . . . . . 15 (𝑃 ∈ 𝑋 β†’ (π‘‡β€˜π‘ƒ) ∈ (BaseSetβ€˜π‘Š))
31 eqid 2732 . . . . . . . . . . . . . . . . 17 ( βˆ’π‘£ β€˜π‘Š) = ( βˆ’π‘£ β€˜π‘Š)
32 eqid 2732 . . . . . . . . . . . . . . . . 17 (normCVβ€˜π‘Š) = (normCVβ€˜π‘Š)
337, 31, 32, 8imsdval 29977 . . . . . . . . . . . . . . . 16 ((π‘Š ∈ NrmCVec ∧ (π‘‡β€˜π‘₯) ∈ (BaseSetβ€˜π‘Š) ∧ (π‘‡β€˜π‘ƒ) ∈ (BaseSetβ€˜π‘Š)) β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) = ((normCVβ€˜π‘Š)β€˜((π‘‡β€˜π‘₯)( βˆ’π‘£ β€˜π‘Š)(π‘‡β€˜π‘ƒ))))
346, 33mp3an1 1448 . . . . . . . . . . . . . . 15 (((π‘‡β€˜π‘₯) ∈ (BaseSetβ€˜π‘Š) ∧ (π‘‡β€˜π‘ƒ) ∈ (BaseSetβ€˜π‘Š)) β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) = ((normCVβ€˜π‘Š)β€˜((π‘‡β€˜π‘₯)( βˆ’π‘£ β€˜π‘Š)(π‘‡β€˜π‘ƒ))))
3529, 30, 34syl2an 596 . . . . . . . . . . . . . 14 ((π‘₯ ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) = ((normCVβ€˜π‘Š)β€˜((π‘‡β€˜π‘₯)( βˆ’π‘£ β€˜π‘Š)(π‘‡β€˜π‘ƒ))))
361, 6, 253pm3.2i 1339 . . . . . . . . . . . . . . . 16 (π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ NrmCVec ∧ 𝑇 ∈ 𝐿)
372, 20, 31, 26lnosub 30050 . . . . . . . . . . . . . . . 16 (((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (π‘₯ ∈ 𝑋 ∧ 𝑃 ∈ 𝑋)) β†’ (π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) = ((π‘‡β€˜π‘₯)( βˆ’π‘£ β€˜π‘Š)(π‘‡β€˜π‘ƒ)))
3836, 37mpan 688 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ (π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) = ((π‘‡β€˜π‘₯)( βˆ’π‘£ β€˜π‘Š)(π‘‡β€˜π‘ƒ)))
3938fveq2d 6895 . . . . . . . . . . . . . 14 ((π‘₯ ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) = ((normCVβ€˜π‘Š)β€˜((π‘‡β€˜π‘₯)( βˆ’π‘£ β€˜π‘Š)(π‘‡β€˜π‘ƒ))))
4035, 39eqtr4d 2775 . . . . . . . . . . . . 13 ((π‘₯ ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) = ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))))
4140breq1d 5158 . . . . . . . . . . . 12 ((π‘₯ ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ (((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1 ↔ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1))
4224, 41imbi12d 344 . . . . . . . . . . 11 ((π‘₯ ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ (((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1) ↔ (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1)))
4342ancoms 459 . . . . . . . . . 10 ((𝑃 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋) β†’ (((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1) ↔ (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1)))
4443adantlr 713 . . . . . . . . 9 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ π‘₯ ∈ 𝑋) β†’ (((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1) ↔ (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1)))
4544ralbidva 3175 . . . . . . . 8 ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) β†’ (βˆ€π‘₯ ∈ 𝑋 ((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1) ↔ βˆ€π‘₯ ∈ 𝑋 (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1)))
46 2fveq3 6896 . . . . . . . . . . . 12 (𝑧 = (0vecβ€˜π‘ˆ) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) = ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(0vecβ€˜π‘ˆ))))
47 fveq2 6891 . . . . . . . . . . . . 13 (𝑧 = (0vecβ€˜π‘ˆ) β†’ ((normCVβ€˜π‘ˆ)β€˜π‘§) = ((normCVβ€˜π‘ˆ)β€˜(0vecβ€˜π‘ˆ)))
4847oveq2d 7427 . . . . . . . . . . . 12 (𝑧 = (0vecβ€˜π‘ˆ) β†’ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)) = ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜(0vecβ€˜π‘ˆ))))
4946, 48breq12d 5161 . . . . . . . . . . 11 (𝑧 = (0vecβ€˜π‘ˆ) β†’ (((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)) ↔ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(0vecβ€˜π‘ˆ))) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜(0vecβ€˜π‘ˆ)))))
501a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ π‘ˆ ∈ NrmCVec)
51 simpll 765 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ 𝑃 ∈ 𝑋)
52 simpr 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) β†’ 𝑦 ∈ ℝ+)
532, 21nvcl 29952 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘ˆ ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) β†’ ((normCVβ€˜π‘ˆ)β€˜π‘§) ∈ ℝ)
541, 53mpan 688 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ 𝑋 β†’ ((normCVβ€˜π‘ˆ)β€˜π‘§) ∈ ℝ)
5554adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ)) β†’ ((normCVβ€˜π‘ˆ)β€˜π‘§) ∈ ℝ)
56 eqid 2732 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (0vecβ€˜π‘ˆ) = (0vecβ€˜π‘ˆ)
572, 56, 21nvgt0 29965 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘ˆ ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) β†’ (𝑧 β‰  (0vecβ€˜π‘ˆ) ↔ 0 < ((normCVβ€˜π‘ˆ)β€˜π‘§)))
581, 57mpan 688 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ 𝑋 β†’ (𝑧 β‰  (0vecβ€˜π‘ˆ) ↔ 0 < ((normCVβ€˜π‘ˆ)β€˜π‘§)))
5958biimpa 477 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ)) β†’ 0 < ((normCVβ€˜π‘ˆ)β€˜π‘§))
6055, 59elrpd 13015 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ)) β†’ ((normCVβ€˜π‘ˆ)β€˜π‘§) ∈ ℝ+)
61 rpdivcl 13001 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ ℝ+ ∧ ((normCVβ€˜π‘ˆ)β€˜π‘§) ∈ ℝ+) β†’ (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) ∈ ℝ+)
6252, 60, 61syl2an 596 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) ∈ ℝ+)
6362rpcnd 13020 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) ∈ β„‚)
64 simprl 769 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ 𝑧 ∈ 𝑋)
65 eqid 2732 . . . . . . . . . . . . . . . . . . . . . 22 ( ·𝑠OLD β€˜π‘ˆ) = ( ·𝑠OLD β€˜π‘ˆ)
662, 65nvscl 29917 . . . . . . . . . . . . . . . . . . . . 21 ((π‘ˆ ∈ NrmCVec ∧ (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) ∈ β„‚ ∧ 𝑧 ∈ 𝑋) β†’ ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧) ∈ 𝑋)
6750, 63, 64, 66syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧) ∈ 𝑋)
68 eqid 2732 . . . . . . . . . . . . . . . . . . . . 21 ( +𝑣 β€˜π‘ˆ) = ( +𝑣 β€˜π‘ˆ)
692, 68, 20nvpncan2 29944 . . . . . . . . . . . . . . . . . . . 20 ((π‘ˆ ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧) ∈ 𝑋) β†’ ((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃) = ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))
7050, 51, 67, 69syl3anc 1371 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃) = ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))
7170fveq2d 6895 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((normCVβ€˜π‘ˆ)β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃)) = ((normCVβ€˜π‘ˆ)β€˜((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)))
7262rprege0d 13025 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) ∈ ℝ ∧ 0 ≀ (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))))
732, 65, 21nvsge0 29955 . . . . . . . . . . . . . . . . . . 19 ((π‘ˆ ∈ NrmCVec ∧ ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) ∈ ℝ ∧ 0 ≀ (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))) ∧ 𝑧 ∈ 𝑋) β†’ ((normCVβ€˜π‘ˆ)β€˜((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) = ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
7450, 72, 64, 73syl3anc 1371 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((normCVβ€˜π‘ˆ)β€˜((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) = ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
75 rpcn 12986 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℝ+ β†’ 𝑦 ∈ β„‚)
7675ad2antlr 725 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ 𝑦 ∈ β„‚)
7754ad2antrl 726 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((normCVβ€˜π‘ˆ)β€˜π‘§) ∈ ℝ)
7877recnd 11244 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((normCVβ€˜π‘ˆ)β€˜π‘§) ∈ β„‚)
792, 56, 21nvz 29960 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘ˆ ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) β†’ (((normCVβ€˜π‘ˆ)β€˜π‘§) = 0 ↔ 𝑧 = (0vecβ€˜π‘ˆ)))
801, 79mpan 688 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ 𝑋 β†’ (((normCVβ€˜π‘ˆ)β€˜π‘§) = 0 ↔ 𝑧 = (0vecβ€˜π‘ˆ)))
8180necon3bid 2985 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ 𝑋 β†’ (((normCVβ€˜π‘ˆ)β€˜π‘§) β‰  0 ↔ 𝑧 β‰  (0vecβ€˜π‘ˆ)))
8281biimpar 478 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ)) β†’ ((normCVβ€˜π‘ˆ)β€˜π‘§) β‰  0)
8382adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((normCVβ€˜π‘ˆ)β€˜π‘§) β‰  0)
8476, 78, 83divcan1d 11993 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)) = 𝑦)
8571, 74, 843eqtrd 2776 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((normCVβ€˜π‘ˆ)β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃)) = 𝑦)
86 rpre 12984 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ+ β†’ 𝑦 ∈ ℝ)
8786leidd 11782 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℝ+ β†’ 𝑦 ≀ 𝑦)
8887ad2antlr 725 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ 𝑦 ≀ 𝑦)
8985, 88eqbrtrd 5170 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((normCVβ€˜π‘ˆ)β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦)
902, 68nvgcl 29911 . . . . . . . . . . . . . . . . . 18 ((π‘ˆ ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧) ∈ 𝑋) β†’ (𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) ∈ 𝑋)
9150, 51, 67, 90syl3anc 1371 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) ∈ 𝑋)
92 fvoveq1 7434 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = (𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) β†’ ((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) = ((normCVβ€˜π‘ˆ)β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃)))
9392breq1d 5158 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = (𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) β†’ (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 ↔ ((normCVβ€˜π‘ˆ)β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦))
94 fvoveq1 7434 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = (𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) β†’ (π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) = (π‘‡β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃)))
9594fveq2d 6895 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = (𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) = ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃))))
9695breq1d 5158 . . . . . . . . . . . . . . . . . . 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 3608 . . . . . . . . . . . . . . . . 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 7085 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ 𝑋 β†’ (π‘‡β€˜π‘§) ∈ (BaseSetβ€˜π‘Š))
1027, 32nvcl 29952 . . . . . . . . . . . . . . . . . . 19 ((π‘Š ∈ NrmCVec ∧ (π‘‡β€˜π‘§) ∈ (BaseSetβ€˜π‘Š)) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ∈ ℝ)
1036, 101, 102sylancr 587 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ 𝑋 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ∈ ℝ)
104103ad2antrl 726 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ∈ ℝ)
105 1red 11217 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ 1 ∈ ℝ)
106104, 105, 62lemuldiv2d 13068 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) Β· ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§))) ≀ 1 ↔ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (1 / (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)))))
10770fveq2d 6895 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (π‘‡β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃)) = (π‘‡β€˜((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)))
108 eqid 2732 . . . . . . . . . . . . . . . . . . . . . . 23 ( ·𝑠OLD β€˜π‘Š) = ( ·𝑠OLD β€˜π‘Š)
1092, 65, 108, 26lnomul 30051 . . . . . . . . . . . . . . . . . . . . . 22 (((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) ∈ β„‚ ∧ 𝑧 ∈ 𝑋)) β†’ (π‘‡β€˜((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) = ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘Š)(π‘‡β€˜π‘§)))
11036, 109mpan 688 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) ∈ β„‚ ∧ 𝑧 ∈ 𝑋) β†’ (π‘‡β€˜((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) = ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘Š)(π‘‡β€˜π‘§)))
11163, 64, 110syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (π‘‡β€˜((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧)) = ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘Š)(π‘‡β€˜π‘§)))
112107, 111eqtrd 2772 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (π‘‡β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃)) = ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘Š)(π‘‡β€˜π‘§)))
113112fveq2d 6895 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃))) = ((normCVβ€˜π‘Š)β€˜((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘Š)(π‘‡β€˜π‘§))))
1146a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ π‘Š ∈ NrmCVec)
115101ad2antrl 726 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (π‘‡β€˜π‘§) ∈ (BaseSetβ€˜π‘Š))
1167, 108, 32nvsge0 29955 . . . . . . . . . . . . . . . . . . 19 ((π‘Š ∈ NrmCVec ∧ ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) ∈ ℝ ∧ 0 ≀ (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))) ∧ (π‘‡β€˜π‘§) ∈ (BaseSetβ€˜π‘Š)) β†’ ((normCVβ€˜π‘Š)β€˜((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘Š)(π‘‡β€˜π‘§))) = ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) Β· ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§))))
117114, 72, 115, 116syl3anc 1371 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((normCVβ€˜π‘Š)β€˜((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘Š)(π‘‡β€˜π‘§))) = ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) Β· ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§))))
118113, 117eqtrd 2772 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃))) = ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) Β· ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§))))
119118breq1d 5158 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (((normCVβ€˜π‘Š)β€˜(π‘‡β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1 ↔ ((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)) Β· ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§))) ≀ 1))
120 rpcnne0 12994 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℝ+ β†’ (𝑦 ∈ β„‚ ∧ 𝑦 β‰  0))
121 rpcnne0 12994 . . . . . . . . . . . . . . . . . . . 20 (((normCVβ€˜π‘ˆ)β€˜π‘§) ∈ ℝ+ β†’ (((normCVβ€˜π‘ˆ)β€˜π‘§) ∈ β„‚ ∧ ((normCVβ€˜π‘ˆ)β€˜π‘§) β‰  0))
122 recdiv 11922 . . . . . . . . . . . . . . . . . . . 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 12992 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℝ+ β†’ 𝑦 β‰  0)
126125ad2antlr 725 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ 𝑦 β‰  0)
12778, 76, 126divrec2d 11996 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (((normCVβ€˜π‘ˆ)β€˜π‘§) / 𝑦) = ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
128124, 127eqtr2d 2773 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)) = (1 / (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))))
129128breq2d 5160 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)) ↔ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (1 / (𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§)))))
130106, 119, 1293bitr4d 310 . . . . . . . . . . . . . . 15 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (((normCVβ€˜π‘Š)β€˜(π‘‡β€˜((𝑃( +𝑣 β€˜π‘ˆ)((𝑦 / ((normCVβ€˜π‘ˆ)β€˜π‘§))( ·𝑠OLD β€˜π‘ˆ)𝑧))( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1 ↔ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
131100, 130sylibd 238 . . . . . . . . . . . . . 14 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ))) β†’ (βˆ€π‘₯ ∈ 𝑋 (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
132131anassrs 468 . . . . . . . . . . . . 13 ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ)) β†’ (βˆ€π‘₯ ∈ 𝑋 (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
133132imp 407 . . . . . . . . . . . 12 (((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ)) ∧ βˆ€π‘₯ ∈ 𝑋 (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1)) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
134133an32s 650 . . . . . . . . . . 11 (((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ βˆ€π‘₯ ∈ 𝑋 (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1)) ∧ 𝑧 β‰  (0vecβ€˜π‘ˆ)) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
135 eqid 2732 . . . . . . . . . . . . . . . . . 18 (0vecβ€˜π‘Š) = (0vecβ€˜π‘Š)
1362, 7, 56, 135, 26lno0 30047 . . . . . . . . . . . . . . . . 17 ((π‘ˆ ∈ NrmCVec ∧ π‘Š ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) β†’ (π‘‡β€˜(0vecβ€˜π‘ˆ)) = (0vecβ€˜π‘Š))
1371, 6, 25, 136mp3an 1461 . . . . . . . . . . . . . . . 16 (π‘‡β€˜(0vecβ€˜π‘ˆ)) = (0vecβ€˜π‘Š)
138137fveq2i 6894 . . . . . . . . . . . . . . 15 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(0vecβ€˜π‘ˆ))) = ((normCVβ€˜π‘Š)β€˜(0vecβ€˜π‘Š))
139135, 32nvz0 29959 . . . . . . . . . . . . . . . 16 (π‘Š ∈ NrmCVec β†’ ((normCVβ€˜π‘Š)β€˜(0vecβ€˜π‘Š)) = 0)
1406, 139ax-mp 5 . . . . . . . . . . . . . . 15 ((normCVβ€˜π‘Š)β€˜(0vecβ€˜π‘Š)) = 0
141138, 140eqtri 2760 . . . . . . . . . . . . . 14 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(0vecβ€˜π‘ˆ))) = 0
142 0le0 12315 . . . . . . . . . . . . . 14 0 ≀ 0
143141, 142eqbrtri 5169 . . . . . . . . . . . . 13 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(0vecβ€˜π‘ˆ))) ≀ 0
14417rpcnd 13020 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ+ β†’ (1 / 𝑦) ∈ β„‚)
14556, 21nvz0 29959 . . . . . . . . . . . . . . . . 17 (π‘ˆ ∈ NrmCVec β†’ ((normCVβ€˜π‘ˆ)β€˜(0vecβ€˜π‘ˆ)) = 0)
1461, 145ax-mp 5 . . . . . . . . . . . . . . . 16 ((normCVβ€˜π‘ˆ)β€˜(0vecβ€˜π‘ˆ)) = 0
147146oveq2i 7422 . . . . . . . . . . . . . . 15 ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜(0vecβ€˜π‘ˆ))) = ((1 / 𝑦) Β· 0)
148 mul01 11395 . . . . . . . . . . . . . . 15 ((1 / 𝑦) ∈ β„‚ β†’ ((1 / 𝑦) Β· 0) = 0)
149147, 148eqtrid 2784 . . . . . . . . . . . . . 14 ((1 / 𝑦) ∈ β„‚ β†’ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜(0vecβ€˜π‘ˆ))) = 0)
150144, 149syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ+ β†’ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜(0vecβ€˜π‘ˆ))) = 0)
151143, 150breqtrrid 5186 . . . . . . . . . . . 12 (𝑦 ∈ ℝ+ β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(0vecβ€˜π‘ˆ))) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜(0vecβ€˜π‘ˆ))))
152151ad3antlr 729 . . . . . . . . . . 11 ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ βˆ€π‘₯ ∈ 𝑋 (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1)) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(0vecβ€˜π‘ˆ))) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜(0vecβ€˜π‘ˆ))))
15349, 134, 152pm2.61ne 3027 . . . . . . . . . 10 ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ βˆ€π‘₯ ∈ 𝑋 (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1)) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
154153ex 413 . . . . . . . . 9 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) β†’ (βˆ€π‘₯ ∈ 𝑋 (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1) β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
155154ralrimdva 3154 . . . . . . . 8 ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) β†’ (βˆ€π‘₯ ∈ 𝑋 (((normCVβ€˜π‘ˆ)β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃)) ≀ 𝑦 β†’ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜(π‘₯( βˆ’π‘£ β€˜π‘ˆ)𝑃))) ≀ 1) β†’ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
15645, 155sylbid 239 . . . . . . 7 ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) β†’ (βˆ€π‘₯ ∈ 𝑋 ((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1) β†’ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
157156imp 407 . . . . . 6 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ βˆ€π‘₯ ∈ 𝑋 ((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1)) β†’ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
158 oveq1 7418 . . . . . . . . 9 (π‘₯ = (1 / 𝑦) β†’ (π‘₯ Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)) = ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
159158breq2d 5160 . . . . . . . 8 (π‘₯ = (1 / 𝑦) β†’ (((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (π‘₯ Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)) ↔ ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
160159ralbidv 3177 . . . . . . 7 (π‘₯ = (1 / 𝑦) β†’ (βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (π‘₯ Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)) ↔ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
161160rspcev 3612 . . . . . 6 (((1 / 𝑦) ∈ ℝ ∧ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ ((1 / 𝑦) Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (π‘₯ Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
16219, 157, 161syl2anc 584 . . . . 5 (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ βˆ€π‘₯ ∈ 𝑋 ((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1)) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (π‘₯ Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
163162rexlimdva2 3157 . . . 4 (𝑃 ∈ 𝑋 β†’ (βˆƒπ‘¦ ∈ ℝ+ βˆ€π‘₯ ∈ 𝑋 ((π‘₯𝐢𝑃) ≀ 𝑦 β†’ ((π‘‡β€˜π‘₯)𝐷(π‘‡β€˜π‘ƒ)) ≀ 1) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (π‘₯ Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
16416, 163syl5 34 . . 3 (𝑃 ∈ 𝑋 β†’ (𝑇 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (π‘₯ Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
165164imp 407 . 2 ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ)) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (π‘₯ Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
166 blocni.5 . . . 4 𝐡 = (π‘ˆ BLnOp π‘Š)
1672, 21, 32, 26, 166, 1, 6isblo3i 30092 . . 3 (𝑇 ∈ 𝐡 ↔ (𝑇 ∈ 𝐿 ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (π‘₯ Β· ((normCVβ€˜π‘ˆ)β€˜π‘§))))
16825, 167mpbiran 707 . 2 (𝑇 ∈ 𝐡 ↔ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ 𝑋 ((normCVβ€˜π‘Š)β€˜(π‘‡β€˜π‘§)) ≀ (π‘₯ Β· ((normCVβ€˜π‘ˆ)β€˜π‘§)))
169165, 168sylibr 233 1 ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ)) β†’ 𝑇 ∈ 𝐡)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070   class class class wbr 5148  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7411  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113   Β· cmul 11117   < clt 11250   ≀ cle 11251   / cdiv 11873  β„+crp 12976  βˆžMetcxmet 20935  MetOpencmopn 20940   CnP ccnp 22736  NrmCVeccnv 29875   +𝑣 cpv 29876  BaseSetcba 29877   ·𝑠OLD cns 29878  0veccn0v 29879   βˆ’π‘£ cnsb 29880  normCVcnmcv 29881  IndMetcims 29882   LnOp clno 30031   BLnOp cblo 30033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191  ax-mulf 11192
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-sup 9439  df-inf 9440  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-3 12278  df-n0 12475  df-z 12561  df-uz 12825  df-q 12935  df-rp 12977  df-xneg 13094  df-xadd 13095  df-xmul 13096  df-seq 13969  df-exp 14030  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-topgen 17391  df-psmet 20942  df-xmet 20943  df-met 20944  df-bl 20945  df-mopn 20946  df-top 22403  df-topon 22420  df-bases 22456  df-cnp 22739  df-grpo 29784  df-gid 29785  df-ginv 29786  df-gdiv 29787  df-ablo 29836  df-vc 29850  df-nv 29883  df-va 29886  df-ba 29887  df-sm 29888  df-0v 29889  df-vs 29890  df-nmcv 29891  df-ims 29892  df-lno 30035  df-nmoo 30036  df-blo 30037  df-0o 30038
This theorem is referenced by:  blocni  30096  lnocni  30097
  Copyright terms: Public domain W3C validator