Find a better definition of df-gsum for iset.mm

[jkingdon]

Right now iset.mm has a gsum definition (copied from set.mm) but that is just to let a few other definitions not diverge too far from set.mm; iset.mm doesn't have any gsum related theorems so far.

This definition has many problems for iset.mm:

• it relies on decidability of whether structure elements are equal to the identity or not (in several places). Although this would be true of some realistic examples like ZZ, Z/nZ , or QQ, we also want group sums on real numbers and other sets which cannot have decidable equality.
• it relies on decidability of whether the index set is a range of integers.

Let's look at the cases handled by gsum in set.mm:

• "If A = (/) and G has an identity element, then the sum equals this identity." If A is finite, we can use https://us.metamath.org/ileuni/fin0or.html to decide whether we are in this case or not, and it likely can otherwise be handled as in set.mm
• "If A = ( M ... N ) and G is any magma, then the sum is the sum of the elements, evaluated left-to-right". Provided we have a way of replacing the if expression on dom f e. ran ... from the set.mm defiinition, this seems feasible.
• "If A is a finite set (or is nonzero for finitely many indices) . . ." Let's start with the "nonzero for finitely many indices" - that is either impossible or more trouble than it is worth - see the discussion of support at Define polynomials in iset.mm #4846 and the pages linked from there. So assuming we are just looking at the finite case, we get:
• "If A is a finite set and G is a commutative monoid, then the sum adds up these elements in some order". How useful is this case? Any finite set can be put into bijection with ( M ... N ) for some integers M,N so how important is it to build that into gsum? I don't know if it is possible to pull some trick like we have in https://us.metamath.org/ileuni/df-sumdc.html (in which two halves of the definition coincide for the part where they both make sense) but even if that is possible it is a lot of work to put into practice, so I'm not planning on jumping into that lightly.

I won't (yet) try to write out the exact definition which would try to handle the first two cases, but it seems like it would handle a lot of the ways gsum is used in set.mm. For example, if W e. Word (Base ` G ) then G gsum W would be of this form.

Any ideas of other definitions? Anything wrong or incomplete about the above?