add a few more polynomial theorems to iset.mm (#5030)

* add plymul0or to mmil.html

* add ofmulrt to mmil.html

* copy plyreres from set.mm to iset.mm

Author: jkingdon

iset.mm

@@ -179476,6 +179476,20 @@ theorem as stated here (although versions with additional conditions,
       EWRXAWSXB $.
   $}
 
+  ${
+    $d F a $.
+    $( Real-coefficient polynomials restrict to real functions.  (Contributed
+       by Stefan O'Rear, 16-Nov-2014.) $)
+    plyreres $p |- ( F e. ( Poly ` RR ) -> ( F |` RR ) : RR --> RR ) $=
+      ( va cr cply cfv wcel cres wfn crn wss wf cc plybss wb plyf fnssresb wceq
+      ffn adantl ccj 3syl mpbird cv wral wa recn ffvelcdm syl2an plyrecj sylan2
+      fvres cjre fveq2d cjrebd eqeltrd ralrimiva fnfvrnss syl2anc df-f sylanbrc
+      eqtrd ) ACDEFZACGZCHZVCICJZCCVCKVBVDCLJZCAMVBLLAKZALHVDVFNCAOZLLARLCAPUAU
+      BZVBVDBUCZVCEZCFZBCUDVEVIVBVLBCVBVJCFZUEZVKVJAEZCVMVKVOQVBVJCAUKSVNVOVBVG
+      VJLFZVOLFVMVHVJUFZLLVJAUGUHVNVOTEZVJTEZAEZVOVMVBVPVRVTQVQVJAUIUJVNVSVJAVM
+      VSVJQVBVJULSUMVAUNUOUPBCCVCUQURCCVCUSUT $.
+  $}
+
 
 $(
 #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#

mmil.raw.html

@@ -14405,6 +14405,18 @@
   specifies coefficients explicitly</td>
 </tr>
 
+<tr>
+  <td>plymul0or</td>
+  <td><i>none</i></td>
+  <td>presumably not possible for reasons analogous to mul0ord</td>
+</tr>
+
+<tr>
+  <td>ofmulrt</td>
+  <td><i>none</i></td>
+  <td>the set.mm proof uses mul0ord</td>
+</tr>
+
 <tr>
   <td>fta1</td>
   <td><i>none</i></td>