Add mulGrp to iset.mm

iset-discouraged

@@ -107,8 +107,11 @@
 "basendx" is used by "2stropg".
 "basendx" is used by "2strstr1g".
 "basendx" is used by "2strstrg".
+"basendx" is used by "basendxltdsndx".
+"basendx" is used by "basendxlttsetndx".
 "basendx" is used by "lmodstrd".
 "basendx" is used by "rngstrg".
+"basendx" is used by "scandxnbasendx".
 "basendx" is used by "setsmsbasg".
 "basendx" is used by "topgrpstrd".
 "bj-axemptylem" is used by "bj-axempty".
@@ -364,7 +367,7 @@ New usage of "axpre-suploc" is discouraged (0 uses).
 New usage of "axprecex" is discouraged (2 uses).
 New usage of "axresscn" is discouraged (4 uses).
 New usage of "axrnegex" is discouraged (0 uses).
-New usage of "basendx" is discouraged (9 uses).
+New usage of "basendx" is discouraged (12 uses).
 New usage of "baseval" is discouraged (0 uses).
 New usage of "bdcnulALT" is discouraged (0 uses).
 New usage of "bdnthALT" is discouraged (0 uses).

iset.mm

@@ -142848,6 +142848,25 @@ could not be used in an extensible structure (slots must be positive
   scaslid $p |- ( Scalar = Slot ( Scalar ` ndx ) /\ ( Scalar ` ndx ) e. NN ) $=
     ( csca c5 df-sca 5nn ndxslid ) ABCDE $.
 
+  $( The slot for the scalar is not the slot for the base set in an extensible
+     structure.  (Contributed by AV, 21-Oct-2024.) $)
+  scandxnbasendx $p |- ( Scalar ` ndx ) =/= ( Base ` ndx ) $=
+    ( cnx csca cfv cbs wne c5 c1 1re 1lt5 gtneii scandx basendx neeq12i mpbir )
+    ABCZADCZEFGEGFHIJOFPGKLMN $.
+
+  $( The slot for the scalar field is not the slot for the group operation in
+     an extensible structure.  (Contributed by AV, 18-Oct-2024.) $)
+  scandxnplusgndx $p |- ( Scalar ` ndx ) =/= ( +g ` ndx ) $=
+    ( cnx csca cfv cplusg wne c5 2re 2lt5 gtneii scandx plusgndx neeq12i mpbir
+    c2 ) ABCZADCZEFNENFGHIOFPNJKLM $.
+
+  $( The slot for the scalar field is not the slot for the ring
+     (multiplication) operation in an extensible structure.  (Contributed by
+     AV, 29-Oct-2024.) $)
+  scandxnmulrndx $p |- ( Scalar ` ndx ) =/= ( .r ` ndx ) $=
+    ( cnx csca cfv cmulr wne c5 c3 3re 3lt5 gtneii scandx mulrndx neeq12i mpbir
+    ) ABCZADCZEFGEGFHIJOFPGKLMN $.
+
   $( Index value of the ~ df-vsca slot.  (Contributed by Mario Carneiro,
      14-Aug-2015.) $)
   vscandx $p |- ( .s ` ndx ) = 6 $=
@@ -143029,6 +143048,52 @@ could not be used in an extensible structure (slots must be positive
       /\ ( TopSet ` ndx ) e. NN ) $=
     ( cts c9 df-tset 9nn ndxslid ) ABCDE $.
 
