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/07055492-46da-43a2-a8dd-87d05667e0d7%40googlegroups.com.
