Move 'monoid of endomorphisms' subsection from my mathbox to Main. Sh…

…orten a few proofs.
metamath · Sep 26, 2024 · 8382693 · 8382693
1 parent e883152
commit 8382693
Show file tree

Hide file tree

Showing 2 changed files with 128 additions and 98 deletions.
diff --git a/discouraged b/discouraged
@@ -16168,6 +16168,9 @@ New usage of "funop" is discouraged (2 uses).
 New usage of "funopg" is discouraged (0 uses).
 New usage of "funopsn" is discouraged (2 uses).
 New usage of "fvimacnvALT" is discouraged (0 uses).
+New usage of "fvpr1OLD" is discouraged (0 uses).
+New usage of "fvpr2OLD" is discouraged (0 uses).
+New usage of "fvpr2gOLD" is discouraged (0 uses).
 New usage of "fvprcALT" is discouraged (0 uses).
 New usage of "gcdabsOLD" is discouraged (0 uses).
 New usage of "gcdmultipleOLD" is discouraged (0 uses).
@@ -19792,6 +19795,9 @@ Proof modification of "funcrngcsetcALT" is discouraged (765 steps).
 Proof modification of "fundcmpsurinjALT" is discouraged (221 steps).
 Proof modification of "fvilbdRP" is discouraged (27 steps).
 Proof modification of "fvimacnvALT" is discouraged (102 steps).
+Proof modification of "fvpr1OLD" is discouraged (56 steps).
+Proof modification of "fvpr2OLD" is discouraged (44 steps).
+Proof modification of "fvpr2gOLD" is discouraged (75 steps).
 Proof modification of "fvprcALT" is discouraged (26 steps).
 Proof modification of "gcdabsOLD" is discouraged (170 steps).
 Proof modification of "gcdmultipleOLD" is discouraged (348 steps).