+  $( The index of the slot for the group operation in an extensible structure
+     is a positive integer.  (Contributed by AV, 31-Oct-2024.) $)
+  tsetndxnn $p |- ( TopSet ` ndx ) e. NN $=
+    ( cnx cts cfv c9 cn tsetndx 9nn eqeltri ) ABCDEFGH $.
+
+  $( The index of the slot for the base set is less then the index of the slot
+     for the topology in an extensible structure.  (Contributed by AV,
+     31-Oct-2024.) $)
+  basendxlttsetndx $p |- ( Base ` ndx ) < ( TopSet ` ndx ) $=
+    ( c1 c9 cnx cbs cfv cts clt 1lt9 basendx tsetndx 3brtr4i ) ABCDECFEGHIJK $.
+
+  $( The slot for the topology is not the slot for the base set in an
+     extensible structure.  (Contributed by AV, 21-Oct-2024.)  (Proof shortened
+     by AV, 31-Oct-2024.) $)
+  tsetndxnbasendx $p |- ( TopSet ` ndx ) =/= ( Base ` ndx ) $=
+    ( cnx cbs cfv cts basendxnn nnrei basendxlttsetndx gtneii ) ABCZADCIEFGH $.
+
+  $( The slot for the topology is not the slot for the group operation in an
+     extensible structure.  (Contributed by AV, 18-Oct-2024.) $)
+  tsetndxnplusgndx $p |- ( TopSet ` ndx ) =/= ( +g ` ndx ) $=
+    ( cnx cts cfv cplusg wne c9 2re 2lt9 gtneii tsetndx plusgndx neeq12i mpbir
+    c2 ) ABCZADCZEFNENFGHIOFPNJKLM $.
+
+  $( The slot for the topology is not the slot for the ring multiplication
+     operation in an extensible structure.  (Contributed by AV,
+     31-Oct-2024.) $)
+  tsetndxnmulrndx $p |- ( TopSet ` ndx ) =/= ( .r ` ndx ) $=
+    ( cnx cts cfv cmulr wne c9 c3 3re 3lt9 gtneii tsetndx mulrndx neeq12i mpbir
+    ) ABCZADCZEFGEGFHIJOFPGKLMN $.
+
+  $( The slot for the topology is not the slot for the involution in an
+     extensible structure.  (Contributed by AV, 11-Nov-2024.) $)
+  tsetndxnstarvndx $p |- ( TopSet ` ndx ) =/= ( *r ` ndx ) $=
+    ( cnx cts cfv cstv wne c9 c4 4re 4lt9 gtneii tsetndx starvndx neeq12i mpbir
+    ) ABCZADCZEFGEGFHIJOFPGKLMN $.
+
+  $( The slots ` Scalar ` , ` .s ` and ` .i ` are different from the slot
+     ` TopSet ` .  (Contributed by AV, 29-Oct-2024.) $)
+  slotstnscsi $p |- ( ( TopSet ` ndx ) =/= ( Scalar ` ndx )
+                   /\ ( TopSet ` ndx ) =/= ( .s ` ndx )
+                   /\ ( TopSet ` ndx ) =/= ( .i ` ndx ) ) $=
+    ( cnx cts cfv csca wne cvsca cip c9 c5 5re 5lt9 gtneii tsetndx scandx mpbir
+    neeq12i c6 6re 6lt9 c8 vscandx 8re 8lt9 ipndx 3pm3.2i ) ABCZADCZEZUFAFCZEZU
+    FAGCZEZUHHIEIHJKLUFHUGIMNPOUJHQEQHRSLUFHUIQMUAPOULHTETHUBUCLUFHUKTMUDPOUE
+    $.
+
   ${
     topgrpfn.w $e |- W = { <. ( Base ` ndx ) , B >. ,
        <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } $.
