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 > <http://www.google.com/url?q=http%3A%2F%2Fus2.metamath.org%2Fmpeuni%2Ffsumshftd.html&sa=D&sntz=1&usg=AFQjCNFb4jlynHzWN9mPYLXScFapS9OJWA> > > 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/4565a491-12d2-4ea5-8f1c-a884396d68bd%40googlegroups.com.
