Intuitionize SRing (#4522)

* Add SRing to iset.mm

This is the syntax and df-srg .  Copied without change from set.mm.

* copy sbceqbid from set.mm to iset.mm

* Add issrg to iset.mm

Stated as in set.mm.  The proof needs intuitionizing at most steps but
follows the set.mm proof closely.

* copy srgcmn and srgmnd from set.mm to iset.mm

* copy srgmgp from set.mm to iset.mm

* copy srgi from set.mm to iset.mm

* Add srgcl to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is
basically the set.mm proof.

* Add srgass to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is based
on the set.mm proof.

* Add srgideu to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is similar
to the set.mm proof.

* copy srgfcl from set.mm to iset.mm

* copy srgdi and srgdir from set.mm to iset.mm

* Add srgidcl to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is
basically the set.mm proof.

* copy srg0cl from set.mm to iset.mm

* Add srgidmlem to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is
basically the set.mm proof.

* copy srglidm and srgridm from set.mm to iset.mm

* Add issrgid to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is based
on the set.mm proof.

* copy srgacl and srgcom from set.mm to iset.mm

* copy simprld and simprrd from set.mm to iset.mm

* copy srgrz and srglz from set.mm to iset.mm

* copy srgisid from set.mm to iset.mm

* Add srg1zr to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is
basically the set.mm proof.

* copy srgen1zr from set.mm to iset.mm

* copy srgmulgass from set.mm to iset.mm

* Add srgpcomp to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is
basically the set.mm proof.

* Add srgpcompp to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is
basically the set.mm proof.

* Add srgpcomppsc to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is
basically the set.mm proof.

* Add srglmhm to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is
basically the set.mm proof.

* Add srgrmhm to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is
basically the set.mm proof.

* Add function support theorems to mmil.html

This is df-supp , df-fsupp , srgsummulcr , and sgsummulcl .

* Add srg1expzeq1 to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is
basically the set.mm proof.

* Add srgbinom , csrgbinom to mmil.html

* Revise df-srg comment in set.mm and iset.mmm

Be more clear when we compare the definition of SRing and Ring .
Wording suggested by tirix .

* Rename srgi to srgdilem

This is in set.mm and iset.mm

changes-set.txt

@@ -92,6 +92,7 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+ 3-Jan-25 srgi      srgdilem
  2-Jan-25 pr2nelem  enpr2
 28-Dec-24 fovrnd    fovcdmd
 28-Dec-24 fovrnda   fovcdmda