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/CAFXXJStM7MyX9avDaeVfwnMBGHg9vvakUcy2bg5XFepS-0GHyQ%40mail.gmail.com.
