You're welcome. :) Norm On Wednesday, November 13, 2019 at 10:23:09 AM UTC-5, Olivier Binda wrote: > > Many thanks for this post, Norman. > > I am using it to prove fsumshftd from Mephistolus, by using fsumshft > > I tried by myself (but had a distinct problem while using fsumsht with [_ > / ]_ ... I understand now, why I need F/_ and not only distinct vars > theorems > So, I started studying your proof (it helps me grow in metamath), I > understood quite a few things along the way and I am really grateful > Many thanks for that answer. > :) > > Olivier > > > Le samedi 2 novembre 2019 00:33:58 UTC+1, Norman Megill a écrit : >> >> By using one less dummy variable, I found a shorter proof that might be >> easier to understand, updated at >> >> http://us2.metamath.org/mpeuni/fsumshftd.html >> >> To summarize the proof, we use csbeq1 at step 17 to eliminate the >> hypothesis fsumshft.5. This converts the implicit substitution to an >> explicit substitution version of fsumshft at step 18. Note that fsumshft >> requires $d j B, which is not satisfied when we substitute [_ ( k - K ) / j >> ]_ A for B. So to avoid a dv conflict, we use dummy variable w instead of >> j. We use cbvsumi at step 4 to change w in the fsumshft conclusion to j. >> Of particular interest is the use of csbied at step 22, which, using the >> new (weaker) hypothesis fsumshftd.5, gives us [_ ( k - K ) / j ]_ A = B to >> get rid of the explicit substitution on A and result in B. >> >> Norm >> >> On Friday, November 1, 2019 at 1:27:50 PM UTC-4, Norman Megill wrote: >>> >>> Getting back to your original question, we can prove fsumshft with your >>> modified (weaker) fsumshft.5 starting from directly from fsumshft with the >>> stronger fsumshft.5. I show a proof here: >>> >> >>> http://us2.metamath.org/mpeuni/fsumshftdOLD.html >>> >>> To summarize the proof, we use csbeq1 at step 15 to eliminate the >>> hypothesis fsumshft.5. This converts the implicit substitution to an >>> explicit substitution version of fsumshft at step 16. Next we use cbvsumi >>> at steps 18 and 25 to change the dummy variables x and y in the fsumshft >>> conclusion to j and k. Of particular interest is the use of sbcied at step >>> 30, which, using the new (weaker) hypothesis fsumshftd.5, results in [_ ( k >>> - K ) / j ]_ A = B to get rid of the explicit substitution on A and result >>> in B. >>> >>> The proof is somewhat long. Maybe someone can find a shorter proof or >>> devise a library theorem to simplify this conversion. But given its >>> current size, this technique probably shouldn't be used routinely just to >>> allow using fsumshftd.5 for things other than simple substitutions, unless >>> the size savings in the target theorem's proof compensates for the size of >>> the fsumshftd proof. >>> >>> Norm >>> >>> On Monday, October 28, 2019 at 5:18:40 PM UTC-4, Olivier Binda wrote: >>>> >>>> Why doesn't fsumshft.5 have a ph -> part like other hypotheses ? >>>> >>>> fsumshft.5 [image: |-] [image: (][image: j] [image: =] [image: (][image: >>>> k] [image: -] [image: K][image: )] [image: ->] [image: A] [image: =] >>>> [image: >>>> B][image: )] >>>> Is the same theorem with ( ph -> ( j = ( k-K ) -> A = B ) ) false ? or >>>> stupid ? or unnecessary ? >>>> >>>> It looks stronger to me as I probably cannot prove it easily from >>>> fsumshtf >>>> >>>> I am still grasping at all the subtleties of Metamath, so I may not >>>> understand something important here. >>>> >>>> Could someone please enlighten me ? >>>> >>>> Best regards, >>>> Olivier >>>> >>>
-- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/b5cc3310-30cc-422e-9db1-95f7c71cf513%40googlegroups.com.
