fsumshft.5 doesn't have a "ph ->" antecedent because its purpose is simply to specify that B is a substitution instance of A. We sometimes call this "implicit substitution" as opposed to "explicit substitution", which would be B = [. ( k - K ) / j ]. A (or just using [. ( k - K ) / j ]. A in place of B instead of having a separate hypothesis).
Compare, for example, the implicit substitutions in first 4 hypotheses of the deduction form nn0indd. In order to use a theorem with implicit substitution, the proof usually eliminates the implicit substitution hypotheses with a chain of equality and/or biconditional theorems. The hypotheses are then completely eliminated, and ph is hardly ever needed to achieve that (if ever). So we rarely bother to add a ph antecedent. Offhand I can't recall a case where it would have helped in practice. The primary reason we tend to use implicit substitution rather than explicit substitution is to obtain shorter proofs. Note that (in this case) the variable j doesn't appear in B i.e. $d j B. If instead we used [. ( k - K ) / j ]. A, we might have to use say reximd in place of reximdv, requiring a chain of nf* theorems to eliminate the "not free in" hypotheses and maybe making the proof longer. Or, alternately, we could use intermediate dummy variables with cbv* + reximdv, also making the proof longer. There are also theorems like sbcie to convert implicit to explicit. Occasionally we have both versions of a theorem such as finds1 (implicit) vs. findes (explicit). Note that the latter hasn't found a use yet. 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/d0dff8da-3f16-4078-bd49-39f57448c77d%40googlegroups.com.
