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/fsumshftd.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/1b12ceed-ae8a-47c2-882b-08facbf37252%40googlegroups.com.