diff --git a/set.mm b/set.mm
@@ -66040,7 +66040,7 @@ pairs as classes (in set.mm, the Kuratowski encoding).  A more
   $( Recover the original function from a point-added function.  (Contributed
      by Stefan O'Rear, 28-Feb-2015.) $)
   fsnunres $p |- ( ( F Fn S /\ -. X e. S ) ->
-      ( ( F u. { <. X , Y >. } ) |` S ) = F ) $=
+                                     ( ( F u. { <. X , Y >. } ) |` S ) = F ) $=
     ( wfn wcel wn wa cres cop csn cun c0 fnresdm adantr ressnop0 adantl uneq12d
     wceq resundir un0 eqcomi 3eqtr4g ) BAEZCAFGZHZBAIZCDJKZAIZLBMLZBUHLAIBUFUGB
     UIMUDUGBSUEABNOUEUIMSUDCDAPQRBUHATUJBBUAUBUC $.
@@ -66056,12 +66056,46 @@ pairs as classes (in set.mm, the Kuratowski encoding).  A more
     AKLHZMAUGUJIJZULMZAUIUKUMULUFUKUMNZUHUFAOUOAPABQRSTUFAUGUAUHAUNNAUBUGABUCUD
     UE $.
 
+  $( The value of a function with a domain of (at most) two elements.
+     (Contributed by Alexander van der Vekens, 3-Dec-2017.) $)
+  fvpr1g $p |- ( ( A e. V /\ C e. W /\ A =/= B )
+                 -> ( { <. A , C >. , <. B , D >. } ` A ) = C ) $=
+    ( wcel wne w3a cop cpr cfv csn wceq cun df-pr fveq1i necom fvunsn sylbi
+    syl5eq 3ad2ant3 fvsng 3adant3 eqtrd ) AEGZCFGZABHZIAACJZBDJZKZLZAUIMZLZCUHU
+    FULUNNUGUHULAUMUJMOZLZUNAUKUOUIUJPQUHBAHUPUNNABRUMBDASTUAUBUFUGUNCNUHACEFUC
+    UDUE $.
+
+  $( The value of a function with a domain of (at most) two elements.
+     (Contributed by Alexander van der Vekens, 3-Dec-2017.)  (Proof shortened
+     by BJ, 26-Sep-2024.) $)
+  fvpr2g $p |- ( ( B e. V /\ D e. W /\ A =/= B )
+                 -> ( { <. A , C >. , <. B , D >. } ` B ) = D ) $=
+    ( wcel wne w3a cop cpr cfv prcom fveq1i wceq necom fvpr1g syl3an3b syl5eq )
+    BEGZDFGZABHZIBACJZBDJZKZLBUDUCKZLZDBUEUFUCUDMNUBTUABAHUGDOABPBADCEFQRS $.
+
+  $( Obsolete version of ~ fvpr2g as of 26-Sep-2024.  (Contributed by Alexander
+     van der Vekens, 3-Dec-2017.)  (Proof modification is discouraged.)
+     (New usage is discouraged.) $)
+  fvpr2gOLD $p |- ( ( B e. V /\ D e. W /\ A =/= B )
+                  -> ( { <. A , C >. , <. B , D >. } ` B ) = D ) $=
+    ( wcel wne w3a cop cpr cfv csn wceq cun prcom df-pr eqtri fveq1i fvunsn
+    syl5eq 3ad2ant3 fvsng 3adant3 eqtrd ) BEGZDFGZABHZIBACJZBDJZKZLZBUJMZLZDUHU
+    FULUNNUGUHULBUMUIMOZLUNBUKUOUKUJUIKUOUIUJPUJUIQRSUMACBTUAUBUFUGUNDNUHBDEFUC
+    UDUE $.
+
   ${
     fvpr1.1 $e |- A e. _V $.
     fvpr1.2 $e |- C e. _V $.
     $( The value of a function with a domain of two elements.  (Contributed by
-       Jeff Madsen, 20-Jun-2010.) $)
+       Jeff Madsen, 20-Jun-2010.)  (Proof shortened by BJ, 26-Sep-2024.) $)
     fvpr1 $p |- ( A =/= B -> ( { <. A , C >. , <. B , D >. } ` A ) = C ) $=
+      ( cvv wcel wne cop cpr cfv wceq fvpr1g mp3an12 ) AGHCGHABIAACJBDJKLCMEFAB
+      CDGGNO $.
+
+    $( Obsolete version of ~ fvpr1 as of 26-Sep-2024.  (Contributed by Jeff
+       Madsen, 20-Jun-2010.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    fvpr1OLD $p |- ( A =/= B -> ( { <. A , C >. , <. B , D >. } ` A ) = C ) $=
       ( wne cop cpr cfv csn df-pr fveq1i wceq necom fvunsn sylbi syl5eq fvsn
       cun eqtrdi ) ABGZAACHZBDHZIZJZAUCKZJZCUBUFAUGUDKTZJZUHAUEUIUCUDLMUBBAGUJU
       HNABOUGBDAPQRACEFSUA $.
@@ -66071,30 +66105,19 @@ pairs as classes (in set.mm, the Kuratowski encoding).  A more
     fvpr2.1 $e |- B e. _V $.
     fvpr2.2 $e |- D e. _V $.
     $( The value of a function with a domain of two elements.  (Contributed by
-       Jeff Madsen, 20-Jun-2010.) $)
+       Jeff Madsen, 20-Jun-2010.)  (Proof shortened by BJ, 26-Sep-2024.) $)
     fvpr2 $p |- ( A =/= B -> ( { <. A , C >. , <. B , D >. } ` B ) = D ) $=
+      ( cvv wcel wne cop cpr cfv wceq fvpr2g mp3an12 ) BGHDGHABIBACJBDJKLDMEFAB
+      CDGGNO $.
+
+    $( Obsolete version of ~ fvpr2 as of 26-Sep-2024.  (Contributed by Jeff
+       Madsen, 20-Jun-2010.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    fvpr2OLD $p |- ( A =/= B -> ( { <. A , C >. , <. B , D >. } ` B ) = D ) $=
       ( wne cop cpr cfv prcom fveq1i wceq necom fvpr1 sylbi syl5eq ) ABGZBACHZB
       DHZIZJBTSIZJZDBUAUBSTKLRBAGUCDMABNBADCEFOPQ $.
   $}
 
-  $( The value of a function with a domain of (at most) two elements.
-     (Contributed by Alexander van der Vekens, 3-Dec-2017.) $)
-  fvpr1g $p |- ( ( A e. V /\ C e. W /\ A =/= B )
-                 -> ( { <. A , C >. , <. B , D >. } ` A ) = C ) $=
-    ( wcel wne w3a cop cpr cfv csn wceq cun df-pr fveq1i necom fvunsn sylbi
-    syl5eq 3ad2ant3 fvsng 3adant3 eqtrd ) AEGZCFGZABHZIAACJZBDJZKZLZAUIMZLZCUHU
-    FULUNNUGUHULAUMUJMOZLZUNAUKUOUIUJPQUHBAHUPUNNABRUMBDASTUAUBUFUGUNCNUHACEFUC
-    UDUE $.
-
-  $( The value of a function with a domain of (at most) two elements.
-     (Contributed by Alexander van der Vekens, 3-Dec-2017.) $)
-  fvpr2g $p |- ( ( B e. V /\ D e. W /\ A =/= B )
-                 -> ( { <. A , C >. , <. B , D >. } ` B ) = D ) $=
-    ( wcel wne w3a cop cpr cfv csn wceq cun prcom df-pr eqtri fveq1i fvunsn
-    syl5eq 3ad2ant3 fvsng 3adant3 eqtrd ) BEGZDFGZABHZIBACJZBDJZKZLZBUJMZLZDUHU
-    FULUNNUGUHULBUMUIMOZLUNBUKUOUKUJUIKUOUIUJPUJUIQRSUMACBTUAUBUFUGUNDNUHBDEFUC
-    UDUE $.
-
   ${
     $d A x y $.  $d B x y $.  $d F x y $.  $d R x y $.
     fprb.1 $e |- A e. _V $.
@@ -70390,11 +70413,11 @@ result of an operator (deduction version).  (Contributed by Paul
     ovigg.1 $e |- ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) ) $.
     ovigg.4 $e |- E* z ph $.
     ovigg.5 $e |- F = { <. <. x , y >. , z >. | ph } $.
-    $( The value of an operation class abstraction.  Compare ~ ovig .  The
-       condition ` ( x e. R /\ y e. S ) ` is been removed.  (Contributed by FL,
+    $( The value of an operation class abstraction.  Compared with ~ ovig , the
+       condition ` ( x e. R /\ y e. S ) ` is removed.  (Contributed by FL,
        24-Mar-2007.)  (Revised by Mario Carneiro, 19-Dec-2013.) $)
-    ovigg $p |- ( ( A e. V /\ B e. W /\ C e. X ) ->
-                         ( ps -> ( A F B ) = C ) ) $=
+    ovigg $p |-
+               ( ( A e. V /\ B e. W /\ C e. X ) -> ( ps -> ( A F B ) = C ) ) $=
       ( wcel w3a cop wceq cfv coprab eloprabga df-ov fveq1i eqtri wfun funoprab
       co wi funopfv ax-mp syl5eq syl6bir ) FJPGKPHLPQBFGRZHRACDEUAZPZFGIUHZHSAB
       CDEFGHJKLMUBUPUQUNUOTZHUQUNITURFGIUCUNIUOOUDUEUOUFUPURHSUIACDENUGUNHUOUJU
@@ -221332,6 +221355,76 @@ proposition to be be proved (the first four hypotheses tell its values
   $}
 
 
+$(
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+  Monoid of endomorphisms
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+$)
+
+  $c End $.
+  $( Token for the monoid of endomorphisms. $)
+  cend $a class End $. $( Syntax for the monoid of endomorphisms. $)
+
+  ${
+    $d c x $.
+    $( Define the monoid of endomorphisms on an object of a category.
+       (Contributed by BJ, 4-Apr-2024.) $)
+    df-end $a |- End = ( c e. Cat |-> ( x e. ( Base ` c ) |->
+                 { <. ( Base ` ndx ) , ( x ( Hom ` c ) x ) >. ,
+                   <. ( +g ` ndx ) , ( <. x , x >. ( comp ` c ) x ) >. } ) ) $.
+  $}
+
+  ${
+    $d C c x $.  $d X c x $.  $d ph c x $.
+    endval.c $e |- ( ph -> C e. Cat ) $.
+    endval.x $e |- ( ph -> X e. ( Base ` C ) ) $.
+    $( Value of the monoid of endomorphisms on an object of a category.
+       (Contributed by BJ, 5-Apr-2024.) $)
+    endval $p |- ( ph -> ( ( End ` C ) ` X ) =
+                   { <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. ,
+                     <. ( +g ` ndx ) , ( <. X , X >. ( comp ` C ) X ) >. } ) $=
+      ( vx vc cnx cbs cfv cv chom co cop cco cpr cvv wceq fveq2 opeq2d cend a1i
+      cplusg cmpt ccat df-end oveqd preq12d mpteq12dv wcel fvex fvmptd3 oveq12d
+      mptex id opeq12d adantl prex fvmptd ) AFCHIJZFKZVABLJZMZNZHUCJZVAVANZVABO
+      JZMZNZPZUTCCVBMZNZVECCNZCVGMZNZPZBIJZBUAJQAGBFGKZIJZUTVAVAVRLJZMZNZVEVFVA
+      VROJZMZNZPZUDFVQVJUDZUEUAQFGUFVRBRZFVSWFVQVJVRBISWHWBVDWEVIWHWAVCUTWHVTVB
+      VAVAVRBLSUGTWHWDVHVEWHWCVGVFVAVRBOSUGTUHUIDWGQUJAFVQVJBIUKUNUBULVACRZVJVP
+      RAWIVDVLVIVOWIVCVKUTWIVACVACVBWIUOZWJUMTWIVHVNVEWIVFVMVACVGWIVACVACWJWJUP
+      WJUMTUHUQEVPQUJAVLVOURUBUS $.
+
+    $( Base set of the monoid of endomorphisms on an object of a category.
+       (Contributed by BJ, 5-Apr-2024.) $)
+    endbase $p |- ( ph ->
+                      ( Base ` ( ( End ` C ) ` X ) ) = ( X ( Hom ` C ) X ) ) $=
+      ( cnx cbs cfv cend chom co cop cplusg cco cpr endval fveq1d c1 cvv fvexd
+      df-base 1nn strndxid wceq basendxnplusgndx fvex ovex fvpr1 mp1i 3eqtr3d
+      wne ) AFGHZCBIHZHZHULULCCBJHZKZLFMHZCCLCBNHKZLOZHZUNGHUPAULUNUSABCDEPQAUN
+      GRSACUMTUAUBUCULUQUKUTUPUDAUEULUQUPURFGUFCCUOUGUHUIUJ $.
+
+    $( Composition law of the monoid of endomorphisms on an object of a
+       category.  (Contributed by BJ, 5-Apr-2024.) $)
+    endcomp $p |- ( ph ->
+             ( +g ` ( ( End ` C ) ` X ) ) = ( <. X , X >. ( comp ` C ) X ) ) $=
+      ( cnx cplusg cfv cend cbs chom co cop cco cpr endval fveq1d c2 cvv fvexd
+      df-plusg 2nn strndxid wceq basendxnplusgndx fvex ovex fvpr2 mp1i 3eqtr3d
+      wne ) AFGHZCBIHZHZHULFJHZCCBKHLZMULCCMZCBNHZLZMOZHZUNGHUSAULUNUTABCDEPQAU
+      NGRSACUMTUAUBUCUOULUKVAUSUDAUEUOULUPUSFGUFUQCURUGUHUIUJ $.
+
+    $d C x y z $.  $d X x y z $.  $d ph x y z $.
+    $( The monoid of endomorphisms on an object of a category is a monoid.
+       (Contributed by BJ, 5-Apr-2024.) $)
+    endmnd $p |- ( ph -> ( ( End ` C ) ` X ) e. Mnd ) $=
+      ( vx vy vz cfv co cbs eqcomd cv wcel w3a eqid 3ad2ant1 simp3 adantr syl
+      chom cop cco cend ccid endbase cplusg endcomp ccat simp2 catcocl wa simpr
+      simp1 catass catidcl catlid catrid ismndd ) AFGHCCBUAIZJZCCUBCBUCIZJZCBUD
+      IIZCBUEIZIAVDKIVAABCDEUFLAVDUGIVCABCDEUHLAFMZVANZGMZVANZOBKIZBVBVHVFUTCCC
+      VJPZUTPZVBPZAVGBUINZVIDQAVGCVJNZVIEQZVPVPAVGVIRAVGVIUJUKAVGVIHMZVANZOZULZ
+      VJBVBVQVHUTVFCCCCVKVLVMAVNVSDSAVOVSESZWAWAVTVSVRAVSUMZVGVIVRRTVTVSVIWBVGV
+      IVRUJTWAVTVSVGWBVGVIVRUNTUOAVJBVEUTCVKVLVEPZDEUPAVGULZVJBVBVEVFUTCCVKVLWC
+      AVNVGDSZAVOVGESZVMWFAVGUMZUQWDVJBVBVEVFUTCCVKVLWCWEWFVMWFWGURUS $.
+  $}
+
+
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
   Iterated sums in a monoid
@@ -441175,6 +441268,9 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the
     "<IMG SRC='_mnd.gif' WIDTH=28 HEIGHT=19 ALT=' Mnd' TITLE='Mnd'>";
   althtmldef "Mnd" as "Mnd";
   latexdef "Mnd" as "\mathrm{Mnd}";
+htmldef "End" as "End ";
+  althtmldef "End" as "End ";
+  latexdef "End" as "\operatorname{End}";
 htmldef "Grp" as
     "<IMG SRC='_grp.gif' WIDTH=25 HEIGHT=19 ALT=' Grp' TITLE='Grp'>";
   althtmldef "Grp" as "Grp";
@@ -445867,9 +445963,6 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the
 htmldef "RRVec" as "RR-Vec";
   althtmldef "RRVec" as "&#8477;-Vec";
   latexdef "RRVec" as "{\mathbb{R}-\mathrm{Vec}}";
-htmldef "End" as "End ";
-  althtmldef "End" as "End ";
-  latexdef "End" as "\operatorname{End}";
 /* End of BJ's mathbox */
 
 /* Mathbox of Norm Megill */
@@ -524495,6 +524588,7 @@ Real and complex numbers (cont.)
     ZURUSVAVBURUSJUOVBUQACVBUQAKBAUDLMNVDUSUTUOVBUSUTUMUNVBUSIUTRULBACOUEPUIQUL
     UMUPVBUFZUNULASBSVEUMATBTABUGUHUJUK $.
 
+
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
   Properties of real and complex numbers
@@ -553041,76 +553135,6 @@ coordinates of a barycenter of two points in one dimension (complex
       GVCVFVDTVEUOVG $.
   $}
 
-
-$(
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
-  Monoid of endomorphisms
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
-$)
-
-  $c End $.
-  $( Token for the monoid of endomorphisms. $)
-  cend $a class End $. $( Syntax for the monoid of endomorphisms. $)
-
-  ${
-    $d c x $.
-    $( The monoid of endomorphisms on an object of a category.  (Contributed by
-       BJ, 4-Apr-2024.) $)
-    df-bj-end $a |- End = ( c e. Cat |-> ( x e. ( Base ` c ) |->
-                 { <. ( Base ` ndx ) , ( x ( Hom ` c ) x ) >. ,
-                   <. ( +g ` ndx ) , ( <. x , x >. ( comp ` c ) x ) >. } ) ) $.
-  $}
-
-  ${
-    $d C c x $.  $d X c x $.  $d ph c x $.
-    bj-endval.c $e |- ( ph -> C e. Cat ) $.
-    bj-endval.x $e |- ( ph -> X e. ( Base ` C ) ) $.
-    $( Value of the monoid of endomorphisms on an object of a category.
-       (Contributed by BJ, 5-Apr-2024.) $)
-    bj-endval $p |- ( ph -> ( ( End ` C ) ` X ) =
-                   { <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. ,
-                     <. ( +g ` ndx ) , ( <. X , X >. ( comp ` C ) X ) >. } ) $=
-      ( vx vc cnx cbs cfv cv chom co cop cco cpr cvv wceq fveq2 opeq2d cend a1i
-      cplusg cmpt ccat df-bj-end preq12d mpteq12dv wcel fvex fvmptd3 id oveq12d
-      oveqd mptex opeq12d adantl prex fvmptd ) AFCHIJZFKZVABLJZMZNZHUCJZVAVANZV
-      ABOJZMZNZPZUTCCVBMZNZVECCNZCVGMZNZPZBIJZBUAJQAGBFGKZIJZUTVAVAVRLJZMZNZVEV
-      FVAVROJZMZNZPZUDFVQVJUDZUEUAQFGUFVRBRZFVSWFVQVJVRBISWHWBVDWEVIWHWAVCUTWHV
-      TVBVAVAVRBLSUNTWHWDVHVEWHWCVGVFVAVRBOSUNTUGUHDWGQUIAFVQVJBIUJUOUBUKVACRZV
-      JVPRAWIVDVLVIVOWIVCVKUTWIVACVACVBWIULZWJUMTWIVHVNVEWIVFVMVACVGWIVACVACWJW
-      JUPWJUMTUGUQEVPQUIAVLVOURUBUS $.
-
-    $( Base set of the monoid of endomorphisms on an object of a category.
-       (Contributed by BJ, 5-Apr-2024.) $)
-    bj-endbase $p |- ( ph ->
-                      ( Base ` ( ( End ` C ) ` X ) ) = ( X ( Hom ` C ) X ) ) $=
-      ( cnx cbs cfv cend chom co cop cplusg cco cpr bj-endval fveq1d cvv fvexd
-      c1 df-base 1nn strndxid wne wceq basendxnplusgndx fvex ovex fvpr1 3eqtr3d
-      mp1i ) AFGHZCBIHZHZHULULCCBJHZKZLFMHZCCLCBNHKZLOZHZUNGHUPAULUNUSABCDEPQAU
-      NGTRACUMSUAUBUCULUQUDUTUPUEAUFULUQUPURFGUGCCUOUHUIUKUJ $.
-
-    $( Composition law of the monoid of endomorphisms on an object of a
-       category.  (Contributed by BJ, 5-Apr-2024.) $)
-    bj-endcomp $p |- ( ph ->
-             ( +g ` ( ( End ` C ) ` X ) ) = ( <. X , X >. ( comp ` C ) X ) ) $=
-      ( cnx cplusg cfv cend cbs chom co cop cco cpr bj-endval fveq1d cvv fvexd
-      c2 df-plusg 2nn strndxid wne wceq basendxnplusgndx fvex ovex mp1i 3eqtr3d
-      fvpr2 ) AFGHZCBIHZHZHULFJHZCCBKHLZMULCCMZCBNHZLZMOZHZUNGHUSAULUNUTABCDEPQ
-      AUNGTRACUMSUAUBUCUOULUDVAUSUEAUFUOULUPUSFGUGUQCURUHUKUIUJ $.
-
-    $d C x y z $.  $d X x y z $.  $d ph x y z $.
-    $( The monoid of endomorphisms on an object of a category is a monoid.
-       (Contributed by BJ, 5-Apr-2024.) $)
-    bj-endmnd $p |- ( ph -> ( ( End ` C ) ` X ) e. Mnd ) $=
-      ( vx vy vz cfv co cbs eqcomd cv wcel w3a eqid 3ad2ant1 simp3 adantr syl
-      chom cop cco cend ccid bj-endbase cplusg bj-endcomp ccat simp2 catcocl wa
-      simpr simp1 catass catidcl catlid catrid ismndd ) AFGHCCBUAIZJZCCUBCBUCIZ
-      JZCBUDIIZCBUEIZIAVDKIVAABCDEUFLAVDUGIVCABCDEUHLAFMZVANZGMZVANZOBKIZBVBVHV
-      FUTCCCVJPZUTPZVBPZAVGBUINZVIDQAVGCVJNZVIEQZVPVPAVGVIRAVGVIUJUKAVGVIHMZVAN
-      ZOZULZVJBVBVQVHUTVFCCCCVKVLVMAVNVSDSAVOVSESZWAWAVTVSVRAVSUMZVGVIVRRTVTVSV
-      IWBVGVIVRUJTWAVTVSVGWBVGVIVRUNTUOAVJBVEUTCVKVLVEPZDEUPAVGULZVJBVBVEVFUTCC
-      VKVLWCAVNVGDSZAVOVGESZVMWFAVGUMZUQWDVJBVBVEVFUTCCVKVLWCWEWFVMWFWGURUS $.
-  $}
-
 $( (End of BJ's mathbox.) $)
 $( End $[ set-mbox-bj.mm $] $)