From ca97d9edd8be70f2e77235d70261474f7c28ef7d Mon Sep 17 00:00:00 2001 From: avekens Date: Sun, 25 Feb 2024 17:04:20 +0100 Subject: [PATCH] Submonoids of injectiv/surjective endofunctions MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ~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). --- discouraged | 2 ++ set.mm | 73 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 75 insertions(+) diff --git a/discouraged b/discouraged index 36b80e245e..844ca047fb 100755 --- 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 index 567d0f90f6..6182760a4b 100644 --- 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