Add lgseisenlem4 to iset.mm (#5010)

* add gsumzsubmcl to mmil.html

* add gsumsubgcl to mmil.html

* add gsumzaddlem , gsumzadd , gsumadd to mmil.html

* add gsummptfsadd to mmil.html

* add gsum split theorems to mmil.html

This is gsumzsplit , gsumsplit , gsumsplit2 , gsummptfidmsplit ,
gsummptfidmsplitres , gsummptfzsplit , and gsummptfzsplitl

* Add gsumfzconst to iset.mm

This is gsumconst from set.mm where the sum is indexed by consecutive
integers.  The proof is a new one by induction.

* add gsumconstf to mmil.html

* add gsummptshft to mmil.html

* Add gsumfzmhm to iset.mm

This is gsummhm from set.mm but where the sum is indexed by consecutive
integers.  The proof is from gsumfzval , seqhomog , and some monoid
theorems.

* Add gsumfzmhm2 to iset.mm

This is gsummhm2 from set.mm where the sum is indexed by
consecutive integers.  The proof is similar to the set.mm proof.

* Add gsumfzconstf to iset.mm

This is gsumconstf from set.mm but indexed by consecutive integers.  It
is also gsumfzconst from iset.mm but with a freeness hypothesis in place
of distinct variables.  The proof is similar to the set.mm proof of
gsumconstf .

* Add gsumfzsnfd to iset.mm

This is gsumsnfd from set.mm except that M has to be an integer.
Naming this similarly to the other gsumfz* theorems seems more
appealing than trying to use a different convention.

The proof is similar to the set.mm proof.

* Add gsumsnd , gsumsnf , gsumsn to mmil.html

* add gsumpr to mmil.html

* Add mpocnfldadd to iset.mm

Stated as in set.mm.  This is provided for compatibility with set.mm but
at least so far makes no effort to reduce axiom usage.  The proof is
based on the set.mm proof of cnfldadd .

* Add gsumfzfsum to iset.mm

This is gsumfsum from set.mm but where the sums are indexed by
consecutive integers.

As with the set.mm proof the proof separates the empty case (lemma
gsumfzfsumlem0 ) from the inhabited case (lemma gsumfzfsumlemm ,
here proved by induction which is perhaps simpler than trying to adapt
theorems like fsum3 ).

* Add submmulg to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with one small
change in extensible structure theorems.

* Add mpocnfldmul to iset.mm

Stated as in set.mm.  At least for now, this uses the same complex
number axioms as cnfldmul .  The proof is from ax-mulf and cnfldmul .

* Add cnfldui to iset.mm

This is similar to drngui from set.mm but for CCfld in particular, not
division rings in general.  The proof is a new one from crngunit ,
dvdsrd , and recapb .

* Add expghmap to iset.mm

This is expghm from set.mm with not equal changed to apart.  The proof
is basically the set.mm proof but needs changes of not equal to apart
and other intuitionizations on most steps.

* Add lgseisenlem4 to iset.mm

Stated as in set.mm.  The proof is basically the set.mm proof but
requires intuitionizing in many places for a variety of reasons.
Remove one sentence from the comment in set.mm (which seemed to be an
incorrect copy-paste from lgseisenlem2 ).

Author: jkingdon

iset-discouraged

@@ -70,6 +70,7 @@
 "ax-addf" is used by "addcncntop".
 "ax-addf" is used by "addex".
 "ax-addf" is used by "cnfldplusf".
+"ax-addf" is used by "mpocnfldadd".
 "ax-addrcl" is used by "readdcl".
 "ax-arch" is used by "arch".
 "ax-caucvg" is used by "caucvgre".
@@ -86,6 +87,7 @@
 "ax-mulass" is used by "mulass".
 "ax-mulcl" is used by "mulcl".
 "ax-mulcom" is used by "mulcom".
+"ax-mulf" is used by "mpocnfldmul".
 "ax-mulf" is used by "mulcncntop".
 "ax-mulf" is used by "mulex".
 "ax-mulrcl" is used by "remulcl".
@@ -354,7 +356,7 @@ New usage of "ax-1re" is discouraged (1 uses).
 New usage of "ax-addass" is discouraged (1 uses).
 New usage of "ax-addcl" is discouraged (1 uses).
 New usage of "ax-addcom" is discouraged (1 uses).
-New usage of "ax-addf" is discouraged (3 uses).
+New usage of "ax-addf" is discouraged (4 uses).
 New usage of "ax-addrcl" is discouraged (1 uses).
 New usage of "ax-arch" is discouraged (1 uses).
 New usage of "ax-caucvg" is discouraged (1 uses).
@@ -370,7 +372,7 @@ New usage of "ax-io" is discouraged (1 uses).
 New usage of "ax-mulass" is discouraged (1 uses).
 New usage of "ax-mulcl" is discouraged (1 uses).
 New usage of "ax-mulcom" is discouraged (1 uses).
-New usage of "ax-mulf" is discouraged (2 uses).
+New usage of "ax-mulf" is discouraged (3 uses).
 New usage of "ax-mulrcl" is discouraged (1 uses).
 New usage of "ax0id" is discouraged (0 uses).
 New usage of "ax0lt1" is discouraged (0 uses).