Add Poly to iset.mm (#5003)

* Add Poly and Xp to iset.mm

This is the syntax, df-ply , and df-idp .  Copied without change from
set.mm.

* Revise mmil.html entries for df-coe and df-dgr

This is to clarify how we approach the coefficients and degree of a
polynomial.

* add plyco0 to mmil.html

* Add plyval to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with a number of
changes for set existence.

* copy plybss from set.mm to iset.mm

* Add elply to iset.mm

This is copied from set.mm and although I ended up sending the proof
through mmj2 I didn't need to change anything.

* copy ifexg from set.mm to iset.mm

* Add ifex to iset.mm

Stated as in set.mm.  The proof is from ifexg .

* add elply2 to mmil.html

* copy plyun0 from set.mm to iset.mm

* Add plyf to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with one small
change for differences in finiteness.

* Add plyss to iset.mm

Stated as in set.mm.  I loaded and saved the proof in mmj2 but didn't
need to otherwise edit it.

* Add plyssc to iset.mm

Stated as in set.mm.  The proof is based on the set.mm proof but needs
to have some logic rearranged.

* copy elplyr from set.mm to iset.mm

* Add elplyd to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with a small change
to show one proposition is decidable.

* Add ply1term to iset.mm

Stated as in set.mm.  The proof, including for the lemma ply1termlem ,
is the set.mm proof with small changes for decidability and
finite set theorems.

* copy plypow from set.mm to iset.mm

* copy plyconst from set.mm to iset.mm

* Add df-0p and ne0p to mmil.html

* add ply0 to mmil.html

* Copy opabresid and mptresid from set.mm to iset.mm

This flips the two sides of the equality.

Update the five proofs which use mptresid .

This changed in set.mm in 2023 so this change is to get closer
alignment between set.mm and iset.mm.

* copy plyid from set.mm to iset.mm

* add plyeq0 to mmil.html

* add plypf1 to mmil.html

* copy mptima and mptimass from set.mm to iset.mm

* add rnmptc to mmil.html

* Add elply2 to iset.mm

Stated as in set.mm.  The proof is the set.mm proof except:

* a small change for set existence
* a rewrite of the part of the proof which had used plyco0 , to use
  theorems including mptima , fconstmpt , and rnxpm instead.
* proving decidability when working with if

* Add plyaddlem1 to iset.mm

Stated as in set.mm.  The proof is the set.mm proof except for changes
for differences in sum and maximum theorems.

* Add plymullem1 to iset.mm

Stated as in set.mm.  The proof is the set.mm theorem with changes for
differences in sum and finite set theorems.

* Add plyaddlem to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with one small
change to show that a proposition is decidable.

* Add plymullem to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with small changes
for differences in sum and integer range theorems.

* copy plyadd from set.mm to iset.mm

* copy plymul from set.mm to iset.mm

* copy plysub from set.mm to iset.mm

* copy plyaddcl from set.mm to iset.mm

* copy plymulcl from set.mm to iset.mm

* copy plysubcl from set.mm to iset.mm

* Wording fix to plyf comment

"The" -> "A"

Author: jkingdon

iset-discouraged

@@ -608,7 +608,7 @@ Proof modification of "findset" is discouraged (96 steps).
 Proof modification of "fnexALT" is discouraged (111 steps).
 Proof modification of "idALT" is discouraged (26 steps).
 Proof modification of "idi" is discouraged (1 steps).
-Proof modification of "idref" is discouraged (94 steps).
+Proof modification of "idref" is discouraged (97 steps).
 Proof modification of "infnninfOLD" is discouraged (127 steps).
 Proof modification of "nn0ge2m1nnALT" is discouraged (48 steps).
 Proof modification of "nnindALT" is discouraged (15 steps).