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.
