I am at a more basic level than what you are trying to address. My goal is
to learn how to prove theorems in metamath.
My current task is to do the follow: given B = { x | ph }, how would I
prove that A e. B. This is beginning level stuff.
I see that there is theorem elab2g that would be useful: I just need to
show the following: x = A -> ( ph <-> ps )
For substitution: df-sb: [t/x] phi <-> Ay ( y = t -> Ax ( x = y -> phi ))
I find this more intuitive: sb5 |- ( [. y / x ]. ph <-> E. x ( x = y /\ ph
)
Since I was having trouble with proving things with the substitution
notation, I was trying to see if I could get by without using it.
Again, I understand that the substitution notation is working at a higher
conceptual level. But, I am trying to learn that conceptual level.
My original question was whether the definition of Mgm required the
substitution notation. Your answer was that it was not required. Also, my
revised definition would not produce problems later on.
On Thursday, October 12, 2023 at 12:15:24 AM UTC-5 [email protected] wrote:
> Usually we prioritize minimizing the length of the definition (number of
> symbols) over the length of the extraction theorem, because the former is
> an axiom and the latter is not.
>
> On Thu, Oct 12, 2023 at 12:46 AM [email protected] <[email protected]>
> wrote:
>
>> You say that the definitions are the same, but to me "substitution" needs
>> to be proved in a roundabout way: that is, it is not just substituting "(
>> Base ` g )" for "b".
>>
>> The theorem ismgm that immediately follows the definition for Mgm
>> requires 19 steps, whereas only 8 steps are needed for the revised
>> definition.
>>
>> I guess you answered my question that the revised definition is valid.
>>
>>
>>
>> On Wednesday, October 11, 2023 at 11:11:22 PM UTC-5 [email protected]
>> wrote:
>>
>>> Those two definitions are the same except you have removed the
>>> substitutions b := ( Base ` g ) and o := ( +g ` g ) . The substitutions are
>>> there to make the definition more readable (and usually shorter, although
>>> it might be a wash in a short definition like this one). For a more
>>> elaborate example check out https://us.metamath.org/mpeuni/df-lmod.html
>>> .
>>>
>>> On Wed, Oct 11, 2023 at 11:38 PM [email protected] <[email protected]>
>>> wrote:
>>>
>>>> The given definition of magma is:
>>>>
>>>> df-mgm |- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x
>>>> e. b A. y e. b ( x o y ) e. b }
>>>>
>>>>
>>>> Would it be ok to define magma as follows:
>>>>
>>>> df-mgm |- Mgm = { g | A. x e. ( Base ` g ) A. y e. ( Base ` g ) ( x (
>>>> +g ` g ) y ) e. ( Base ` g ) }
>>>>
>>>> If so, what problems would result ?
>>>>
>>>> In other words, why was the given definition chosen over the more
>>>> explicit definition ?
>>>>
>>>> --
>>>> 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/3e26ed0a-5b15-4c29-adf5-434fb591eb96n%40googlegroups.com
>>>>
>>>> <https://groups.google.com/d/msgid/metamath/3e26ed0a-5b15-4c29-adf5-434fb591eb96n%40googlegroups.com?utm_medium=email&utm_source=footer>
>>>> .
>>>>
>>> --
>> 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/726a9570-1c6f-47ea-86af-ba553f89690fn%40googlegroups.com
>>
>> <https://groups.google.com/d/msgid/metamath/726a9570-1c6f-47ea-86af-ba553f89690fn%40googlegroups.com?utm_medium=email&utm_source=footer>
>> .
>>
>
--
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/6973d699-2ba3-4d27-9a19-cdc347b58cd1n%40googlegroups.com.
