Submonoids of injectiv/surjective endofunctions

~sursubmefmnd and ~injsubmefmnd as proposed by Gérard Lang, allowing for a a shorter proof of ~symgsubmefmnd, also proposed by Gérard Lang (~insubm required).
avekens · Feb 25, 2024 · ca97d9e · ca97d9e
1 parent 1c9692e
commit ca97d9e
Show file tree

Hide file tree

Showing 2 changed files with 75 additions and 0 deletions.
diff --git a/discouraged b/discouraged
@@ -17612,6 +17612,7 @@ New usage of "supsrlem" is discouraged (1 uses).
 New usage of "swrdnznd" is discouraged (1 uses).
 New usage of "syl5imp" is discouraged (0 uses).
 New usage of "syl5impVD" is discouraged (0 uses).
+New usage of "symgsubmefmndALT" is discouraged (0 uses).
 New usage of "tarski-bernays-ax2" is discouraged (0 uses).
 New usage of "tb-ax1" is discouraged (3 uses).
 New usage of "tb-ax2" is discouraged (1 uses).
@@ -19351,6 +19352,7 @@ Proof modification of "suctrALTcfVD" is discouraged (164 steps).
 Proof modification of "supp0cosupp0OLD" is discouraged (176 steps).
 Proof modification of "syl5imp" is discouraged (23 steps).
 Proof modification of "syl5impVD" is discouraged (57 steps).
+Proof modification of "symgsubmefmndALT" is discouraged (199 steps).
 Proof modification of "symrefref3" is discouraged (75 steps).
 Proof modification of "tarski-bernays-ax2" is discouraged (557 steps).
 Proof modification of "tb-ax1" is discouraged (4 steps).

diff --git a/set.mm b/set.mm
@@ -218589,6 +218589,28 @@ everywhere defined internal operation (see ~ mndcl ), whose operation is
       DEVBVFVAABVICVSURUS $.
   $}
 
