Merge branch 'develop' of https://github.com/metamath/set.mm into av-…

…extstr4

changes-set.txt

@@ -94,8 +94,17 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+18-Nov-24 csbcog    [same]      moved from RP's mathbox to main set.mm
+18-Nov-24 csbwrecsg [same]      moved from ML's mathbox to main set.mm
+18-Nov-24 csbpredg  [same]      moved from ML's mathbox to main set.mm
+18-Nov-24 csbdif    [same]      moved from ML's mathbox to main set.mm
+18-Nov-24 df-wrecs  dfwrecsOLD  obsoleted
+18-Nov-24 dfwrecs2  df-wrecs    moved from BJ's mathbox to main set.mm and
+                                made the main definition
+16-Nov-24 rspcdvinvd rspcdv2    moved from SP's mathbox to main set.mm
 15-Nov-24 baseltedgf basendxltedgfndx 
 12-Nov-24 sseldi    sselid      compare to sselii or sseldd
+11-Nov-24 mpteq12da [same]      moved from GS's mathbox to main set.mm
  9-Nov-24 eqsb3     eqsb1
  9-Nov-24 eqsbc3    eqsbc1
  9-Nov-24 eqsbc3r   eqsbc2

mmil.raw.html

@@ -2198,6 +2198,11 @@
 ~ notnotsnex .</P></TD>
 </TR>
 
+<tr>
+  <td>prex</td>
+  <td>~ prexg</td>
+</tr>
+
 <TR>
   <TD>nssss</TD>
   <TD>~ nssssr</TD>
@@ -2673,7 +2678,7 @@
 
 <TR>
 <TD>iotaex</TD>
-<TD>~iotacl , ~ euiotaex </TD>
+<TD>~ iotacl , ~ euiotaex , ~ riotaexg</TD>
 </TR>
 
 <TR>
@@ -10224,6 +10229,145 @@
   are different without excluded middle).</TD>
 </TR>
 
+<tr>
+  <td>plusffval</td>
+  <td>~ plusffvalg</td>
+</tr>
+
+<tr>
+  <td>plusfval</td>
+  <td>~ plusfvalg</td>
+</tr>
+
+<tr>
+  <td>plusfeq</td>
+  <td>~ plusfeqg</td>
+</tr>
+
+<tr>
+  <td>plusffn</td>
+  <td>~ plusffng</td>
+</tr>
+
+<tr>
+  <td>issstrmgm</td>
+  <td><i>none</i></td>
+  <td>the set.mm proof uses ressbas2</td>
+</tr>
+
+<tr>
+  <td>mgm0b</td>
+  <td><i>none</i></td>
+  <td>should be provable if a ` O e. _V ` condition
+  is added.</td>
+</tr>
+
+<tr>
+  <td>opifismgm</td>
+  <td>~ opifismgmdc</td>
+</tr>
+
+<tr>
+  <td>grpidval</td>
+  <td>~ grpidvalg</td>
+</tr>
+
+<tr>
+  <td>grpidpropd</td>
+  <td>~ grpidpropdg</td>
+</tr>
+
+<tr>
+  <td>gsumvalx</td>
+  <td><i>none</i></td>
+  <td>Would seem to need ` DECID ran F C_ O ` and
+  ` DECID A e. ran ... ` conditions.  Also, probably
+  a closer look at how to express the finite sums
+  here and in ~ df-gsum (most likely would need to
+  define the tail end of the sequence to consist of
+  occurences of the identity, as we do in ~ df-sumdc
+  and ~ df-proddc ).
+  </td>
+</tr>
+
+<tr>
+  <td>gsumval</td>
+  <td><i>none</i></td>
+  <td>likely the same caveats as gsumvalx would apply</td>
+</tr>
+
+<tr>
+  <td>gsumpropd</td>
+  <td><i>none</i></td>
+  <td>the set.mm proof uses gsumvalx</td>
+</tr>
+
+<tr>
+  <td>gsumpropd2lem , gsumpropd2</td>
+  <td><i>none</i></td>
+  <td>the set.mm proof uses gsumvalx</td>
+</tr>
+
+<tr>
+  <td>gsummgmpropd</td>
+  <td><i>none</i></td>
+  <td>the set.mm proof uses gsumpropd2</td>
+</tr>
+
+<tr>
+  <td>gsumress</td>
+  <td><i>none</i></td>
+  <td>the set.mm proof uses gsumval</td>
+</tr>
+
+<tr>
+  <td>gsumval1</td>
+  <td><i>none</i></td>
+  <td>the set.mm proof uses gsumval</td>
+</tr>
+
+<tr>
+  <td>gsum0</td>
+  <td><i>none</i></td>
+  <td>would seem to need a ` G e. _V ` condition</td>
+</tr>
+
+<tr>
+  <td>gsumval2a</td>
+  <td><i>none</i></td>
+  <td>the set.mm proof uses gsumval</td>
+</tr>
+
+<tr>
+  <td>gsumval2</td>
+  <td><i>none</i></td>
+  <td>the set.mm proof uses several theorems we do not have</td>
+</tr>
+
+<tr>
+  <td>gsumsplit1r</td>
+  <td><i>none</i></td>
+  <td>the set.mm proof uses several theorems we do not have</td>
+</tr>
+
+<tr>
+  <td>gsumprval</td>
+  <td><i>none</i></td>
+  <td>the set.mm proof uses several theorems we do not have</td>
+</tr>
+
+<tr>
+  <td>gsumpr12val</td>
+  <td><i>none</i></td>
+  <td>the set.mm proof uses gsumprval</td>
+</tr>
+
+<tr>
+  <td>sgrp0b</td>
+  <td><i>none</i></td>
+  <td>the set.mm proof uses mgm0b</td>
+</tr>
+
 <tr>
   <td id="missing-df-cnfld">df-cnfld and all theorems using CCfld</td>
   <td><i>none</i></td>

mmnotes.txt

@@ -963,7 +963,7 @@ Mario Carneiro finished a major revision of set.mm. Here are his notes:
     fvunsn: eliminate D e. _V hypothesis
     caoprcld, caoprassg, caoprcomg: deduction form
     winafpi: dedth demonstration
-    avglt1, avglt2, avgle1, avgle2: average ordering theorem colleciton
+    avglt1, avglt2, avgle1, avgle2: average ordering theorem collection
     peano2fzr: recurring lemma
     fzfid: very common use due to deduction-form sum theorems
     seqcl2 thru seq1p: deduction form