I think the discussion mentioned by Giovanni is about a different case -
it's about "definitions", i.e. hypotheses in the form $e |- A = ... $. For
example, look at ~ fmpt :
fmpt.1 $e |- F = ( x e. A |-> C ) $.
fmpt $p |- ( A. x e. A C e. B <-> F : A --> B ) $=
Here, "F" is defined as being (of the form) "( x e. A |-> C )", meaning
that "F" could be replacd (at least in principle) by "( x e. A |-> C )" in
the conclusion:
( A. x e. A C e. B <-> ( x e. A |-> C ) : A --> B )
No additional assumptions/prerequistes are requird (for which an antecedent
"ph ->" would be needed) in this case. Mario explains this in
https://groups.google.com/d/msg/metamath/V6QPBWzqvu4/jmY9kwLWCgAJ in more
detail.
The present case, however, shows a different kind of hypotheses often used
in deduction style (unfortunately not mentioned in the Metamath book or in
http://us.metamath.org/mpegif/mmnatded.html ). It is a variant of
hypotheses in the form $e |- ( x = y -> A = B ) $., often also enhanced by
the general antecedent ph: $e |- ( ( ph /\ x = y ) -> A = B ) $.
Examples:
gsumsn.b $e |- B = ( Base ` G ) $.
gsumsn.s $e |- ( k = M -> A = C ) $.
gsumsn $p |- ( ( G e. Mnd /\ M e. V /\ C e. B ) -> ( G gsum ( k e. { M
} |-> A ) ) = C ) $=
...
gsumsnd.s $e |- ( ( ph /\ k = M ) -> A = C ) $.
gsumsnd $p |- ( ph -> ( G gsum ( k e. { M } |-> A ) ) = C ) $=
These are abbreviations for substitutions (also called "implicit
substitutions"), which could be written also as explicit substitutions: [_
M / k ]_ A = C (see also ~ csbied ). In other words, you can think of A as
a class expression containing the setvar variable k, and B as a class
expression containing the class variable M, so that A equals B after the
substitution of k by M.
Example: replace M, A, C by the follwing expressions:
M := ( 2 + 5 )
A := ( k - 3 )
C := ( ( 2 + 5 ) - 3 )
Then ( k = M -> A = C ) is true.
In the case of ~ fsumshft mentioned by Olivier, j can be considered as
being contained in A (A usually depends on j, because the summation is over
j), and k can be considered as being contained in B (B usually depends on
k, because the summation is over k), and the conclusion holds if A equals B
after j is substituted by ( k - K ) within A.
Using explicit substitution the theorem ~ fsumshft
fsumshft.5 $e |- ( j = ( k - K ) -> A = B ) $.
fsumshft $p |- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M + K
) ... ( N + K ) ) B ) $=
could also be written as
fsumshft $p |- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M + K
) ... ( N + K ) ) [ ( k - K ) / j ] A ) $=
As a conclusion, the patterns $e |- ( x = y -> A = B ) $. or $e |- ( ( ph
/\ x = y ) -> A = B ) $. for hypotheses are also allowed for deduction
style theorems, and they could be considered as abbreviations for
substitutions.
>From my personal view I would recommend to use the pattern $e |- ( ( ph /\
x = y ) -> A = B ) $ only. Although this is not always necessary, it is
often convenient to have all assumptions/prerequistes provided by ph
available in a proof using such a theorem to show that A = B actually holds.
Alexander
On Monday, October 28, 2019 at 10:18:40 PM UTC+1, 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/5981cc46-d454-4e68-bd6e-440d6ec0fd5c%40googlegroups.com.
