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/CAFXXJSukO3AKf_%3DqDnyQCQCoVqo5k4gGkcAPqXTTjq7%2BJc4mZw%40mail.gmail.com.
