Theorems about magmas, semigroups and monoids (continued)

Subsection "Identity elements":
* ~grprinvlem, ~grprinvd, ~grpridd moved from subsection "Operations"
* ~lidrididd ~lidrideqd moved from AV's mathbox to main

Subsection "Iterated sums in a magma":
* ~gsumsplit1r moved from AV's mathbox to main

Subsection "Definition and basic properties of monoids":
*  ~mndbn0 moved from AV's mathbox to main
*  proofs of ~slmdbn0 , ~slmdsn0 in TA's mathbox shortened

Subsection "Iterated sums in a monoid":
* ~gsumsgrpccat moved from AV's mathbox to main
* proof of ~gsumccat shortened

Subsection "Group multiple operation":
* ~mulgnn0gsum, ~mulgnngsum moved from AV's mathbox to main

New subsection "Cyclic monoids and groups":
* ~cycsubgcl, ~cycsubgss, ~cycsubg, ~cycsubg2, ~cycsubg2cl, ~cycsubggend, ~cycsubgcld  moved from other places
* ~cycsubm ~cycsubmcl ~cycsubmel moved from AV's mathbox to main

New subsection header "Direct products (extension)":
* ~smndlsmidm, ~mndlsmidm moved from AV's mathbox to main
* proof of ~lsmidm shortened

Subsection "Abelian groups":
* new theorem ~invmod (variant of ~caovmo) added

Subsubsection "Group sum operation"
* ~gsumreidx, ~gsumxp2 moved from AV's mathbox to main
* ~gsumcom3, ~gsumcom3fi moved up from section "Matrix multiplication"

Miscellaneous:
* ~gcdmultiplez,  ~gcdmultiple moved up and proofs shortened
* Header for subsubsection "Definition and basic properties" of subsection "Simple groups" added
* Header for subsubsection "Convert operation laws using setvar variables to class notation" of subsection "Operations" added

changes-set.txt

@@ -81,6 +81,20 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+13-Jan-24 mndlsmidm [same]      moved from AV's mathbox to main set.mm
+13-Jan-24 smndlsmidm [same]     moved from AV's mathbox to main set.mm
+13-Jan-24 cycsubm   [same]      moved from AV's mathbox to main set.mm
+13-Jan-24 cycsubmcl [same]      moved from AV's mathbox to main set.mm
+13-Jan-24 cycsubmel [same]      moved from AV's mathbox to main set.mm
+13-Jan-24 mulgnn0gsum [same]    moved from AV's mathbox to main set.mm
+13-Jan-24 mulgnngsum [same]     moved from AV's mathbox to main set.mm
+13-Jan-24 gsumxp2   [same]      moved from AV's mathbox to main set.mm
+13-Jan-24 gsumreidx [same]      moved from AV's mathbox to main set.mm
+13-Jan-24 gsumsgrpccat [same]   moved from AV's mathbox to main set.mm
+13-Jan-24 gsumsplit1r [same]    moved from AV's mathbox to main set.mm
+13-Jan-24 mndbn0    [same]      moved from AV's mathbox to main set.mm
+13-Jan-24 lidrididd [same]      moved from AV's mathbox to main set.mm
+13-Jan-24 lidrideqd [same]      moved from AV's mathbox to main set.mm
  5-Jan-24 ---       ---         sections "Groups" and "Simple groups"
                                 moved from RR's mathbox to main set.mm
  5-Jan-24 rr-php2d  phpeqd      moved from RR's mathbox to main set.mm

discouraged

@@ -15266,6 +15266,8 @@ New usage of "fvsnOLD" is discouraged (0 uses).
 New usage of "fvsngOLD" is discouraged (0 uses).
 New usage of "fvsnun1OLD" is discouraged (0 uses).
 New usage of "fvsnun2OLD" is discouraged (0 uses).
+New usage of "gcdmultipleOLD" is discouraged (0 uses).
+New usage of "gcdmultiplezOLD" is discouraged (0 uses).
 New usage of "gen11" is discouraged (19 uses).
 New usage of "gen11nv" is discouraged (5 uses).
 New usage of "gen12" is discouraged (7 uses).
@@ -15349,6 +15351,7 @@ New usage of "grporndm" is discouraged (4 uses).
 New usage of "grposnOLD" is discouraged (1 uses).
 New usage of "grpplusgx" is discouraged (3 uses).
 New usage of "grpsubfvalALT" is discouraged (0 uses).
+New usage of "gsumccatOLD" is discouraged (0 uses).
 New usage of "gt-lt" is discouraged (0 uses).
 New usage of "gt-lth" is discouraged (1 uses).
 New usage of "gt0srpr" is discouraged (2 uses).
@@ -16105,6 +16108,7 @@ New usage of "lsatfixedN" is discouraged (1 uses).
 New usage of "lshpinN" is discouraged (0 uses).
 New usage of "lshpnel2N" is discouraged (0 uses).
 New usage of "lshpset2N" is discouraged (1 uses).
+New usage of "lsmidmOLD" is discouraged (0 uses).
 New usage of "ltaddnq" is discouraged (7 uses).
 New usage of "ltaddpr" is discouraged (5 uses).
 New usage of "ltaddpr2" is discouraged (1 uses).
@@ -18765,6 +18769,8 @@ Proof modification of "fvsnOLD" is discouraged (28 steps).
 Proof modification of "fvsngOLD" is discouraged (86 steps).
 Proof modification of "fvsnun1OLD" is discouraged (124 steps).
 Proof modification of "fvsnun2OLD" is discouraged (112 steps).
+Proof modification of "gcdmultipleOLD" is discouraged (348 steps).
+Proof modification of "gcdmultiplezOLD" is discouraged (230 steps).
 Proof modification of "gen11" is discouraged (27 steps).
 Proof modification of "gen11nv" is discouraged (14 steps).
 Proof modification of "gen12" is discouraged (16 steps).
@@ -18779,7 +18785,7 @@ Proof modification of "ghomlinOLD" is discouraged (161 steps).
 Proof modification of "grpinvfvalALT" is discouraged (161 steps).
 Proof modification of "grposnOLD" is discouraged (291 steps).
 Proof modification of "grpsubfvalALT" is discouraged (189 steps).
-Proof modification of "gsumccatNEW" is discouraged (310 steps).
+Proof modification of "gsumccatOLD" is discouraged (994 steps).
 Proof modification of "hadcomaOLD" is discouraged (37 steps).
 Proof modification of "hashge3el3dif" is discouraged (229 steps).
 Proof modification of "hba1-o" is discouraged (34 steps).
@@ -18872,7 +18878,7 @@ Proof modification of "latmassOLD" is discouraged (309 steps).
 Proof modification of "lcmftp" is discouraged (1057 steps).
 Proof modification of "lediv2aALT" is discouraged (264 steps).
 Proof modification of "leibpilem1OLD" is discouraged (254 steps).
-Proof modification of "lsmidmNEW" is discouraged (25 steps).
+Proof modification of "lsmidmOLD" is discouraged (116 steps).
 Proof modification of "luk-1" is discouraged (73 steps).
 Proof modification of "luk-2" is discouraged (52 steps).
 Proof modification of "luk-3" is discouraged (20 steps).