+  ${
+    $d A a b x y $.  $d B a b x y $.  $d M a b x y $.
+    $( The intersection of two submonoids is a submonoid.  (Contributed by AV,
+       25-Feb-2024.) $)
+    insubm $p |- ( ( A e. ( SubMnd ` M ) /\ B e. ( SubMnd ` M ) )
+                   -> ( A i^i B ) e. ( SubMnd ` M ) ) $=
+      ( va vb vx vy cfv wcel wi wss cv co wral w3a wa elin imp adantl eleq1d ex
+      csubmnd cin cmnd submrcl cbs cplusg ssinss1 3ad2ant1 ad2antrl simplbi2com
+      c0g 3ad2ant2 com12 anbi12i oveq1 oveq2 simpl eqidd rspc2vd 3ad2ant3 simpr
+      adantr elind syl5bi ralrimivv 3jca eqid issubm anbi12d 3imtr4d expd mpcom
+      weq ) ACUBHZIZBVOIZABUCZVOIZCUDIZVPVQVSJACUEVTVPVQVSVTACUFHZKZCULHZAIZDLZ
+      ELZCUGHZMZAIZEANDANZOZBWAKZWCBIZWHBIZEBNDBNZOZPZVRWAKZWCVRIZFLZGLZWGMZVRI
+      ZGVRNFVRNZOZVPVQPVSVTWQXEVTWQPZWRWSXDWKWRVTWPWBWDWRWJABWAUHUIUJWQWSVTWKWP
+      WSWDWBWPWSJWJWPWDWSWMWLWDWSJWOWSWDWMWCABQUKUMUNUMRSXFXCFGVRVRWTVRIZXAVRIZ
+      PWTAIZWTBIZPZXAAIZXABIZPZPZXFXCXGXKXHXNWTABQXAABQUOXFXOXCXFXOPABXBXFXOXBA
+      IZWKXOXPJZVTWPWJWBXQWDXOWJXPXOXPWTWFWGMZAIWIDEWTXAAAADFVNZWHXRAWEWTWFWGUP
+      ZTEGVNZXRXBAWFXAWTWGUQZTXKXIXNXIXJURVCXOXSPZAUSXNXLXKXLXMURSUTUNVAUJRXFXO
+      XBBIZWQXOYDJZVTWPYEWKWOWLYEWMXOWOYDXOYDXRBIWNDEWTXABBBXSWHXRBXTTYAXRXBBYB
+      TXKXJXNXIXJVBVCYCBUSXNXMXKXLXMVBSUTUNVASSRVDUAVEVFVGUAVTVPWKVQWPDEWAWGACW
+      CWAVHZWCVHZWGVHZVIDEWAWGBCWCYFYGYHVIVJFGWAWGVRCWCYFYGYHVIVKVLVMR $.
+  $}
+
   ${
     $d x y B $.  $d x y M $.  $d x y N $.  $d x y .0. $.
     0mhm.z $e |- .0. = ( 0g ` N ) $.
@@ -741927,6 +741949,46 @@ According to Wikipedia ("Endomorphism", 25-Jan-2024,
       ULUMUNUOVKWHVPSDEBBFFVOUPUQUTVAVBVCVDVEBFGCIKMLVFVGVH $.
   $}
 
+  ${
+    $d A h x y $.  $d M x y $.  $d V x y $.
+    sursubmefmnd.m $e |- M = ( EndoFMnd ` A ) $.
+    $( The set of surjective endofunctions on a set ` A ` is a submonoid of the
+       monoid of endofunctions on ` A ` .  (Contributed by AV, 25-Feb-2024.) $)
+    sursubmefmnd $p |- ( A e. V
+                         -> { h | h : A -onto-> A } e. ( SubMnd ` M ) ) $=
+      ( vx vy wcel cv wfo cfv wral vex foeq1 elab wf fof eqid syl wa cab cplusg
+      csubmnd cbs wss c0g elefmndbas syl5ibr syl5bi ssrdv cid cres efmndid wf1o
+      co f1oi f1ofo mp1i cvv wb resiexg elabg mpbird eqeltrrd anbi12i ccom foco
+      adantl wceq anim12i anbi12d imp efmndov eleq1d coex syl6bb ralrimivv cmnd
+      ex w3a efmndmnd issubm mpbir3and ) ADHZAABIZJZBUAZCUCKHZWGCUDKZUEZCUFKZWG
+      HZFIZGIZCUBKZUOZWGHZGWGLFWGLZWDFWGWIWMWGHZAAWMJZWDWMWIHZWFWTBWMFMZAAWEWMN
+      OZWTXAWDAAWMPZAAWMQZAWIWMCDEWIRZUGZUHUIUJWDUKAULZWKWGACDEUMWDXHWGHZAAXHJZ
+      AAXHUNXJWDAUPAAXHUQURWDXHUSHXIXJUTADVAWFXJBXHUSAAWEXHNVBSVCVDWDWQFGWGWGWS
+      WNWGHZTWTAAWNJZTZWDWQWSWTXKXLXCWFXLBWNGMZAAWEWNNOVEWDXMWQWDXMTZWQAAWMWNVF
+      ZJZXMXQWDAAAWMWNVGVHXOWQXPWGHXQXOWPXPWGXOXAWNWIHZTZWPXPVIWDXMXSXMXSWDXDAA
+      WNPZTWTXDXLXTXEAAWNQVJWDXAXDXRXTXGAWIWNCDEXFUGVKUHVLAWIWOCWMWNEXFWORZVMSV
+      NWFXQBXPWMWNXBXNVOAAWEXPNOVPVCVSUIVQWDCVRHWHWJWLWRVTUTACDEWAFGWIWOWGCWKXF
+      WKRYAWBSWC $.
+
+    $( The set of injective endofunctions on a set ` A ` is a submonoid of the
+       monoid of endofunctions on ` A ` .  (Contributed by AV, 25-Feb-2024.) $)
+    injsubmefmnd $p |- ( A e. V
+                         -> { h | h : A -1-1-> A } e. ( SubMnd ` M ) ) $=
+      ( vx vy wcel cv wf1 cfv wral vex f1eq1 elab wf f1f eqid syl wa cab cplusg
+      csubmnd cbs wss c0g elefmndbas syl5ibr syl5bi ssrdv cid cres efmndid wf1o
+      co f1oi f1of1 mp1i cvv wb resiexg elabg mpbird eqeltrrd anbi12i ccom f1co
+      adantl wceq anim12i anbi12d imp efmndov eleq1d coex syl6bb ralrimivv cmnd
+      ex w3a efmndmnd issubm mpbir3and ) ADHZAABIZJZBUAZCUCKHZWGCUDKZUEZCUFKZWG
+      HZFIZGIZCUBKZUOZWGHZGWGLFWGLZWDFWGWIWMWGHZAAWMJZWDWMWIHZWFWTBWMFMZAAWEWMN
+      OZWTXAWDAAWMPZAAWMQZAWIWMCDEWIRZUGZUHUIUJWDUKAULZWKWGACDEUMWDXHWGHZAAXHJZ
+      AAXHUNXJWDAUPAAXHUQURWDXHUSHXIXJUTADVAWFXJBXHUSAAWEXHNVBSVCVDWDWQFGWGWGWS
+      WNWGHZTWTAAWNJZTZWDWQWSWTXKXLXCWFXLBWNGMZAAWEWNNOVEWDXMWQWDXMTZWQAAWMWNVF
+      ZJZXMXQWDAAAWMWNVGVHXOWQXPWGHXQXOWPXPWGXOXAWNWIHZTZWPXPVIWDXMXSXMXSWDXDAA
+      WNPZTWTXDXLXTXEAAWNQVJWDXAXDXRXTXGAWIWNCDEXFUGVKUHVLAWIWOCWMWNEXFWORZVMSV
+      NWFXQBXPWMWNXBXNVOAAWEXPNOVPVCVSUIVQWDCVRHWHWJWLWRVTUTACDEWAFGWIWOWGCWKXF
+      WKRYAWBSWC $.
+  $}
+
   ${
     $d A f $.  $d A x y $.  $d B x y $.  $d M x y $.  $d V f $.
     symgsubmefmnd.m $e |- M = ( EndoFMnd ` A ) $.
@@ -741935,6 +741997,17 @@ According to Wikipedia ("Endomorphism", 25-Jan-2024,
     $( The symmetric group on a set ` A ` is a submonoid of the monoid of
        endofunctions on ` A ` .  (Contributed by AV, 18-Feb-2024.) $)
     symgsubmefmnd $p |- ( A e. V -> B e. ( SubMnd ` M ) ) $=
+      ( vf wcel cv wf1o cab csubmnd cfv symgbas wf1 wfo cin eqeltrid inab abbii
+      wa df-f1o bicomi eqtr2i injsubmefmnd sursubmefmnd insubm syl2anc ) AEJZBA
+      AIKZLZIMZDNOZIABCGHPUKUNAAULQZIMZAAULRZIMZSZUOUTUPURUCZIMUNUPURIUAVAUMIUM
+      VAAAULUDUEUBUFUKUQUOJUSUOJUTUOJAIDEFUGAIDEFUHUQUSDUIUJTT $.
+
+    $( The symmetric group on a set ` A ` is a submonoid of the monoid of
+       endofunctions on ` A ` .  Alternate proof based on ~ submefmnd and not
+       on ~ injsubmefmnd and ~ sursubmefmnd .  (Contributed by AV,
+       18-Feb-2024.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    symgsubmefmndALT $p |- ( A e. V -> B e. ( SubMnd ` M ) ) $=
       ( vx vy vf wcel cmnd cbs cfv wss c0g cv syl eqid cplusg ccom cmpo csubmnd
       w3a wceq cgrp symggrp grpmnd wf1o cab cmap co nfv nfab1 nfcv abid wf f1of
       id elmapd syl5ibr syl5bi ssrd symgbas efmndbas 3sstr4g cid efmndid symgid