@@ -143097,6 +143162,64 @@ could not be used in an extensible structure (slots must be positive
   dsslid $p |- ( dist = Slot ( dist ` ndx ) /\ ( dist ` ndx ) e. NN ) $=
     ( cds c1 c2 cdc df-ds 1nn0 2nn decnncl ndxslid ) ABCDEBCFGHI $.
 
+  $( The index of the slot for the distance in an extensible structure is a
+     positive integer.  (Contributed by AV, 28-Oct-2024.) $)
+  dsndxnn $p |- ( dist ` ndx ) e. NN $=
+    ( cnx cds cfv c1 c2 cdc cn dsndx 1nn0 2nn decnncl eqeltri ) ABCDEFGHDEIJKL
+    $.
+
+  $( The index of the slot for the base set is less then the index of the slot
+     for the distance in an extensible structure.  (Contributed by AV,
+     28-Oct-2024.) $)
+  basendxltdsndx $p |- ( Base ` ndx ) < ( dist ` ndx ) $=
+    ( c1 c2 cdc cnx cbs cfv cds clt 1nn 2nn0 1lt10 declti basendx dsndx 3brtr4i
+    1nn0 ) AABCDEFDGFHABAIJPKLMNO $.
+
+  $( The slot for the distance is not the slot for the base set in an
+     extensible structure.  (Contributed by AV, 21-Oct-2024.)  (Proof shortened
+     by AV, 28-Oct-2024.) $)
+  dsndxnbasendx $p |- ( dist ` ndx ) =/= ( Base ` ndx ) $=
+    ( cnx cbs cfv cds basendxnn nnrei basendxltdsndx gtneii ) ABCZADCIEFGH $.
+
+  $( The slot for the distance function is not the slot for the group operation
+     in an extensible structure.  (Contributed by AV, 18-Oct-2024.) $)
+  dsndxnplusgndx $p |- ( dist ` ndx ) =/= ( +g ` ndx ) $=
+    ( cnx cds cfv cplusg wne c1 c2 cdc 2re 1nn 2nn0 2lt10 declti dsndx plusgndx
+    gtneii neeq12i mpbir ) ABCZADCZEFGHZGEGUAIFGGJKKLMPSUATGNOQR $.
+
+  $( The slot for the distance function is not the slot for the ring
+     multiplication operation in an extensible structure.  (Contributed by AV,
+     31-Oct-2024.) $)
+  dsndxnmulrndx $p |- ( dist ` ndx ) =/= ( .r ` ndx ) $=
+    ( cnx cds cfv cmulr wne c1 c2 cdc c3 3re 1nn 2nn0 3lt10 declti gtneii dsndx
+    3nn0 mulrndx neeq12i mpbir ) ABCZADCZEFGHZIEIUCJFGIKLQMNOUAUCUBIPRST $.
+
+  $( The slots ` Scalar ` , ` .s ` and ` .i ` are different from the slot
+     ` dist ` .  (Contributed by AV, 29-Oct-2024.) $)
+  slotsdnscsi $p |- ( ( dist ` ndx ) =/= ( Scalar ` ndx )
+                   /\ ( dist ` ndx ) =/= ( .s ` ndx )
+                   /\ ( dist ` ndx ) =/= ( .i ` ndx ) ) $=
+    ( cnx cds cfv csca wne cvsca cip c1 c2 cdc c5 1nn 2nn0 declti dsndx neeq12i
+    gtneii mpbir c6 c8 5re 5nn0 5lt10 scandx 6re 6nn0 6lt10 vscandx 8lt10 ipndx
+    8re 8nn0 3pm3.2i ) ABCZADCZEZUNAFCZEZUNAGCZEZUPHIJZKEKVAUAHIKLMUBUCNQUNVAUO
+    KOUDPRURVASESVAUEHISLMUFUGNQUNVAUQSOUHPRUTVATETVAUKHITLMULUINQUNVAUSTOUJPRU
+    M $.
+
+  $( The slot for the distance function is not the slot for the topology in an
+     extensible structure.  (Contributed by AV, 29-Oct-2024.) $)
+  dsndxntsetndx $p |- ( dist ` ndx ) =/= ( TopSet ` ndx ) $=
+    ( cnx cds cfv cts wne c1 c2 cdc 9re 1nn 2nn0 9nn0 9lt10 declti gtneii dsndx
+    c9 tsetndx neeq12i mpbir ) ABCZADCZEFGHZQEQUCIFGQJKLMNOUAUCUBQPRST $.
+
+  $( The index of the slot for the distance is not the index of other slots.
+     (Contributed by AV, 11-Nov-2024.) $)
+  slotsdifdsndx $p |- ( ( *r ` ndx ) =/= ( dist ` ndx )
+                        /\ ( le ` ndx ) =/= ( dist ` ndx ) ) $=
+    ( cnx cstv cfv cds wne cple c4 c1 c2 cdc 4re 2nn0 4nn0 4lt10 ltneii neeq12i
+    1nn dsndx mpbir cc0 declti starvndx 10re 1nn0 0nn0 2pos declt plendx pm3.2i
+    2nn ) ABCZADCZEZAFCZULEZUMGHIJZEGUPKHIGQLMNUAOUKGULUPUBRPSUOHTJZUPEUQUPUCHT
+    IUDUEUJUFUGOUNUQULUPUHRPSUI $.
+
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -147216,6 +147339,177 @@ since the target of the homomorphism (operator ` O ` in our model) need
   $}
 
 
+$(
+#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
+  Rings
+#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
+$)
+
+
+$(
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+  Multiplicative Group
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+$)
+
+  $( Introduce new constant symbols. $)
+  $c mulGrp $. $( Multiplicative group $)
+
+  $( Multiplicative group. $)
+  cmgp $a class mulGrp $.
+
+  $( Define a structure that puts the multiplication operation of a ring in the
+     addition slot.  Note that this will not actually be a group for the
+     average ring, or even for a field, but it will be a monoid, and we get a
+     group if we restrict to the elements that have inverses.  This allows us
+     to formalize such notions as "the multiplication operation of a ring is a
+     monoid" or "the multiplicative identity" in terms of the identity of a
+     monoid ( ~ df-ur ).  (Contributed by Mario Carneiro, 21-Dec-2014.) $)
+  df-mgp $a |- mulGrp = ( w e. _V |->
+    ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) ) $.
+
+  $( The multiplicative group operator is a function.  (Contributed by Mario
+     Carneiro, 11-Mar-2015.) $)
+  fnmgp $p |- mulGrp Fn _V $=
+    ( vx cvv cv cnx cplusg cfv cmulr cop csts co cmgp wcel cslot wceq plusgslid
+    cn vex simpri mulrslid slotex elv setsex mp3an df-mgp fnmpti ) ABACZDEFZUFG
+    FZHIJZKUFBLUGPLZUHBLZUIBLAQEUGMNUJORUKAUFGBSTUAUGUHUFBBPUBUCAUDUE $.
+
+  ${
+    $d r R $.  $d r .x. $.
+    mgpval.1 $e |- M = ( mulGrp ` R ) $.
+    mgpval.2 $e |- .x. = ( .r ` R ) $.
+    $( Value of the multiplication group operation.  (Contributed by Mario
+       Carneiro, 21-Dec-2014.) $)
+    mgpvalg $p |- ( R e. V -> M = ( R sSet <. ( +g ` ndx ) , .x. >. ) ) $=
+      ( vr wcel cmgp cfv cnx cplusg cop csts co cv cmulr cvv wceq cn id eqtr4di
+      df-mgp fveq2 opeq2d oveq12d elex cslot plusgslid simpri mulrslid eqeltrid
+      a1i slotex setsex mpd3an23 fvmptd3 eqtrid ) ADHZCAIJAKLJZBMZNOZEUSGAGPZUT
+      VCQJZMZNOVBRIRGUCVCASZVCAVEVANVFUAVFVDBUTVFVDAQJZBVCAQUDFUBUEUFADUGUSUTTH
+      ZBRHVBRHVHUSLUTUHSVHUIUJUMUSBVGRFAQDUKUNULUTBADRTUOUPUQUR $.
+
+    $( Value of the group operation of the multiplication group.  (Contributed
+       by Mario Carneiro, 21-Dec-2014.) $)
+    mgpplusgg $p |- ( R e. V -> .x. = ( +g ` M ) ) $=
+      ( wcel cnx cplusg cfv cop csts co cvv wceq cmulr mulrslid slotex eqeltrid
+      plusgslid setsslid mpdan mgpvalg fveq2d eqtr4d ) ADGZBAHIJBKLMZIJZCIJUFBN
+      GBUHOUFBAPJNFAPDQRSDBINATUAUBUFCUGIABCDEFUCUDUE $.
+  $}
+
+  ${
+    mgpbas.1 $e |- M = ( mulGrp ` R ) $.
+
+    ${
+      mgpbas.2 $e |- B = ( Base ` R ) $.
+      $( Base set of the multiplication group.  (Contributed by Mario Carneiro,
+         21-Dec-2014.)  (Revised by Mario Carneiro, 5-Oct-2015.) $)
+      mgpbasg $p |- ( R e. V -> B = ( Base ` M ) ) $=
+        ( wcel cbs cfv cnx cplusg cop csts co cvv wceq mulrslid slotex baseslid
+        cmulr basendxnplusgndx cslot cn plusgslid simpri setsslnid eqid mgpvalg
+        mpdan fveq2d eqtr4d eqtrid ) BDGZABHIZCHIZFUMUNBJKIZBTIZLMNZHIZUOUMUQOG
+        UNUSPBTDQRDUQUPHOBSUAKUPUBPUPUCGUDUEUFUIUMCURHBUQCDEUQUGUHUJUKUL $.
+    $}
+
+    ${
+      mgpsca.s $e |- S = ( Scalar ` R ) $.
+      $( The multiplication monoid has the same (if any) scalars as the
+         original ring.  (Contributed by Mario Carneiro, 12-Mar-2015.)
+         (Revised by Mario Carneiro, 5-May-2015.) $)
+      mgpscag $p |- ( R e. V -> S = ( Scalar ` M ) ) $=
+        ( wcel csca cfv cnx cplusg cop csts co cvv wceq mulrslid slotex scaslid
+        cmulr scandxnplusgndx cslot cn plusgslid simpri setsslnid mpdan mgpvalg
+        eqid fveq2d eqtr4d eqtrid ) ADGZBAHIZCHIZFUMUNAJKIZATIZLMNZHIZUOUMUQOGU
+        NUSPATDQRDUQUPHOASUAKUPUBPUPUCGUDUEUFUGUMCURHAUQCDEUQUIUHUJUKUL $.
+    $}
+
+    $( Topology component of the multiplication group.  (Contributed by Mario
+       Carneiro, 5-Oct-2015.) $)
+    mgptsetg $p |- ( R e. V -> ( TopSet ` R ) = ( TopSet ` M ) ) $=
+      ( wcel cts cfv cnx cplusg cmulr cop csts co wceq mulrslid slotex tsetslid
+      cvv tsetndxnplusgndx cslot plusgslid simpri setsslnid eqid mgpvalg fveq2d
+      cn mpdan eqtr4d ) ACEZAFGZAHIGZAJGZKLMZFGZBFGUJUMREUKUONAJCOPCUMULFRAQSIU
+      LTNULUGEUAUBUCUHUJBUNFAUMBCDUMUDUEUFUI $.
+
+    ${
+      mgptopn.2 $e |- J = ( TopOpen ` R ) $.
+      $( Topology of the multiplication group.  (Contributed by Mario Carneiro,
+         5-Oct-2015.) $)
+      mgptopng $p |- ( R e. V -> J = ( TopOpen ` M ) ) $=
+        ( wcel cts cfv cbs crest co ctopn topnvalg mgptsetg mgpbasg oveq12d cvv
+        eqid cmgp eqtr3d eqtrid wceq fnmgp elex funfvex funfni sylancr eqeltrid
+        wfn syl eqtrd ) ADGZBCHIZCJIZKLZCMIZUMBAMIZUPFUMAHIZAJIZKLURUPUTUSDAUTS
+        ZUSSNUMUSUNUTUOKACDEOUTACDEVAPQUAUBUMCRGUPUQUCUMCATIZREUMTRUJARGVBRGZUD
+        ADUEVCRATATUFUGUHUIUOUNRCUOSUNSNUKUL $.
+    $}
+
+    ${
+      mgpds.2 $e |- B = ( dist ` R ) $.
+      $( Distance function of the multiplication group.  (Contributed by Mario
+         Carneiro, 5-Oct-2015.) $)
+      mgpdsg $p |- ( R e. V -> B = ( dist ` M ) ) $=
+        ( wcel cds cfv cnx cplusg cmulr cop csts co wceq mulrslid slotex dsslid
+        cvv dsndxnplusgndx cslot plusgslid simpri setsslnid eqid mgpvalg fveq2d
+        cn mpdan eqtr4d eqtrid ) BDGZABHIZCHIZFUMUNBJKIZBLIZMNOZHIZUOUMUQTGUNUS
+        PBLDQRDUQUPHTBSUAKUPUBPUPUIGUCUDUEUJUMCURHBUQCDEUQUFUGUHUKUL $.
+    $}
+  $}
+
+
+$(
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+  Ring unit
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+$)
+
+  $c 1r $.
+
+  $( Extend class notation with ring unit. $)
+  cur $a class 1r $.
+
+  $( Define the multiplicative identity, i.e., the monoid identity ( ~ df-0g )
+     of the multiplicative monoid ( ~ df-mgp ) of a ring-like structure.  This
+     definition works by transferring the multiplicative operation from the
+     ` .r ` slot to the ` +g ` slot and then looking at the element which is
+     then the ` 0g ` element, that is an identity with respect to the operation
+     which started out in the ` .r ` slot.
+
+     See also ~ dfur2g , which derives the "traditional" definition as the
+     unique element of a ring which is left- and right-neutral under
+     multiplication.  (Contributed by NM, 27-Aug-2011.)  (Revised by Mario
+     Carneiro, 27-Dec-2014.) $)
+  df-ur $a |- 1r = ( 0g o. mulGrp ) $.
+
+  ${
+    ringidval.g $e |- G = ( mulGrp ` R ) $.
+    ringidval.u $e |- .1. = ( 1r ` R ) $.
+    $( The value of the unity element of a ring.  (Contributed by NM,
+       27-Aug-2011.)  (Revised by Mario Carneiro, 27-Dec-2014.) $)
+    ringidvalg $p |- ( R e. V -> .1. = ( 0g ` G ) ) $=
+      ( wcel cur cfv cmgp c0g cvv wceq elex ccom df-ur fveq1i wfn fnmgp fvco2
+      mpan eqtrid syl fveq2i 3eqtr4g ) ADGZAHIZAJIZKIZBCKIUFALGZUGUIMADNUJUGAKJ
+      OZIZUIAHUKPQJLRUJULUIMSLKJATUAUBUCFCUHKEUDUE $.
+  $}
+
+  ${
+    $d e x B $.  $d e x R $.  $d e x V $.
+    dfur2.b $e |- B = ( Base ` R ) $.
+    dfur2.t $e |- .x. = ( .r ` R ) $.
+    dfur2.u $e |- .1. = ( 1r ` R ) $.
+    $( The multiplicative identity is the unique element of the ring that is
+       left- and right-neutral on all elements under multiplication.
+       (Contributed by Mario Carneiro, 10-Jan-2015.) $)
+    dfur2g $p |- ( R e. V -> .1. = ( iota e ( e e. B /\
+      A. x e. B ( ( e .x. x ) = x /\ ( x .x. e ) = x ) ) ) ) $=
+      ( wcel cmgp cfv cv co wceq wa wral cvv eqid c0g cbs cplusg cio fnmgp elex
+      wfn funfvex funfni sylancr grpidvalg syl ringidvalg mgpbasg eleq2d eqeq1d
+      mgpplusgg oveqd anbi12d raleqbidv iotabidv 3eqtr4d ) CGKZCLMZUAMZFNZVDUBM
+      ZKZVFANZVDUCMZOZVIPZVIVFVJOZVIPZQZAVGRZQZFUDZEVFBKZVFVIDOZVIPZVIVFDOZVIPZ
+      QZABRZQZFUDVCVDSKZVEVRPVCLSUGCSKWGUECGUFWGSCLCLUHUIUJAVGVJFVDSVEVGTVJTVET
+      UKULCEVDGVDTZJUMVCWFVQFVCVSVHWEVPVCBVGVFBCVDGWHHUNZUOVCWDVOABVGWIVCWAVLWC
+      VNVCVTVKVIVCDVJVFVICDVDGWHIUQZURUPVCWBVMVIVCDVJVIVFWJURUPUSUTUSVAVB $.
+  $}
+
+
 $(
 #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
   The complex numbers as an algebraic extensible structure
@@ -164438,6 +164732,12 @@ Norman Megill (2007) section 1.1.3.  Megill then states, "A number of
 htmldef "SubMnd" as "SubMnd";
   althtmldef "SubMnd" as "SubMnd";
   latexdef "SubMnd" as "\mathrm{SubMnd}";
+htmldef "mulGrp" as "mulGrp";
+  althtmldef "mulGrp" as "mulGrp";
+  latexdef "mulGrp" as "\mathrm{mulGrp}";
+htmldef "1r" as "<IMG SRC='_1r.gif' WIDTH=13 HEIGHT=19 ALT=' 1r' TITLE='1r'>";
+  althtmldef "1r" as "1<SUB>r</SUB>";
+  latexdef "1r" as "1_\mathrm{r}";
 htmldef "numer" as "numer";
   althtmldef "numer" as "numer";
   latexdef "numer" as "\mathrm{numer}";