From 914618bfe88ad452d12ecf35036cf5362aa7f6d4 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Fri, 20 Dec 2024 10:52:57 -0800 Subject: [PATCH 01/49] Add .g to iset.mm This is the syntax and df-mulg . Copied without change from set.mm. --- iset.mm | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/iset.mm b/iset.mm index 16271d6d3..6021bc6d3 100644 --- a/iset.mm +++ b/iset.mm @@ -146444,6 +146444,39 @@ since the target of the homomorphism (operator ` O ` in our model) need $} +$( +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + Group multiple operation +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + + The "group multiple" operation (if the group is multiplicative, also called + "group power" or "group exponentiation" operation), can be defined for + arbitrary magmas, if the multiplier/exponent is a nonnegative integer. See + also the definition in [Lang] p. 6, where an element ` x `(of a monoid) to + the power of a nonnegative integer ` n ` is defined and denoted by ` x ^ n `. + Definition ~ df-mulg , however, defines the group multiple for arbitrary + (i.e. also negative) integers. This is meaningful for groups only, and + requires Definition ~ df-minusg of the inverse operation ` invg ` . + +$) + + $c .g $. + + $( Extend class notation with a function mapping a group operation to the + multiple/power operation for the magma/group. $) + cmg $a class .g $. + + ${ + $d g n s x $. + $( Define the group multiple function, also known as group exponentiation + when viewed multiplicatively. (Contributed by Mario Carneiro, + 11-Dec-2014.) $) + df-mulg $a |- .g = ( g e. _V |-> ( n e. ZZ , x e. ( Base ` g ) |-> + if ( n = 0 , ( 0g ` g ) , [_ seq 1 ( ( +g ` g ) , ( NN X. { x } ) ) / s ]_ + if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) ) ) ) ) $. + $} + + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# The complex numbers as an algebraic extensible structure @@ -163657,6 +163690,9 @@ Norman Megill (2007) section 1.1.3. Megill then states, "A number of " -g"; althtmldef "-g" as "-g"; latexdef "-g" as "-_\mathrm{g}"; +htmldef ".g" as ".g"; + althtmldef ".g" as ".g"; + latexdef ".g" as "\cdot_\mathrm{g}"; htmldef "MndHom" as " MndHom "; althtmldef "MndHom" as " MndHom "; latexdef "MndHom" as " \mathrm{MndHom} "; From 90201bb98fbe9ff4523452259389775dd184b378 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Fri, 20 Dec 2024 11:28:49 -0800 Subject: [PATCH 02/49] Add mulgfvalg to iset.mm This is mulgfval from set.mm with a set existence condition added. The proof is adapted from the mulgfvalALT proof in set.mm and needs some intuitionizing related to the set existence condition. --- iset.mm | 27 +++++++++++++++++++++++++++ mmil.raw.html | 5 +++++ 2 files changed, 32 insertions(+) diff --git a/iset.mm b/iset.mm index 6021bc6d3..81622d2c1 100644 --- a/iset.mm +++ b/iset.mm @@ -146476,6 +146476,33 @@ since the target of the homomorphism (operator ` O ` in our model) need if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) ) ) ) ) $. $} + ${ + $d x w .0. n $. $d x w B n $. $d x w .+ n s $. $d x w n G s $. + $d x w n I s $. $d n x N $. $d n x S $. $d n x X $. + mulgval.b $e |- B = ( Base ` G ) $. + mulgval.p $e |- .+ = ( +g ` G ) $. + mulgval.o $e |- .0. = ( 0g ` G ) $. + mulgval.i $e |- I = ( invg ` G ) $. + mulgval.t $e |- .x. = ( .g ` G ) $. + $( Group multiple (exponentiation) operation. (Contributed by Mario + Carneiro, 11-Dec-2014.) $) + mulgfvalg $p |- ( G e. V -> .x. = ( n e. ZZ , x e. B |-> + if ( n = 0 , .0. , if ( 0 < n , + ( seq 1 ( .+ , ( NN X. { x } ) ) ` n ) , + ( I ` ( seq 1 ( .+ , ( NN X. { x } ) ) ` -u n ) ) ) ) ) ) $= + ( vs wcel cfv cz cbs cvv vw cmg cv cc0 wceq clt wbr csn cxp cseq cneg cif + cn c1 cmpo c0g cplusg cminusg csb df-mulg eqidd fveq2 eqtr4di seqex wa id + a1i seqeq2d sylan9eqr fveq1d simpl fveq2d fveq12d ifeq12d mpoeq123dv elex + csbied zex basfn funfvex funfni sylancr eqeltrid mpoexga fvmptd3 eqtrid + wfn ) FHPZDFUBQEARBEUCZUDUEZIUDWIUFUGZWICUMAUCUHUIZUNUJZQZWIUKZWMQZGQZULZ + ULZUOZNWHUAFEARUAUCZSQZWJXAUPQZOXAUQQZWLUNUJZWKWIOUCZQZWOXFQZXAURQZQZULZU + SZULZUOWTTUBTAUAEOUTXAFUEZEARXBXMRBWSXNRVAXNXBFSQZBXAFSVBJVCXNWJXCIXLWRXN + XCFUPQIXAFUPVBLVCXNOXEXKWRTXETPXNXDWLUNVDVGXNXFXEUEZVEZWKXGWNXJWQXQWIXFWM + XPXNXFXEWMXPVFXNXDCWLUNXNXDFUQQCXAFUQVBKVCVHVIZVJXQXHWPXIGXQXIFURQGXQXAFU + RXNXPVKVLMVCXQWOXFWMXRVJVMVNVQVNVOFHVPZWHRTPBTPWTTPVRWHBXOTJWHSTWGFTPXOTP + ZVSXSXTTFSFSVTWAWBWCEARBWSTTWDWBWEWF $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# diff --git a/mmil.raw.html b/mmil.raw.html index bdb5f67da..0a18a74df 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -10614,6 +10614,11 @@ the set.mm proof depends on prdsgrpd + + mulgfval , mulgfvalALT + ~ mulgfvalg + + df-cnfld and all theorems using CCfld none From 2a27e607d92be74aa6fec83186a887cc80f27400 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Fri, 20 Dec 2024 11:32:24 -0800 Subject: [PATCH 03/49] Add $j usage to mulgfval in set.mm This matches a statement already made in the comment about axiom usage. --- set.mm | 1 + 1 file changed, 1 insertion(+) diff --git a/set.mm b/set.mm index c50b9a0f0..e48c0fd99 100644 --- a/set.mm +++ b/set.mm @@ -230455,6 +230455,7 @@ since the target of the homomorphism (operator ` O ` in our model) need YGUVJTYJZUVJTPUYGUVJOBUJZYJUYHEAOBUVIUVJUVJUUKUUSHUVHUXBUUTUVDUVGUURUVCVG UVFGVGYRYRUUDUYGUYITUVJUYGUYIOTUJTUYGBTOUYGBUWFTIFUPYTUUEUUFOUUGUUHUUIUUJ UVJUULUUMUUNUUOUUP $. + $( $j usage 'mulgfval' avoids 'ax-rep'; $) $( Shorter proof of ~ mulgfval using ~ ax-rep . (Contributed by Mario Carneiro, 11-Dec-2014.) (Proof modification is discouraged.) From 680d1c210733a6d8375d0140ab5cb9aafd055e16 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Fri, 20 Dec 2024 16:38:38 -0800 Subject: [PATCH 04/49] Add ifcli , ifex to mmil.html --- mmil.raw.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mmil.raw.html b/mmil.raw.html index 0a18a74df..78efe4690 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -1911,7 +1911,7 @@ - ifcl , ifcld + ifcl , ifcld , ifcli , ifex ~ ifcldcd , ~ ifcldadc From 1c5f5d13651037a89e5dab81b9cc90e677ea6d05 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Fri, 20 Dec 2024 17:25:28 -0800 Subject: [PATCH 05/49] Add mulgval to iset.mm Stated as in set.mm. The proof needs a lot of intuitionizing but is able to follow roughly the outlines of the set.mm proof. --- iset.mm | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/iset.mm b/iset.mm index 81622d2c1..f480c39ab 100644 --- a/iset.mm +++ b/iset.mm @@ -146501,6 +146501,41 @@ since the target of the homomorphism (operator ` O ` in our model) need XPXNXFXEWMXPVFXNXDCWLUNXNXDFUQQCXAFUQVBKVCVHVIZVJXQXHWPXIGXQXIFURQGXQXAFU RXNXPVKVLMVCXQWOXFWMXRVJVMVNVQVNVOFHVPZWHRTPBTPWTTPVRWHBXOTJWHSTWGFTPXOTP ZVSXSXTTFSFSVTWAWBWCEARBWSTTWDWBWEWF $. + + mulgval.s $e |- S = seq 1 ( .+ , ( NN X. { X } ) ) $. + + ${ + $d .+ u v $. $d B u v $. $d G u v $. $d X u v $. + $( Value of the group multiple (exponentiation) operation. (Contributed + by Mario Carneiro, 11-Dec-2014.) $) + mulgval $p |- ( ( N e. ZZ /\ X e. B ) -> ( N .x. X ) = if ( N = 0 , .0. , + if ( 0 < N , ( S ` N ) , ( I ` ( S ` -u N ) ) ) ) ) $= + ( wcel wa cvv cc0 cn vn vx vu vv cz co wceq clt wbr cfv cneg cif basmex + adantl cv csn cxp cseq mulgfvalg simpl eqeq1d breq2d simpr sneqd xpeq2d + c1 cmpo seqeq3d eqtr4di fveq12d negeqd fveq2d ifbieq12d ifbieq2d simpll + simplr c0g fn0g funfvex funfni mpan eqeltrid ad2antlr wn nnuz fvconst2g + wfn wf 1zzd eqeltrd elexd adantlr simprl cplusg plusgslid slotex simprr + ovexg syl3anc feq1i sylibr ad5ant23 simp-4l sylanbrc ffvelrnd grpinvfng + seqf elnnz basfn fnex syl2anc ad3antlr znegcl ad4antr ztri3or0 ecase23d + cbs w3o cr zre lt0neg1d mpbid fvexg wdc 0zd zdclt ifcldadc zdceq ovmpod + simplll mpdan ) GUEPZHAPZQZERPZGHDUFGSUGZISGUHUIZGCUJZGUKZCUJZFUJZULZUL + ZUGYMYOYLHAEJUMUNYNYOQZUAUBGHUEAUAUOZSUGZISUUEUHUIZUUEBTUBUOZUPZUQZVFUR + ZUJZUUEUKZUUKUJZFUJZULZULZUUCDRYODUAUBUEAUUQVGUGYNUBABDUAEFRIJKLMNUSUNU + UEGUGZUUHHUGZQZUUQUUCUGUUDUUTUUFYPUUPUUBIUUTUUEGSUURUUSUTZVAUUTUUGYQUUL + UUOYRUUAUUTUUEGSUHUVAVBUUTUUEGUUKCUUTUUKBTHUPZUQZVFURZCUUTUUJUVCBVFUUTU + UIUVBTUUTUUHHUURUUSVCVDVEVHOVIZUVAVJUUTUUNYTFUUTUUMYSUUKCUVEUUTUUEGUVAV + KVJVLVMVNUNYLYMYOVOZYLYMYOVPUUDYPIUUBRYOIRPYNYPYOIEVQUJZRLVQRWGYOUVGRPZ + VRUVHREVQEVQVSVTWAWBWCUUDYPWDZQZYQYRUUARUVJYQQZTRGCYMYOTRCWHZYLUVIYQYMY + OQZTRUVDWHUVLUVMUCUDBRUVCVFTWEUVMWIYMUCUOZTPZUVNUVCUJZRPYOYMUVOQZUVPAUV + QUVPHATHUVNAWFYMUVOUTWJWKWLUVMUVNRPZUDUOZRPZQZQUVRBRPZUVTUVNUVSBUFRPUVM + UVRUVTWMYOUWBYMUWAYOBEWNUJRKEWNRWOWPWBWCUVMUVRUVTWQUVNUVSBRRRWRWSXGTRCU + VDOWTXAZXBUVKYLYQGTPYLYMYOUVIYQXCUVJYQVCGXHXDXEUVJYQWDZQZFRPZYTRPUUARPY + OUWFYNUVIUWDYOFAWGARPUWFAEFRJMXFYOAEXQUJZRJXQRWGYOUWGRPZXIUWHREXQEXQVSV + TWAWBARFXJXKXLUWETRYSCYMYOUVLYLUVIUWDUWCXBUWEYSUEPZSYSUHUIZYSTPYLUWIYMY + OUVIUWDGXMXNUWEGSUHUIZUWJUWEUWKYPYQUUDUVIUWDVPUVJUWDVCYLUWKYPYQXRYMYOUV + IUWDGXOXNXPUWEGYLGXSPYMYOUVIUWDGXTXNYAYBYSXHXDXEYTFRRYCXKUVJSUEPZYLYQYD + UVJYEYLYMYOUVIYJSGYFXKYGUUDYLUWLYPYDUVFUUDYEGSYHXKYGYIYK $. + $} $} From f1f67edcbd3e6d30bdaca42c06b2fa5a83b19483 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sat, 21 Dec 2024 22:22:19 -0700 Subject: [PATCH 06/49] Add mulgfng to iset.mm This is mulgfn from set.mm with an additional set existence condition. The proof is largely taken from the iset.mm proof of mulgval . --- iset.mm | 29 +++++++++++++++++++++++++++++ mmil.raw.html | 5 +++++ 2 files changed, 34 insertions(+) diff --git a/iset.mm b/iset.mm index f480c39ab..c23c4617a 100644 --- a/iset.mm +++ b/iset.mm @@ -146538,6 +146538,35 @@ since the target of the homomorphism (operator ` O ` in our model) need $} $} + ${ + $d B u v n x $. $d G u v n x $. $d V u v n x $. + mulgfn.b $e |- B = ( Base ` G ) $. + mulgfn.t $e |- .x. = ( .g ` G ) $. + $( Functionality of the group multiple operation. (Contributed by Mario + Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) $) + mulgfng $p |- ( G e. V -> .x. Fn ( ZZ X. B ) ) $= + ( vn vx wcel cz wfn cv cc0 c0g cfv cn cvv wa syl ad2antrr vu cxp wceq clt + vv wbr cplusg csn c1 cseq cneg cminusg cmpo wral elex fn0g funfvex funfni + cif mpan wn wf nnuz 1zzd fvconst2g simpl eqeltrd adantll simprl plusgslid + elexd co slotex simprr ovexg syl3anc seqf adantrl simpr sylanbrc ffvelrnd + elnnz eqid grpinvfng basfn eqeltrid fnex syl2anc ad3antrrr znegcld simplr + cbs w3o ztri3or0 ecase23d zred lt0neg1d mpbid fvexg wdc 0zd simplrl zdclt + cr ifcldadc zdceq ralrimivva fnmpo mulgfvalg fneq1d mpbird ) CDIZBJAUBZKG + HJAGLZMUCZCNOZMXNUDUFZXNCUGOZPHLZUHUBZUIUJZOZXNUKZYAOZCULOZOZUSZUSZUMZXMK + ZXLYHQIZHAUNGJUNYJXLYKGHJAXLXNJIZXSAIZRZRZXOXPYGQXLXPQIZYNXOXLCQIZYPCDUOZ + NQKYQYPUPYPQCNCNUQURUTSTYOXOVAZRZXQYBYFQYTXQRZPQXNYAYOPQYAVBZYSXQXLYMUUBY + LXLYMRZUAUEXRQXTUIPVCUUCVDYMUALZPIZUUDXTOZQIXLYMUUERZUUFAUUGUUFXSAPXSUUDA + VEYMUUEVFVGVKVHUUCUUDQIZUELZQIZRZRUUHXRQIZUUJUUDUUIXRVLQIUUCUUHUUJVIXLUUL + YMUUKCUGDVJVMTUUCUUHUUJVNUUDUUIXRQQQVOVPVQVRZTUUAYLXQXNPIYOYLYSXQXLYLYMVI + ZTYTXQVSXNWBVTWAYTXQVAZRZYEQIZYDQIYFQIXLUUQYNYSUUOXLYEAKAQIZUUQACYEDEYEWC + ZWDXLYQUURYRYQACWLOZQEWLQKYQUUTQIZWEUVAQCWLCWLUQURUTWFSAQYEWGWHWIUUPPQYCY + AYOUUBYSUUOUUMTUUPYCJIZMYCUDUFZYCPIYOUVBYSUUOYOXNUUNWJTUUPXNMUDUFZUVCUUPU + VDXOXQYOYSUUOWKYTUUOVSYOUVDXOXQWMZYSUUOYOYLUVEUUNXNWNSTWOUUPXNYOXNXDIYSUU + OYOXNUUNWPTWQWRYCWBVTWAYDYEQQWSWHYTMJIZYLXQWTYTXAXLYLYMYSXBMXNXCWHXEYOYLU + VFXOWTUUNYOXAXNMXFWHXEXGGHJAYHYIQYIWCXHSXLXMBYIHAXRBGCYEDXPEXRWCXPWCUUSFX + IXJXK $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# diff --git a/mmil.raw.html b/mmil.raw.html index 78efe4690..eb0f5375e 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -10619,6 +10619,11 @@ ~ mulgfvalg + + mulgfn + ~ mulgfng + + df-cnfld and all theorems using CCfld none From 8eb4a64dd4d836a97ab787a5e8b5202d52a878c9 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 06:37:35 -0700 Subject: [PATCH 07/49] add mulgfvi to mmil.html --- mmil.raw.html | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index eb0f5375e..590f93cc6 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -10624,6 +10624,12 @@ ~ mulgfng + + mulgfvi + none + the set.mm proof uses case elimination on ` G e. _V ` + + df-cnfld and all theorems using CCfld none From d0901e5d17df3edbece076ef053dcda6bf2cf28b Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 06:53:12 -0700 Subject: [PATCH 08/49] copy mulg0 from set.mm to iset.mm --- iset.mm | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/iset.mm b/iset.mm index c23c4617a..5bc8c388d 100644 --- a/iset.mm +++ b/iset.mm @@ -146567,6 +146567,19 @@ since the target of the homomorphism (operator ` O ` in our model) need IXJXK $. $} + ${ + mulg0.b $e |- B = ( Base ` G ) $. + mulg0.o $e |- .0. = ( 0g ` G ) $. + mulg0.t $e |- .x. = ( .g ` G ) $. + $( Group multiple (exponentiation) operation at zero. (Contributed by + Mario Carneiro, 11-Dec-2014.) $) + mulg0 $p |- ( X e. B -> ( 0 .x. X ) = .0. ) $= + ( cc0 cz wcel co wceq 0z wa clt wbr cfv cif eqid cplusg csn cxp cseq cneg + cn c1 cminusg mulgval iftruei eqtrdi mpan ) IJKZDAKZIDBLZEMNUMUNOUOIIMZEI + IPQICUARZUFDUBUCUGUDZRIUEURRCUHRZRSZSEAUQURBCUSIDEFUQTGUSTHURTUIUPEUTITUJ + UKUL $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# From 569c3512b8ce9b477bd03ce5f9f7e8b7ad508d0f Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 06:54:08 -0700 Subject: [PATCH 09/49] copy mulgnn from set.mm to iset.mm --- iset.mm | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/iset.mm b/iset.mm index 5bc8c388d..7d4e0583d 100644 --- a/iset.mm +++ b/iset.mm @@ -146580,6 +146580,20 @@ since the target of the homomorphism (operator ` O ` in our model) need UKUL $. $} + ${ + mulgnn.b $e |- B = ( Base ` G ) $. + mulgnn.p $e |- .+ = ( +g ` G ) $. + mulgnn.t $e |- .x. = ( .g ` G ) $. + mulgnn.s $e |- S = seq 1 ( .+ , ( NN X. { X } ) ) $. + $( Group multiple (exponentiation) operation at a positive integer. + (Contributed by Mario Carneiro, 11-Dec-2014.) $) + mulgnn $p |- ( ( N e. NN /\ X e. B ) -> ( N .x. X ) = ( S ` N ) ) $= + ( cn wcel wa cc0 wceq cfv cif eqid eqtrd c0g clt wbr cneg cminusg mulgval + co cz nnz sylan nnne0 neneqd iffalsed nngt0 iftrued adantr ) FLMZGAMZNFGD + UGZFOPZEUAQZOFUBUCZFCQZFUDCQEUEQZQZRZRZVCUQFUHMURUSVGPFUIABCDEVDFGVAHIVAS + VDSJKUFUJUQVGVCPURUQVGVFVCUQUTVAVFUQFOFUKULUMUQVBVCVEFUNUOTUPT $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# From ce9b6f0fe5c0d1dfa5f52045065bfec4a67f6541 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 07:55:20 -0700 Subject: [PATCH 10/49] add mulgnngsum to mmil.html --- mmil.raw.html | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index 590f93cc6..2cd9f9cde 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -10630,6 +10630,12 @@ the set.mm proof uses case elimination on ` G e. _V ` + + mulgnngsum + none + the set.mm proof uses gsumval2 + + df-cnfld and all theorems using CCfld none From 35150b9a997030d07f6c9ecff9872232e08de0ef Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 08:02:48 -0700 Subject: [PATCH 11/49] add mulgnn0gsum to mmil.html --- mmil.raw.html | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index 2cd9f9cde..df49ec298 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -10636,6 +10636,12 @@ the set.mm proof uses gsumval2 + + mulgnn0gsum + none + the set.mm proof uses mulgnngsum and gsum0 + + df-cnfld and all theorems using CCfld none From 3a62747a4a332543202af968bbb95830d0733ac1 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 21:42:18 -0700 Subject: [PATCH 12/49] Add mulg1 to iset.mm Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof. --- iset.mm | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/iset.mm b/iset.mm index 7d4e0583d..890f063a3 100644 --- a/iset.mm +++ b/iset.mm @@ -146594,6 +146594,24 @@ since the target of the homomorphism (operator ` O ` in our model) need VDSJKUFUJUQVGVCPURUQVGVFVCUQUTVAVFUQFOFUKULUMUQVBVCVEFUNUOTUPT $. $} + ${ + mulg1.b $e |- B = ( Base ` G ) $. + mulg1.m $e |- .x. = ( .g ` G ) $. + ${ + $d B u v $. $d G u v $. $d X u v $. + $( Group multiple (exponentiation) operation at one. (Contributed by + Mario Carneiro, 11-Dec-2014.) $) + mulg1 $p |- ( X e. B -> ( 1 .x. X ) = X ) $= + ( vu vv wcel c1 co cplusg cfv cn wceq 1nn eqid cvv cv wa csn cxp mulgnn + cseq mpan 1zzd cuz elnnuz fvconst2g simpl eqeltrd elexd sylan2br simprl + basmex plusgslid slotex adantr simprr ovexg syl3anc seq3-1 mpan2 3eqtrd + syl ) DAIZJDBKZJCLMZNDUAUBZJUDZMZJVIMZDJNIZVFVGVKOPAVHVJBCJDEVHQFVJQUCU + EVFGHVHRVIJVFUFGSZJUGMIVFVNNIZVNVIMZRIVNUHVFVOTZVPAVQVPDANDVNAUIVFVOUJU + KULUMVFVNRIZHSZRIZTZTVRVHRIZVTVNVSVHKRIVFVRVTUNVFWBWAVFCRIWBDACEUOCLRUP + UQVEURVFVRVTUSVNVSVHRRRUTVAVBVFVMVLDOPNDJAUIVCVD $. + $} + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# From b7eae8e697328cb4cbe8aa6115d4e71bd2843832 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 22:06:36 -0700 Subject: [PATCH 13/49] Add mulgnnp1 to iset.mm Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof. --- iset.mm | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/iset.mm b/iset.mm index 890f063a3..5534ae767 100644 --- a/iset.mm +++ b/iset.mm @@ -146610,6 +146610,25 @@ since the target of the homomorphism (operator ` O ` in our model) need KULUMVFVNRIZHSZRIZTZTVRVHRIZVTVNVSVHKRIVFVRVTUNVFWBWAVFCRIWBDACEUOCLRUP UQVEURVFVRVTUSVNVSVHRRRUTVAVBVFVMVLDOPNDJAUIVCVD $. $} + + ${ + $d .+ u v $. $d B u v $. $d N u v $. $d X u v $. + mulgnnp1.p $e |- .+ = ( +g ` G ) $. + $( Group multiple (exponentiation) operation at a successor. + (Contributed by Mario Carneiro, 11-Dec-2014.) $) + mulgnnp1 $p |- ( ( N e. NN /\ X e. B ) -> + ( ( N + 1 ) .x. X ) = ( ( N .x. X ) .+ X ) ) $= + ( vu vv cn wcel wa c1 co cfv cvv simpl nnuz caddc csn cxp cseq eleqtrdi + cv simplr simpr eleqtrrdi fvconst2g eqeltrd elexd syl2anc simprl basmex + cuz cplusg plusgslid slotex eqeltrid syl ad2antlr simprr syl3anc seq3p1 + ovexg wceq id peano2nn syl2anr oveq2d eqtrd mulgnn sylan oveq1d 3eqtr4d + eqid ) ELMZFAMZNZEOUAPZBLFUBUCZOUDZQZEWCQZFBPZWAFCPZEFCPZFBPVTWDWEWAWBQ + ZBPWFVTJKBRWBOEVTELOUPQZVRVSSTUEVTJUFZWJMZNZVSWKLMZWKWBQZRMVRVSWLUGWMWK + WJLVTWLUHTUIVSWNNZWOAWPWOFALFWKAUJVSWNSUKULUMVTWKRMZKUFZRMZNZNWQBRMZWSW + KWRBPRMVTWQWSUNVSXAVRWTVSDRMZXAFADGUOXBBDUQQRIDUQRURUSUTVAVBVTWQWSVCWKW + RBRRRVFVDVEVTWIFWEBVSVSWALMZWIFVGVRVSVHEVIZLFWAAUJVJVKVLVRXCVSWGWDVGXDA + BWCCDWAFGIHWCVQZVMVNVTWHWEFBABWCCDEFGIHXEVMVOVP $. + $} $} From ebf188c77bf3c8ee6ab2c7aa2133dbac330503ba Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 22:08:37 -0700 Subject: [PATCH 14/49] copy mulg2 from set.mm to iset.mm --- iset.mm | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/iset.mm b/iset.mm index 5534ae767..6dbf09c62 100644 --- a/iset.mm +++ b/iset.mm @@ -146628,6 +146628,13 @@ since the target of the homomorphism (operator ` O ` in our model) need KWRBPRMVTWQWSUNVSXAVRWTVSDRMZXAFADGUOXBBDUQQRIDUQRURUSUTVAVBVTWQWSVCWKW RBRRRVFVDVEVTWIFWEBVSVSWALMZWIFVGVRVSVHEVIZLFWAAUJVJVKVLVRXCVSWGWDVGXDA BWCCDWAFGIHWCVQZVMVNVTWHWEFBABWCCDEFGIHXEVMVOVP $. + + $( Group multiple (exponentiation) operation at two. (Contributed by + Mario Carneiro, 15-Oct-2015.) $) + mulg2 $p |- ( X e. B -> ( 2 .x. X ) = ( X .+ X ) ) $= + ( wcel c2 co c1 caddc df-2 oveq1i cn wceq 1nn mulgnnp1 mpan mulg1 eqtrd + eqtrid oveq1d ) EAIZJECKZLECKZEBKZEEBKUEUFLLMKZECKZUHJUIECNOLPIUEUJUHQR + ABCDLEFGHSTUCUEUGEEBACDEFGUAUDUB $. $} $} From ba4590a2958cc993193dd7bf32026494425fdaa3 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 22:09:41 -0700 Subject: [PATCH 15/49] copy mulgnegnn from set.mm to iset.mm --- iset.mm | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/iset.mm b/iset.mm index 6dbf09c62..1e0d0aea0 100644 --- a/iset.mm +++ b/iset.mm @@ -146636,6 +146636,21 @@ since the target of the homomorphism (operator ` O ` in our model) need eqtrid oveq1d ) EAIZJECKZLECKZEBKZEEBKUEUFLLMKZECKZUHJUIECNOLPIUEUJUHQR ABCDLEFGHSTUCUEUGEEBACDEFGUAUDUB $. $} + + mulgnegnn.i $e |- I = ( invg ` G ) $. + $( Group multiple (exponentiation) operation at a negative integer. + (Contributed by Mario Carneiro, 11-Dec-2014.) $) + mulgnegnn $p |- ( ( N e. NN /\ X e. B ) -> + ( -u N .x. X ) = ( I ` ( N .x. X ) ) ) $= + ( cn wcel cneg cfv co wceq fveq2d cc0 clt wbr eqid wa cplusg csn cxp cseq + c1 nncn negnegd adantr c0g cif cz nnnegz mulgval sylan wne wn nnne0 cc wb + negeq0 necon3abid syl mpbid iffalsed cr renegcld nngt0 lt0neg2d wi ltnsym + nnre 0re mpan2 sylc eqtrd mulgnn 3eqtr4d ) EJKZFAKZUAZELZLZCUBMZJFUCUDUFU + EZMZDMZEWEMZDMWBFBNZEFBNZDMWAWFWHDWAWCEWEVSWCEOVTVSEEUGZUHUIPPWAWIWBQOZCU + JMZQWBRSZWBWEMZWGUKZUKZWGVSWBULKVTWIWQOEUMAWDWEBCDWBFWMGWDTZWMTIHWETZUNUO + VSWQWGOVTVSWQWPWGVSWLWMWPVSEQUPZWLUQZEURVSEUSKZWTXAUTWKXBWLEQEVAVBVCVDVEV + SWNWOWGVSWBVFKZWBQRSZWNUQZVSEEVLZVGVSQERSXDEVHVSEXFVIVDXCQVFKXDXEVJVMWBQV + KVNVOVEVPUIVPWAWJWHDAWDWEBCEFGWRHWSVQPVR $. $} From cb8bdd8218571f0cba4a0b6b23beafb9b5f240ac Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 22:10:56 -0700 Subject: [PATCH 16/49] copy mulgnn0p1 from set.mm to iset.mm --- iset.mm | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/iset.mm b/iset.mm index 1e0d0aea0..dfdcda74c 100644 --- a/iset.mm +++ b/iset.mm @@ -146653,6 +146653,23 @@ since the target of the homomorphism (operator ` O ` in our model) need KVNVOVEVPUIVPWAWJWHDAWDWEBCEFGWRHWSVQPVR $. $} + ${ + mulgnn0p1.b $e |- B = ( Base ` G ) $. + mulgnn0p1.t $e |- .x. = ( .g ` G ) $. + mulgnn0p1.p $e |- .+ = ( +g ` G ) $. + $( Group multiple (exponentiation) operation at a successor, extended to + ` NN0 ` . (Contributed by Mario Carneiro, 11-Dec-2014.) $) + mulgnn0p1 $p |- ( ( G e. Mnd /\ N e. NN0 /\ X e. B ) -> + ( ( N + 1 ) .x. X ) = ( ( N .x. X ) .+ X ) ) $= + ( cmnd wcel c1 caddc co wceq cc0 wa adantl oveq1d oveq1 cn0 w3a cn simpl3 + simpr mulgnnp1 syl2anc c0g eqid mndlid mulg0 mulg1 3eqtr4rd 3adant2 1e0p1 + cfv eqtr4di eqeq12d syl5ibrcom imp wo simp2 elnn0 sylib mpjaodan ) DJKZEU + AKZFAKZUBZEUCKZELMNZFCNZEFCNZFBNZOZEPOZVIVJQVJVHVOVIVJUEVFVGVHVJUDABCDEFG + HIUFUGVIVPVOVIVOVPLFCNZPFCNZFBNZOZVFVHVTVGVFVHQZDUHUPZFBNFVSVQABDFWBGIWBU + IZUJWAVRWBFBVHVRWBOVFACDFWBGWCHUKRSVHVQFOVFACDFGHULRUMUNVPVLVQVNVSVPVKLFC + VPVKPLMNLEPLMTUOUQSVPVMVRFBEPFCTSURUSUTVIVGVJVPVAVFVGVHVBEVCVDVE $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# From 0a8a69874c33109772ba76e7971d96fc4af9e14e Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 22:40:45 -0700 Subject: [PATCH 17/49] Add mulgnnsubcl to iset.mm Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof. --- iset.mm | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/iset.mm b/iset.mm index dfdcda74c..9ac7a79eb 100644 --- a/iset.mm +++ b/iset.mm @@ -146670,6 +146670,26 @@ since the target of the homomorphism (operator ` O ` in our model) need VPVKPLMNLEPLMTUOUQSVPVMVRFBEPFCTSURUSUTVIVGVJVPVAVFVGVHVBEVCVDVE $. $} + ${ + $d x y .+ $. $d x y B $. $d x y G $. $d x I $. $d x y N $. $d x y S $. + $d x y ph $. $d x .x. $. $d x y X $. + mulgnnsubcl.b $e |- B = ( Base ` G ) $. + mulgnnsubcl.t $e |- .x. = ( .g ` G ) $. + mulgnnsubcl.p $e |- .+ = ( +g ` G ) $. + mulgnnsubcl.g $e |- ( ph -> G e. V ) $. + mulgnnsubcl.s $e |- ( ph -> S C_ B ) $. + mulgnnsubcl.c $e |- ( ( ph /\ x e. S /\ y e. S ) -> ( x .+ y ) e. S ) $. + $( Closure of the group multiple (exponentiation) operation in a + subsemigroup. (Contributed by Mario Carneiro, 10-Jan-2015.) $) + mulgnnsubcl $p |- ( ( ph /\ N e. NN /\ X e. S ) -> ( N .x. X ) e. S ) $= + ( cn wcel co w3a csn cxp c1 cseq cfv wceq simp2 wss 3ad2ant1 simp3 sseldd + eqid mulgnn syl2anc nnuz 1zzd cv fvconst2g sylan simpl3 eqeltrd 3ad2antl1 + wa 3expb seqf ffvelrnd ) AIRSZKFSZUAZIKGTZIERKUBUCZUDUEZUFZFVJVHKDSVKVNUG + AVHVIUHZVJFDKAVHFDUIVIPUJAVHVIUKZULDEVMGHIKLNMVMUMUNUOVJRFIVMVJBCEFVLUDRU + PVJUQVJBURZRSZVDVQVLUFZKFVJVIVRVSKUGVPRKVQFUSUTAVHVIVRVAVBAVHVQFSZCURZFSZ + VDVQWAETFSZVIAVTWBWCQVEVCVFVOVGVB $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# From fd930363228ab8a13a98ba02ebaeffdd29e84f24 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 22:44:33 -0700 Subject: [PATCH 18/49] copy mulgnn0subcl from set.mm to iset.mm --- iset.mm | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/iset.mm b/iset.mm index 9ac7a79eb..473babcef 100644 --- a/iset.mm +++ b/iset.mm @@ -146688,6 +146688,18 @@ since the target of the homomorphism (operator ` O ` in our model) need AVHVIUHZVJFDKAVHFDUIVIPUJAVHVIUKZULDEVMGHIKLNMVMUMUNUOVJRFIVMVJBCEFVLUDRU PVJUQVJBURZRSZVDVQVLUFZKFVJVIVRVSKUGVPRKVQFUSUTAVHVIVRVAVBAVHVQFSZCURZFSZ VDVQWAETFSZVIAVTWBWCQVEVCVFVOVGVB $. + + mulgnn0subcl.z $e |- .0. = ( 0g ` G ) $. + mulgnn0subcl.c $e |- ( ph -> .0. e. S ) $. + $( Closure of the group multiple (exponentiation) operation in a submonoid. + (Contributed by Mario Carneiro, 10-Jan-2015.) $) + mulgnn0subcl $p |- ( ( ph /\ N e. NN0 /\ X e. S ) -> ( N .x. X ) e. S ) $= + ( cn0 wcel w3a cn co wceq mulgnnsubcl 3expa an32s 3adantl2 oveq1 3ad2ant1 + cc0 wa wss simp3 sseldd mulg0 syl sylan9eqr adantr eqeltrd wo simp2 elnn0 + sylib mpjaodan ) AIUAUBZKFUBZUCZIUDUBZIKGUEZFUBZIUMUFZAVIVKVMVHAVKVIVMAVK + VIVMABCDEFGHIJKMNOPQRUGUHUIUJVJVNUNVLLFVNVJVLUMKGUEZLIUMKGUKVJKDUBVOLUFVJ + FDKAVHFDUOVIQULAVHVIUPUQDGHKLMSNURUSUTVJLFUBZVNAVHVPVITULVAVBVJVHVKVNVCAV + HVIVDIVEVFVG $. $} From 521b429e306f3144efe17ed056d6236acd200cb9 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 22:45:04 -0700 Subject: [PATCH 19/49] copy mulgsubcl from set.mm to iset.mm --- iset.mm | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/iset.mm b/iset.mm index 473babcef..a052205bb 100644 --- a/iset.mm +++ b/iset.mm @@ -146700,6 +146700,21 @@ since the target of the homomorphism (operator ` O ` in our model) need VIVMABCDEFGHIJKMNOPQRUGUHUIUJVJVNUNVLLFVNVJVLUMKGUEZLIUMKGUKVJKDUBVOLUFVJ FDKAVHFDUOVIQULAVHVIUPUQDGHKLMSNURUSUTVJLFUBZVNAVHVPVITULVAVBVJVHVKVNVCAV HVIVDIVEVFVG $. + + mulgsubcl.i $e |- I = ( invg ` G ) $. + mulgsubcl.c $e |- ( ( ph /\ x e. S ) -> ( I ` x ) e. S ) $. + $( Closure of the group multiple (exponentiation) operation in a subgroup. + (Contributed by Mario Carneiro, 10-Jan-2015.) $) + mulgsubcl $p |- ( ( ph /\ N e. ZZ /\ X e. S ) -> ( N .x. X ) e. S ) $= + ( cz wcel w3a cn0 co cr cn wa mulgnn0subcl 3expa an32s 3adantl2 cfv simp2 + cneg adantr zcnd negnegd oveq1d wceq id wss 3ad2ant1 simp3 sseldd syl2anr + mulgnegnn eqtr3d cv fveq2 eleq1d wral mulgnnsubcl rspcdva eqeltrd adantrl + ralrimiva wo elznn0nn sylib mpjaodan ) AJUDUEZLFUEZUFZJUGUEZJLGUHZFUEZJUI + UEZJURZUJUEZUKZAWFWHWJWEAWHWFWJAWHWFWJABCDEFGHJKLMNOPQRSTUAULUMUNUOWGWMWJ + WKWGWMUKZWIWLLGUHZIUPZFWOWLURZLGUHZWIWQWOWRJLGWOJWOJWGWEWMAWEWFUQZUSUTVAV + BWMWMLDUEWSWQVCWGWMVDWGFDLAWEFDVEWFRVFAWEWFVGVHDGHIWLLNOUBVJVIVKWOBVLZIUP + ZFUEZWQFUEBFWPXAWPVCXBWQFXAWPIVMVNWGXCBFVOZWMAWEXDWFAXCBFUCVTVFUSAWFWMWPF + UEZWEAWMWFXEAWMWFXEABCDEFGHWLKLNOPQRSVPUMUNUOVQVRVSWGWEWHWNWAWTJWBWCWD $. $} From 7631d0f96d2e6c1229edae97418d1adeef0178ad Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 22:46:07 -0700 Subject: [PATCH 20/49] copy mulgnncl from set.mm to iset.mm --- iset.mm | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/iset.mm b/iset.mm index a052205bb..dc2713c98 100644 --- a/iset.mm +++ b/iset.mm @@ -146717,6 +146717,18 @@ since the target of the homomorphism (operator ` O ` in our model) need UEZWEAWMWFXEAWMWFXEABCDEFGHWLKLNOPQRSVPUMUNUOVQVRVSWGWEWHWNWAWTJWBWCWD $. $} + ${ + $d x y B $. $d x y G $. $d x y N $. $d x .x. $. $d x y X $. + mulgnncl.b $e |- B = ( Base ` G ) $. + mulgnncl.t $e |- .x. = ( .g ` G ) $. + $( Closure of the group multiple (exponentiation) operation for a positive + multiplier in a magma. (Contributed by Mario Carneiro, 11-Dec-2014.) + (Revised by AV, 29-Aug-2021.) $) + mulgnncl $p |- ( ( G e. Mgm /\ N e. NN /\ X e. B ) -> ( N .x. X ) e. B ) $= + ( vx vy cmgm wcel cplusg cfv eqid id ssidd cv mgmcl mulgnnsubcl ) CJKZHIA + CLMZABCDJEFGUANZTOTAPACHQIQUAFUBRS $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# From be2236528a9067d57e162bcb6f7425fcc4fdabd9 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 22:47:00 -0700 Subject: [PATCH 21/49] copy mulgnn0cl from set.mm to iset.mm --- iset.mm | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/iset.mm b/iset.mm index dc2713c98..160257664 100644 --- a/iset.mm +++ b/iset.mm @@ -146727,6 +146727,15 @@ since the target of the homomorphism (operator ` O ` in our model) need mulgnncl $p |- ( ( G e. Mgm /\ N e. NN /\ X e. B ) -> ( N .x. X ) e. B ) $= ( vx vy cmgm wcel cplusg cfv eqid id ssidd cv mgmcl mulgnnsubcl ) CJKZHIA CLMZABCDJEFGUANZTOTAPACHQIQUAFUBRS $. + + $( Closure of the group multiple (exponentiation) operation for a + nonnegative multiplier in a monoid. (Contributed by Mario Carneiro, + 11-Dec-2014.) $) + mulgnn0cl $p |- ( ( G e. Mnd /\ N e. NN0 /\ X e. B ) -> + ( N .x. X ) e. B ) $= + ( vx vy cmnd wcel cplusg cfv c0g eqid id ssidd cv mndcl mndidcl + mulgnn0subcl ) CJKZHIACLMZABCDJECNMZFGUCOZUBPUBAQAUCCHRIRFUESUDOZACUDFUFT + UA $. $} From 0b5e351cc41ac7199dbdb2225378b740d175d8e3 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 22:47:34 -0700 Subject: [PATCH 22/49] copy mulgcl from set.mm to iset.mm --- iset.mm | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/iset.mm b/iset.mm index 160257664..3a3aed27b 100644 --- a/iset.mm +++ b/iset.mm @@ -146736,6 +146736,13 @@ since the target of the homomorphism (operator ` O ` in our model) need ( vx vy cmnd wcel cplusg cfv c0g eqid id ssidd cv mndcl mndidcl mulgnn0subcl ) CJKZHIACLMZABCDJECNMZFGUCOZUBPUBAQAUCCHRIRFUESUDOZACUDFUFT UA $. + + $( Closure of the group multiple (exponentiation) operation. (Contributed + by Mario Carneiro, 11-Dec-2014.) $) + mulgcl $p |- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( N .x. X ) e. B ) $= + ( vx vy cgrp wcel cplusg cfv cminusg c0g eqid id ssidd cv grpcl mulgsubcl + grpidcl grpinvcl ) CJKZHIACLMZABCCNMZDJECOMZFGUEPZUDQUDARAUECHSZISFUHTUGP + ZACUGFUJUBUFPZACUFUIFUKUCUA $. $} From f382ea1356adc4f97ec1b5b635c93e30eb2aaf8f Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 22:48:29 -0700 Subject: [PATCH 23/49] copy mulgneg from set.mm to iset.mm --- iset.mm | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/iset.mm b/iset.mm index 3a3aed27b..75caf1e01 100644 --- a/iset.mm +++ b/iset.mm @@ -146743,6 +146743,24 @@ since the target of the homomorphism (operator ` O ` in our model) need ( vx vy cgrp wcel cplusg cfv cminusg c0g eqid id ssidd cv grpcl mulgsubcl grpidcl grpinvcl ) CJKZHIACLMZABCCNMZDJECOMZFGUEPZUDQUDARAUECHSZISFUHTUGP ZACUGFUJUBUFPZACUFUIFUKUCUA $. + + mulgneg.i $e |- I = ( invg ` G ) $. + $( Group multiple (exponentiation) operation at a negative integer. + (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by Mario Carneiro, + 11-Dec-2014.) $) + mulgneg $p |- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> + ( -u N .x. X ) = ( I ` ( N .x. X ) ) ) $= + ( wcel cz cneg co cfv wceq wa cc0 simpl3 syl2anc oveq1d cgrp w3a cr cn wo + cn0 elnn0 simpr mulgnegnn c0g simpl1 eqid grpinvid syl mulg0 eqtrd fveq2d + negeqd neg0 eqtrdi 3eqtr4rd jaodan sylan2b simprr mulgcl grpinvinv simprl + nnzd syl3anc recnd negnegd eqtr3d simp2 elznn0nn sylib mpjaodan ) CUAJZEK + JZFAJZUBZEUFJZELZFBMZEFBMZDNZOZEUCJZWBUDJZPZWAVTEUDJZEQOZUEWFEUGVTWJWFWKV + TWJPWJVSWFVTWJUHVQVRVSWJRABCDEFGHIUISVTWKPZCUJNZDNZWMWEWCWLVQWNWMOVQVRVSW + KUKCDWMWMULZIUMUNWLWDWMDWLWDQFBMZWMWLEQFBVTWKUHZTWLVSWPWMOVQVRVSWKRABCFWM + GWOHUOUNZUPUQWLWCWPWMWLWBQFBWLWBQLQWLEQWQURUSUTTWRUPVAVBVCVTWIPZWCDNZDNZW + CWEWSVQWCAJZXAWCOVQVRVSWIUKZWSVQWBKJVSXBXCWSWBVTWGWHVDZVHVQVRVSWIRZABCWBF + GHVEVIACDWCGIVFSWSWTWDDWSWBLZFBMZWTWDWSWHVSXGWTOXDXEABCDWBFGHIUISWSXFEFBW + SEWSEVTWGWHVGVJVKTVLUQVLVTVRWAWIUEVQVRVSVMEVNVOVP $. $} From ca55fc6e5ae7bdf07b86c0da6bd191a5b758d6fd Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 22:50:02 -0700 Subject: [PATCH 24/49] copy mulgnegneg from set.mm to iset.mm --- iset.mm | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/iset.mm b/iset.mm index 75caf1e01..d8c986d71 100644 --- a/iset.mm +++ b/iset.mm @@ -146761,6 +146761,15 @@ since the target of the homomorphism (operator ` O ` in our model) need CWEWSVQWCAJZXAWCOVQVRVSWIUKZWSVQWBKJVSXBXCWSWBVTWGWHVDZVHVQVRVSWIRZABCWBF GHVEVIACDWCGIVFSWSWTWDDWSWBLZFBMZWTWDWSWHVSXGWTOXDXEABCDWBFGHIUISWSXFEFBW SEWSEVTWGWHVGVJVKTVLUQVLVTVRWAWIUEVQVRVSVMEVNVOVP $. + + $( The inverse of a negative group multiple is the positive group multiple. + (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, + 30-Aug-2021.) $) + mulgnegneg $p |- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) + -> ( I ` ( -u N .x. X ) ) = ( N .x. X ) ) $= + ( cgrp wcel cz w3a cneg co cfv mulgneg fveq2d wceq simp1 mulgcl grpinvinv + syl2anc eqtrd ) CJKZELKZFAKZMZENFBOZDPEFBOZDPZDPZUJUHUIUKDABCDEFGHIQRUHUE + UJAKULUJSUEUFUGTABCEFGHUAACDUJGIUBUCUD $. $} From 0d5b8199ca13093006cd6c37db9f2bca46465b59 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 22:50:54 -0700 Subject: [PATCH 25/49] copy mulgm1 from set.mm to iset.mm --- iset.mm | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/iset.mm b/iset.mm index d8c986d71..a3dee3d3d 100644 --- a/iset.mm +++ b/iset.mm @@ -146770,6 +146770,14 @@ since the target of the homomorphism (operator ` O ` in our model) need ( cgrp wcel cz w3a cneg co cfv mulgneg fveq2d wceq simp1 mulgcl grpinvinv syl2anc eqtrd ) CJKZELKZFAKZMZENFBOZDPEFBOZDPZDPZUJUHUIUKDABCDEFGHIQRUHUE UJAKULUJSUEUFUGTABCEFGHUAACDUJGIUBUCUD $. + + $( Group multiple (exponentiation) operation at negative one. (Contributed + by Paul Chapman, 17-Apr-2009.) (Revised by Mario Carneiro, + 20-Dec-2014.) $) + mulgm1 $p |- ( ( G e. Grp /\ X e. B ) -> ( -u 1 .x. X ) = ( I ` X ) ) $= + ( cgrp wcel wa c1 cneg co cfv cz wceq 1z mulgneg mp3an2 adantl fveq2d + mulg1 eqtrd ) CIJZEAJZKZLMEBNZLEBNZDOZEDOUELPJUFUHUJQRABCDLEFGHSTUGUIEDUF + UIEQUEABCEFGUCUAUBUD $. $} From 115f8be92f3a0a65ff79e94df8efa2b2e861d392 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 22:51:21 -0700 Subject: [PATCH 26/49] copy mulgcld from set.mm to iset.mm --- iset.mm | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/iset.mm b/iset.mm index a3dee3d3d..28274aac5 100644 --- a/iset.mm +++ b/iset.mm @@ -146780,6 +146780,18 @@ since the target of the homomorphism (operator ` O ` in our model) need UIEQUEABCEFGUCUAUBUD $. $} + ${ + mulgcld.1 $e |- B = ( Base ` G ) $. + mulgcld.2 $e |- .x. = ( .g ` G ) $. + mulgcld.3 $e |- ( ph -> G e. Grp ) $. + mulgcld.4 $e |- ( ph -> N e. ZZ ) $. + mulgcld.5 $e |- ( ph -> X e. B ) $. + $( Deduction associated with ~ mulgcl . (Contributed by Rohan Ridenour, + 3-Aug-2023.) $) + mulgcld $p |- ( ph -> ( N .x. X ) e. B ) $= + ( cgrp wcel cz co mulgcl syl3anc ) ADLMENMFBMEFCOBMIJKBCDEFGHPQ $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# From d4bd807c7701721f73871e0c2925bb442fe8cd1d Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 22:52:48 -0700 Subject: [PATCH 27/49] copy mulgaddcomlem from set.mm to iset.mm --- iset.mm | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/iset.mm b/iset.mm index 28274aac5..518227da6 100644 --- a/iset.mm +++ b/iset.mm @@ -146792,6 +146792,28 @@ since the target of the homomorphism (operator ` O ` in our model) need ( cgrp wcel cz co mulgcl syl3anc ) ADLMENMFBMEFCOBMIJKBCDEFGHPQ $. $} + ${ + mulgaddcom.b $e |- B = ( Base ` G ) $. + mulgaddcom.t $e |- .x. = ( .g ` G ) $. + mulgaddcom.p $e |- .+ = ( +g ` G ) $. + $( Lemma for ~ mulgaddcom . (Contributed by Paul Chapman, 17-Apr-2009.) + (Revised by AV, 31-Aug-2021.) $) + mulgaddcomlem $p |- ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) + /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) + -> ( ( -u y .x. X ) .+ X ) = ( X .+ ( -u y .x. X ) ) ) $= + ( wcel cz co wceq cfv adantr mulgcl oveq1d grpinvadd syl3anc oveq2d cv wa + cgrp cneg cminusg simp1 simp3 znegcl syl3an2 eqid grpinvcl 3adant2 grpass + w3a syl13anc mulgneg adantl 3eqtr2rd 3eqtr2d grpasscan1 3eqtrd grpasscan2 + fveq2 grpcl eqtr3d ) EUCJZAUAZKJZFBJZUNZVGFDLZFCLZFVKCLZMZUBZFVGUDZFDLZCL + ZFEUENZNZCLZFCLZVQFCLVRVOWAVQFCVOWAFVQVTCLZCLZFVTVQCLZCLZVQVOVFVIVQBJZVTB + JZWAWDMVJVFVNVFVHVIUFZOZVJVIVNVFVHVIUGZOZVJWGVNVHVFVPKJVIWGVGUHBDEVPFGHPU + IZOZVJWHVNVFVIWHVHBEVSFGVSUJZUKULOBCEFVQVTGIUMUOVOWCWEFCVOWCVKVSNZVTCLZVM + VSNZWEVOVQWPVTCVJVQWPMVNBDEVSVGFGHWOUPOZQVOVFVIVKBJZWRWQMWJWLVJWTVNBDEVGF + GHPOZBCEVSFVKGIWORSVOWEVTWPCLZVLVSNZWRVOVQWPVTCWSTVOVFWTVIXCXBMWJXAWLBCEV + SVKFGIWORSVNXCWRMVJVLVMVSVCUQURUSTVOVFVIWGWFVQMWJWLWNBCEVSFVQGIWOUTSVAQVO + VFVRBJZVIWBVRMWJVJXDVNVJVFVIWGXDWIWKWMBCEFVQGIVDSOWLBCEVSVRFGIWOVBSVE $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# From 3459d6ec86b7232136cd09563ce03e8df432e715 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 22:53:20 -0700 Subject: [PATCH 28/49] copy mulgaddcom from set.mm to iset.mm --- iset.mm | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/iset.mm b/iset.mm index 518227da6..a16ce1b68 100644 --- a/iset.mm +++ b/iset.mm @@ -146812,6 +146812,30 @@ since the target of the homomorphism (operator ` O ` in our model) need GHPOZBCEVSFVKGIWORSVOWEVTWPCLZVLVSNZWRVOVQWPVTCWSTVOVFWTVIXCXBMWJXAWLBCEV SVKFGIWORSVNXCWRMVJVLVMVSVCUQURUSTVOVFVIWGWFVQMWJWLWNBCEVSFVQGIWOUTSVAQVO VFVRBJZVIWBVRMWJVJXDVNVJVFVIWGXDWIWKWMBCEFVQGIVDSOWLBCEVSVRFGIWOVBSVE $. + + $d B x y $. $d G x y $. $d N x $. $d X x y $. $d .x. x y $. + $d .+ x y $. + $( The group multiple operator commutes with the group operation. + (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, + 31-Aug-2021.) $) + mulgaddcom $p |- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) + -> ( ( N .x. X ) .+ X ) = ( X .+ ( N .x. X ) ) ) $= + ( vx vy wcel co wceq wi cc0 oveq1 oveq1d oveq2d eqeq12d cz cv c1 caddc wa + cgrp cneg weq c0g cfv eqid grplid mulg0 adantl eqtrd 3eqtr4d cn0 w3a nn0z + grprid simp1 mulgcl 3com23 grpass syl13anc syl3an3 adantr grpmnd 3ad2ant1 + simp2 cmnd simp3 mulgnn0p1 syl3anc eqeq1d biimpar ex 3expia mulgaddcomlem + cn nnz 3exp1 com23 imp syl5 zindd 3imp ) DUFLZEUALZFALZEFCMZFBMZFWKBMZNZW + HWJWIWNWHWJWIWNOJUBZFCMZFBMZFWPBMZNPFCMZFBMZFWSBMZNKUBZFCMZFBMZFXCBMZNZXB + UGZFCMZFBMZFXHBMZNZXBUCUDMZFCMZFBMZFXMBMZNZWNWHWJUEZJKEWOPNZWQWTWRXAXRWPW + SFBWOPFCQZRXRWPWSFBXSSTJKUHZWQXDWRXEXTWPXCFBWOXBFCQZRXTWPXCFBYASTWOXLNZWQ + XNWRXOYBWPXMFBWOXLFCQZRYBWPXMFBYCSTWOXGNZWQXIWRXJYDWPXHFBWOXGFCQZRYDWPXHF + BYESTWOENZWQWLWRWMYFWPWKFBWOEFCQZRYFWPWKFBYGSTXQDUIUJZFBMFWTXAABDFYHGIYHU + KZULXQWSYHFBWJWSYHNWHACDFYHGYIHUMUNZRXQXAFYHBMFXQWSYHFBYJSABDFYHGIYIUTUOU + PWHWJXBUQLZXFXPOWHWJYKURZXFXPYLXFUEZXEFBMZFXDBMZXNXOYLYNYONZXFYKWHWJXBUAL + ZYPXBUSWHWJYQURWHWJXCALZWJYPWHWJYQVAWHWJYQVJZWHYQWJYRACDXBFGHVBVCYSABDFXC + FGIVDVEVFVGYMXMXEFBYLXMXENXFYLXMXDXEYLDVKLZYKWJXMXDNWHWJYTYKDVHVIWHWJYKVL + WHWJYKVJABCDXBFGHIVMVNZVOVPRYLXOYONXFYLXMXDFBUUASVGUPVQVRXBVTLYQXQXFXKOZX + BWAWHWJYQUUBOWHYQWJUUBWHYQWJXFXKKABCDFGHIVSWBWCWDWEWFVQWCWG $. $} From c01f432fc459be0a2644f6d7717cc4c018f45c65 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 22:54:50 -0700 Subject: [PATCH 29/49] copy mulginvcom from set.mm to iset.mm --- iset.mm | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/iset.mm b/iset.mm index a16ce1b68..b576799cb 100644 --- a/iset.mm +++ b/iset.mm @@ -146838,6 +146838,38 @@ since the target of the homomorphism (operator ` O ` in our model) need BWAWHWJYQUUBOWHYQWJUUBWHYQWJXFXKKABCDFGHIVSWBWCWDWEWFVQWCWG $. $} + ${ + $d B x y $. $d G x y $. $d I x y $. $d N x $. $d X x y $. + $d .x. x y $. + mulginvcom.b $e |- B = ( Base ` G ) $. + mulginvcom.t $e |- .x. = ( .g ` G ) $. + mulginvcom.i $e |- I = ( invg ` G ) $. + $( The group multiple operator commutes with the group inverse function. + (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, + 31-Aug-2021.) $) + mulginvcom $p |- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) + -> ( N .x. ( I ` X ) ) = ( I ` ( N .x. X ) ) ) $= + ( vx wcel cfv co wceq wi cc0 oveq1 fvoveq1 eqeq12d adantr vy cgrp cz cneg + cv c1 caddc weq c0g eqid grpinvid eqcomd grpinvcl mulg0 syl adantl fveq2d + 3eqtr4d cn0 w3a cplusg oveq2 cmnd grpmnd 3ad2ant1 simp2 3adant2 mulgnn0p1 + wa syl3anc simp1 nn0z 3ad2ant2 mulgaddcom eqtrd syl3an1 syl3an2 grpinvadd + mulgcl syld3an2 3exp1 com23 imp cn nnz mulgneg syld3an3 simpr eqtr4d syl5 + zindd ex 3imp ) CUBKZEUCKZFAKZEFDLZBMZEFBMDLZNZWNWPWOWTWNWPWOWTOJUEZWQBMZ + XAFBMDLZNPWQBMZPFBMZDLZNUAUEZWQBMZXGFBMZDLZNZXGUDZWQBMZXLFBMZDLZNZXGUFUGM + ZWQBMZXQFBMZDLZNZWTWNWPVIZJUAEXAPNXBXDXCXFXAPWQBQXAPFDBRSJUAUHXBXHXCXJXAX + GWQBQXAXGFDBRSXAXQNXBXRXCXTXAXQWQBQXAXQFDBRSXAXLNXBXMXCXOXAXLWQBQXAXLFDBR + SXAENXBWRXCWSXAEWQBQXAEFDBRSYBCUILZYCDLZXDXFWNYCYDNWPWNYDYCCDYCYCUJZIUKUL + TYBWQAKZXDYCNACDFGIUMZABCWQYCGYEHUNUOYBXEYCDWPXEYCNWNABCFYCGYEHUNUPUQURWN + WPXGUSKZXKYAOZOWNYHWPYIWNYHWPXKYAWNYHWPUTZXKVIWQXHCVALZMZWQXJYKMZXRXTXKYL + YMNYJXHXJWQYKVBUPYJXRYLNXKYJXRXHWQYKMZYLYJCVCKZYHYFXRYNNWNYHYOWPCVDZVEWNY + HWPVFWNWPYFYHYGVGZAYKBCXGWQGHYKUJZVHVJYJWNXGUCKZYFYNYLNWNYHWPVKYHWNYSWPXG + VLZVMYQAYKBCXGWQGHYRVNVJVOTYJXTYMNXKYJXTXIFYKMZDLZYMYJXSUUADWNYOYHWPXSUUA + NYPAYKBCXGFGHYRVHVPUQWNXIAKZYHWPUUBYMNYHWNYSWPUUCYTABCXGFGHVSVQAYKCDXIFGY + RIVRVTVOTURWAWBWCXGWDKYSYBXKXPOZXGWEWNWPYSUUDOWNYSWPUUDWNYSWPXKXPWNYSWPUT + ZXKVIZXMXHDLZXOUUEXMUUGNZXKWNYSWPYFUUHWNWPYFYSYGVGABCDXGWQGHIWFWGTUUFXNXH + DUUFXNXJXHUUEXNXJNXKABCDXGFGHIWFTUUEXKWHWIUQWIWAWBWCWJWKWLWBWM $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# From 31b2a19e55dfa87ae74c1f08e593995732c8dfe2 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 22:55:36 -0700 Subject: [PATCH 30/49] copy mulginvinv from set.mm to iset.mm --- iset.mm | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/iset.mm b/iset.mm index b576799cb..bc34aa89d 100644 --- a/iset.mm +++ b/iset.mm @@ -146868,6 +146868,15 @@ since the target of the homomorphism (operator ` O ` in our model) need RIVRVTVOTURWAWBWCXGWDKYSYBXKXPOZXGWEWNWPYSUUDOWNYSWPUUDWNYSWPXKXPWNYSWPUT ZXKVIZXMXHDLZXOUUEXMUUGNZXKWNYSWPYFUUHWNWPYFYSYGVGABCDXGWQGHIWFWGTUUFXNXH DUUFXNXJXHUUEXNXJNXKABCDXGFGHIWFTUUEXKWHWIUQWIWAWBWCWJWKWLWBWM $. + + $( The group multiple operator commutes with the group inverse function. + (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, + 31-Aug-2021.) $) + mulginvinv $p |- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) + -> ( I ` ( N .x. ( I ` X ) ) ) = ( N .x. X ) ) $= + ( cgrp wcel cz w3a cfv co wceq grpinvcl 3adant2 mulginvcom syld3an3 + grpinvinv oveq2d eqtr3d ) CJKZELKZFAKZMZEFDNZDNZBOZEUHBODNZEFBOUDUEUFUHAK + ZUJUKPUDUFULUEACDFGIQRABCDEUHGHISTUGUIFEBUDUFUIFPUEACDFGIUARUBUC $. $} From 793c604705f07feb35cde610d37beb3cdb970795 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 23:12:39 -0700 Subject: [PATCH 31/49] Add mulgnn0z to iset.mm Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof. --- iset.mm | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/iset.mm b/iset.mm index bc34aa89d..d8a5e89a2 100644 --- a/iset.mm +++ b/iset.mm @@ -146879,6 +146879,25 @@ since the target of the homomorphism (operator ` O ` in our model) need ZUJUKPUDUFULUEACDFGIQRABCDEUHGHISTUGUIFEBUDUFUIFPUEACDFGIUARUBUC $. $} + ${ + $d .0. x y $. $d B x y $. $d G x y $. $d N x y $. + mulgnn0z.b $e |- B = ( Base ` G ) $. + mulgnn0z.t $e |- .x. = ( .g ` G ) $. + mulgnn0z.o $e |- .0. = ( 0g ` G ) $. + $( A group multiple of the identity, for nonnegative multiple. + (Contributed by Mario Carneiro, 13-Dec-2014.) $) + mulgnn0z $p |- ( ( G e. Mnd /\ N e. NN0 ) -> ( N .x. .0. ) = .0. ) $= + ( vx vy wcel cn cc0 wceq co wa cfv c1 eqid adantr cn0 wo elnn0 cplusg csn + cmnd cxp cseq mndidcl mulgnn syl2anr mndlid mpdan cuz simpr nnuz eleqtrdi + id cv cfz elfznn fvconst2g syl2an ialgrlemconst mndcl 3expb adantlr eqtrd + seq3id3 oveq1 mulg0 syl sylan9eqr jaodan sylan2b ) DUAKCUFKZDLKZDMNZUBDEB + OZENZDUCVPVQVTVRVPVQPZVSDCUDQZLEUEUGZRUHZQZEVQVQEAKZVSWENVPVQURACEFHUIZAW + BWDBCDEFWBSZGWDSUJUKWAIJWBAWCRDEVPEEWBOENZVQVPWFWIWGAWBCEEFWHHULUMTWADLRU + NQVPVQUOUPUQWAWFIUSZLKWJWCQENWJRDUTOKVPWFVQWGTZWJDVALEWJAVBVCWKWAIEARLUPW + KVDVPWJAKZJUSZAKZPWJWMWBOAKZVQVPWLWNWOAWBCWJWMFWHVEVFVGVIVHVRVPVSMEBOZEDM + EBVJVPWFWPENWGABCEEFHGVKVLVMVNVO $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# From c847ab3670454b493c506a085af6a18dabad6e69 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 22 Dec 2024 23:13:43 -0700 Subject: [PATCH 32/49] copy mulgz from set.mm to iset.mm --- iset.mm | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/iset.mm b/iset.mm index d8a5e89a2..1d64d6b45 100644 --- a/iset.mm +++ b/iset.mm @@ -146896,6 +146896,18 @@ since the target of the homomorphism (operator ` O ` in our model) need NQVPVQUOUPUQWAWFIUSZLKWJWCQENWJRDUTOKVPWFVQWGTZWJDVALEWJAVBVCWKWAIEARLUPW KVDVPWJAKZJUSZAKZPWJWMWBOAKZVQVPWLWNWOAWBCWJWMFWHVEVFVGVIVHVRVPVSMEBOZEDM EBVJVPWFWPENWGABCEEFHGVKVLVMVNVO $. + + $( A group multiple of the identity, for integer multiple. (Contributed by + Mario Carneiro, 13-Dec-2014.) $) + mulgz $p |- ( ( G e. Grp /\ N e. ZZ ) -> ( N .x. .0. ) = .0. ) $= + ( wcel cz wa cn0 co wceq cneg mulgnn0z sylan cfv adantl ad2antrr cgrp zcn + cmnd grpmnd adantr cminusg simpll nn0z grpidcl mulgneg syl3anc cc negnegd + eqid ad2antlr oveq1d fveq2d grpinvid eqtrd 3eqtr3d wo cr simprbi mpjaodan + elznn0 ) CUAIZDJIZKZDLIZDEBMZENZDOZLIZVHCUCIZVIVKVFVNVGCUDUEZABCDEFGHPQVH + VMKZVLOZEBMZVLEBMZCUFRZRZVJEVPVFVLJIZEAIZVRWANVFVGVMUGVMWBVHVLUHSVFWCVGVM + ACEFHUITABCVTVLEFGVTUNZUJUKVPVQDEBVPDVGDULIVFVMDUBUOUMUPVPWAEVTRZEVPVSEVT + VHVNVMVSENVOABCVLEFGHPQUQVFWEENVGVMCVTEHWDURTUSUTVGVIVMVAZVFVGDVBIWFDVEVC + SVD $. $} From c1e92c6839a1ac2011b9d621095b39ebaeaf2b38 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 23 Dec 2024 20:46:04 -0700 Subject: [PATCH 33/49] Add mulgnndir to iset.mm Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof. --- iset.mm | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/iset.mm b/iset.mm index 1d64d6b45..c3f700afd 100644 --- a/iset.mm +++ b/iset.mm @@ -146910,6 +146910,39 @@ since the target of the homomorphism (operator ` O ` in our model) need SVD $. $} + ${ + $d x y z u v B $. $d x y z u v G $. $d x y z u v M $. $d x y z u v N $. + $d x y z u v .+ $. $d x y z u v X $. + mulgnndir.b $e |- B = ( Base ` G ) $. + mulgnndir.t $e |- .x. = ( .g ` G ) $. + mulgnndir.p $e |- .+ = ( +g ` G ) $. + $( Sum of group multiples, for positive multiples. (Contributed by Mario + Carneiro, 11-Dec-2014.) (Revised by AV, 29-Aug-2021.) $) + mulgnndir $p |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> + ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) ) $= + ( wcel cn wa caddc co c1 cfv cv wceq cvv vx vy vz vu vv csgrp w3a csn cxp + cseq cmgm sgrpmgm mgmcl syl3an1 3expb adantlr sgrpass cuz simpr2 eleqtrdi + cz nnuz simpr1 nnzd eluzadd syl2anc nncnd addcomd cc ax-1cn addcom fveq2d + sylancl 3eltr4d simpr3 ialgrlemconst seq3split nnaddcld mulgnn cfz elfznn + eqid fvconst2g syl2an nnaddcl syl2anr eqtr4d elnnuz biimpri simpl eqeltrd + syl2an2r elexd 1nn adantr eluznn sylancom simprl cplusg eqeltrid ad2antrr + a1i plusgslid slotex simprr ovexg syl3anc seqeq1d fveq12d 3eqtr4d oveq12d + seq3shft2 ) DUFKZELKZFLKZGAKZUGZMZEFNOZBLGUHUIZPUJZQZEYAQZXSBXTEPNOZUJZQZ + BOXSGCOZEGCOZFGCOZBOXRUAUBUCBAXTPEXSXMUARZAKZUBRZAKZMYJYLBOZAKZXQXMYKYMYO + XMDUKKYKYMYODULADYJYLBHJUMUNUOUPXMYKYMUCRZAKUGYNYPBOYJYLYPBOBOSXQADYJYLBY + PHJUQUPXRFENOZPENOZURQZXSYDURQXRFPURQZKEVAKYQYSKXRFLYTXMXNXOXPUSZVBUTZXRE + XMXNXOXPVCZVDZEPFVEVFXREFXREUUCVGZXRFUUAVGVHZXRYDYRURXREVIKPVIKYDYRSUUEVJ + EPVKVMZVLVNXRELYTUUCVBUTXRUAGAPLVBXMXNXOXPVOZVPVQXRXSLKXPYGYBSXREFUUCUUAV + RUUHABYACDXSGHJIYAWBZVSVFXRYHYCYIYFBXRXNXPYHYCSUUCUUHABYACDEGHJIUUIVSVFXR + FYAQZYQBXTYRUJZQYIYFXRUDUEBTUAXTXTEPFUUBUUDXRYJPFVTOKZMYJXTQZGYJENOZXTQZX + RXPYJLKZUUMGSUULUUHYJFWAZLGYJAWCWDXRXPUULUUNLKZUUOGSUUHUULUUPXNUURXRUUQUU + CYJEWEWFLGUUNAWCWLWGXRXPUDRZLKZUUSXTQZTKZUUSYTKZUUHUUTUVCUUSWHWIXPUUTMZUV + AAUVDUVAGALGUUSAWCXPUUTWJWKWMZWDXRXPUUSYSKZUUTUVBUUHXRUVFYRLKUUTXRUVFMZPE + PLKUVGWNXBXRXNUVFUUCWOVRUUSYRWPWQUVEWLXRUUSTKZUERZTKZMZMUVHBTKZUVJUUSUVIB + OTKXRUVHUVJWRXMUVLXQUVKXMBDWSQTJDWSUFXCXDWTXAXRUVHUVJXEUUSUVIBTTTXFXGXLXR + XOXPYIUUJSUUAUUHABYACDFGHJIUUIVSVFXRXSYQYEUUKXRYDYRBXTUUGXHUUFXIXJXKXJ $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# From 1a71ff66d82a45e4bb7fba03ce53a06d5f4f855a Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 23 Dec 2024 21:18:51 -0700 Subject: [PATCH 34/49] copy mulgnn0dir from set.mm to iset.mm --- iset.mm | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/iset.mm b/iset.mm index c3f700afd..c2b09fc38 100644 --- a/iset.mm +++ b/iset.mm @@ -146941,6 +146941,24 @@ since the target of the homomorphism (operator ` O ` in our model) need PLKUVGWNXBXRXNUVFUUCWOVRUUSYRWPWQUVEWLXRUUSTKZUERZTKZMZMUVHBTKZUVJUUSUVIB OTKXRUVHUVJWRXMUVLXQUVKXMBDWSQTJDWSUFXCXDWTXAXRUVHUVJXEUUSUVIBTTTXFXGXLXR XOXPYIUUJSUUAUUHABYACDFGHJIUUIVSVFXRXSYQYEUUKXRYDYRBXTUUGXHUUFXIXJXKXJ $. + + $( Sum of group multiples, generalized to ` NN0 ` . (Contributed by Mario + Carneiro, 11-Dec-2014.) $) + mulgnn0dir $p |- ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> + ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) ) $= + ( wcel wa caddc co wceq cc0 adantr simpr oveq1d eqtrd cmnd cn0 cn mndsgrp + w3a csgrp ad2antrr simplr simpr3 mulgnndir syl13anc c0g cfv simpll simpr1 + simplr3 mulgnn0cl syl3anc eqid mndrid syl2anc mulg0 oveq2d nn0cnd addid1d + syl 3eqtr4rd adantlr simpr2 elnn0 sylib mpjaodan simplr2 mndlid addid2d + wo ) DUAKZEUBKZFUBKZGAKZUEZLZEUCKZEFMNZGCNZEGCNZFGCNZBNZOZEPOZWBWCLZFUCKZ + WIFPOZWKWLLDUFKZWCWLVTWIWBWNWCWLVQWNWADUDQUGWBWCWLUHWKWLRWBVTWCWLVQVRVSVT + UIUGABCDEFGHIJUJUKWBWMWIWCWBWMLZWFDULUMZBNZWFWHWEWOVQWFAKZWQWFOVQWAWMUNZW + OVQVRVTWRWSWBVRWMVQVRVSVTUOZQZVRVSVTVQWMUPZACDEGHIUQURABDWFWPHJWPUSZUTVAW + OWGWPWFBWOWGPGCNZWPWOFPGCWBWMRZSWOVTXDWPOZXBACDGWPHXCIVBZVFTVCWOWDEGCWOWD + EPMNEWOFPEMXEVCWOEWOEXAVDVETSVGVHWBWLWMVPZWCWBVSXHVQVRVSVTVIFVJVKQVLWBWJL + ZWPWGBNZWGWHWEXIVQWGAKZXJWGOVQWAWJUNZXIVQVSVTXKXLVRVSVTVQWJVMZVRVSVTVQWJU + PZACDFGHIUQURABDWGWPHJXCVNVAXIWFWPWGBXIWFXDWPXIEPGCWBWJRZSXIVTXFXNXGVFTSX + IWDFGCXIWDPFMNFXIEPFMXOSXIFXIFXMVDVOTSVGWBVRWCWJVPWTEVJVKVL $. $} From 7927f04566aa403144c77c4121a63143007a8d32 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 23 Dec 2024 21:19:26 -0700 Subject: [PATCH 35/49] copy mulgdir from set.mm to iset.mm Includes lemma mulgdirlem --- iset.mm | 51 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) diff --git a/iset.mm b/iset.mm index c2b09fc38..21960625f 100644 --- a/iset.mm +++ b/iset.mm @@ -146959,6 +146959,57 @@ since the target of the homomorphism (operator ` O ` in our model) need ZWPWGBNZWGWHWEXIVQWGAKZXJWGOVQWAWJUNZXIVQVSVTXKXLVRVSVTVQWJVMZVRVSVTVQWJU PZACDFGHIUQURABDWGWPHJXCVNVAXIWFWPWGBXIWFXDWPXIEPGCWBWJRZSXIVTXFXNXGVFTSX IWDFGCXIWDPFMNFXIEPFMXOSXIFXIFXMVDVOTSVGWBVRWCWJVPWTEVJVKVL $. + + $( Lemma for ~ mulgdir . (Contributed by Mario Carneiro, 13-Dec-2014.) $) + mulgdirlem $p |- ( ( G e. Grp /\ + ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) -> + ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) ) $= + ( wcel cz co cn0 wceq wa syl13anc adantr syl3anc oveq1d cgrp caddc simpl1 + w3a cneg grpmndd simprl simprr simpl23 mulgnn0dir anassrs c0g cfv cminusg + cmnd simp22 eqid mulgneg mulgcl grplinv syl2anc oveq2d simpl3 nn0z grprid + eqtrd ad2antll grpass cmin cc simp21 zcnd addcld negsubd pncand eqtr3d wo + syl elznn0 simprbi mpjaodan znegcld 3ad2ant3 grprinv grplid simpr addcomd + cr negcld pncan2d 3eqtrd 3eqtr3d ) DUAKZELKZFLKZGAKZUDZEFUBMZNKZUDZENKZWR + GCMZEGCMZFGCMZBMZOZEUEZNKZWTXAPFNKZXFFUEZNKZWTXAXIXFWTXAXIPZPZDUOKZXAXIWP + XFXMDWMWQWSXLUCUFWTXAXIUGWTXAXIUHWNWOWPWMWSXLUIABCDEFGHIJUJQUKWTXAXKXFWTX + AXKPZPZXBXJGCMZXDBMZBMZXBXEXPXSXBDULUMZBMZXBXPXRXTXBBXPXRXDDUNUMZUMZXDBMZ + XTXPXQYCXDBXPWMWOWPXQYCOWMWQWSXOUCZWTWOXOWMWNWOWPWSUPZRZWNWOWPWMWSXOUIZAC + DYBFGHIYBUQZURSTXPWMXDAKZYDXTOYEXPWMWOWPYJYEYGYHACDFGHIUSSZABDYBXDXTHJXTU + QZYIUTVAVFVBXPWMXBAKZYAXBOYEXPWMWRLKZWPYMYEXPWSYNWMWQWSXOVCZWRVDZVRYHACDW + RGHIUSZSZABDXBXTHJYLVEVAVFXPXBXQBMZXDBMZXSXEXPWMYMXQAKZYJYTXSOYEYRXPWMXJL + KZWPUUAYEXKUUBWTXAXJVDVGYHACDXJGHIUSSYKABDXBXQXDHJVHQXPYSXCXDBXPWRXJUBMZG + CMZYSXCXPXNWSXKWPUUDYSOXPDYEUFYOWTXAXKUHYHABCDWRXJGHIJUJQXPUUCEGCXPUUCWRF + VIMEXPWRFWTWRVJKZXOWTEFWTEWMWNWOWPWSVKZVLZWTFYFVLZVMZRWTFVJKZXOUUHRZVNXPE + FWTEVJKZXOUUGRUUKVOVFTVPTVPVPUKWTXIXKVQZXAWTWOUUMYFWOFWHKUUMFVSVTVRRWAWTX + HPZXCXGGCMZBMZXBBMZXCUUOXBBMZBMZXBXEUUNWMXCAKZUUOAKZYMUUQUUSOWMWQWSXHUCZU + UNWMWNWPUUTUVBWTWNXHUUFRZWNWOWPWMWSXHUIZACDEGHIUSSZUUNWMXGLKWPUVAUVBUUNEU + VCWBUVDACDXGGHIUSSUUNWMYNWPYMUVBWTYNXHWSWMYNWQYPWCRUVDYQSZABDXCUUOXBHJVHQ + UUNUUQXTXBBMZXBUUNUUPXTXBBUUNUUPXCXCYBUMZBMZXTUUNUUOUVHXCBUUNWMWNWPUUOUVH + OUVBUVCUVDACDYBEGHIYIURSVBUUNWMUUTUVIXTOUVBUVEABDYBXCXTHJYLYIWDVAVFTUUNWM + YMUVGXBOUVBUVFABDXBXTHJYLWEVAVFUUNUURXDXCBUUNXGWRUBMZGCMZUURXDUUNXNXHWSWP + UVKUUROUUNDUVBUFWTXHWFWMWQWSXHVCUVDABCDXGWRGHIJUJQUUNUVJFGCUUNUVJWRXGUBMW + REVIMFUUNXGWRUUNEWTUULXHUUGRZWIWTUUEXHUUIRZWGUUNWREUVMUVLVNUUNEFUVLWTUUJX + HUUHRWJWKTVPVBWLWTWNXAXHVQZUUFWNEWHKUVNEVSVTVRWA $. + + $( Sum of group multiples, generalized to ` ZZ ` . (Contributed by Mario + Carneiro, 13-Dec-2014.) $) + mulgdir $p |- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> + ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) ) $= + ( wcel cz co cn0 wceq cneg cfv adantr mulgneg syl3anc cgrp w3a mulgdirlem + wa caddc 3expa cminusg simpll simpr2 znegcld simpr1 simplr3 negcld negdid + zcnd comraddd simpr eqeltrrd syl131anc oveq1d zaddcld eqid eqtr3d oveq12d + mulgcl grpinvadd eqtr4d 3eqtr3d fveq2d grpinvinv syl2anc grpcl wo simprbi + cr elznn0 syl mpjaodan ) DUAKZELKZFLKZGAKZUBZUDZEFUEMZNKZWEGCMZEGCMZFGCMZ + BMZOZWEPZNKZVSWCWFWKABCDEFGHIJUCUFWDWMUDZWGDUGQZQZWOQZWJWOQZWOQZWGWJWNWPW + RWOWNFPZEPZUEMZGCMZWTGCMZXAGCMZBMZWPWRWNVSWTLKXALKWBXBNKXCXFOVSWCWMUHZWNF + WDWAWMVSVTWAWBUIZRZUJWNEWDVTWMVSVTWAWBUKZRZUJVTWAWBVSWMULZWNWLXBNWNWLXAWT + WNEWNEXKUOZUMWNFWNFXIUOZUMWNEFXMXNUNUPZWDWMUQURABCDWTXAGHIJUCUSWNWLGCMZXC + WPWNWLXBGCXOUTWNVSWELKZWBXPWPOXGWDXQWMWDEFXJXHVAZRZXLACDWOWEGHIWOVBZSTVCW + NXFWIWOQZWHWOQZBMZWRWNXDYAXEYBBWNVSWAWBXDYAOXGXIXLACDWOFGHIXTSTWNVSVTWBXE + YBOXGXKXLACDWOEGHIXTSTVDWNVSWHAKZWIAKZWRYCOXGWNVSVTWBYDXGXKXLACDEGHIVETZW + NVSWAWBYEXGXIXLACDFGHIVETZABDWOWHWIHJXTVFTVGVHVIWNVSWGAKZWQWGOXGWNVSXQWBY + HXGXSXLACDWEGHIVETADWOWGHXTVJVKWNVSWJAKZWSWJOXGWNVSYDYEYIXGYFYGABDWHWIHJV + LTADWOWJHXTVJVKVHWDXQWFWMVMZXRXQWEVOKYJWEVPVNVQVR $. $} From 06f61fd34f72a7ae3d59c3db1eb01ca3fc0c8d2e Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 23 Dec 2024 21:21:25 -0700 Subject: [PATCH 36/49] copy mulgp1 from set.mm to iset.mm --- iset.mm | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/iset.mm b/iset.mm index 21960625f..45bdcb6ab 100644 --- a/iset.mm +++ b/iset.mm @@ -147010,6 +147010,14 @@ since the target of the homomorphism (operator ` O ` in our model) need NVSWAWBYEXGXIXLACDFGHIVETZABDWOWHWIHJXTVFTVGVHVIWNVSWGAKZWQWGOXGWNVSXQWBY HXGXSXLACDWEGHIVETADWOWGHXTVJVKWNVSWJAKZWSWJOXGWNVSYDYEYIXGYFYGABDWHWIHJV LTADWOWJHXTVJVKVHWDXQWFWMVMZXRXQWEVOKYJWEVPVNVQVR $. + + $( Group multiple (exponentiation) operation at a successor, extended to + ` ZZ ` . (Contributed by Mario Carneiro, 11-Dec-2014.) $) + mulgp1 $p |- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> + ( ( N + 1 ) .x. X ) = ( ( N .x. X ) .+ X ) ) $= + ( cgrp wcel cz w3a c1 caddc co wceq 1z mulgdir mp3anr2 3impb mulg1 oveq2d + 3ad2ant3 eqtrd ) DJKZELKZFAKZMZENOPFCPZEFCPZNFCPZBPZUKFBPUFUGUHUJUMQZUFUG + NLKUHUNRABCDENFGHISTUAUIULFUKBUHUFULFQUGACDFGHUBUDUCUE $. $} From 91198cc93d12cd18d0fdcddb9bb491d544554f0c Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 23 Dec 2024 21:22:42 -0700 Subject: [PATCH 37/49] copy mulgneg2 from set.mm to iset.mm --- iset.mm | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/iset.mm b/iset.mm index 45bdcb6ab..116b73eb9 100644 --- a/iset.mm +++ b/iset.mm @@ -147020,6 +147020,36 @@ since the target of the homomorphism (operator ` O ` in our model) need NLKUHUNRABCDENFGHISTUAUIULFUKBUHUFULFQUGACDFGHUBUDUCUE $. $} + ${ + $d n x B $. $d n x G $. $d n x I $. $d n x .x. $. $d n x X $. + $d x N $. + mulgneg2.b $e |- B = ( Base ` G ) $. + mulgneg2.m $e |- .x. = ( .g ` G ) $. + mulgneg2.i $e |- I = ( invg ` G ) $. + $( Group multiple (exponentiation) operation at a negative integer. + (Contributed by Mario Carneiro, 13-Dec-2014.) $) + mulgneg2 $p |- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> + ( -u N .x. X ) = ( N .x. ( I ` X ) ) ) $= + ( wcel cneg co cfv wceq cc0 c1 negeq oveq1d oveq1 eqeq12d vx vn cgrp neg0 + cz cv caddc wa eqtrdi c0g eqid mulg0 adantl grpinvcl syl eqtr4d wi cplusg + cn0 cc nn0cn ax-1cn negdi sylancl simpll nn0negz 1z znegcl simplr mulgdir + mp1i syl13anc mulgm1 adantr oveq2d 3eqtrd grpmnd ad2antrr simpr mulgnn0p1 + cmnd syl3anc syl5ibr ex cn fveq2 nnnegz mulgneg id mulgnegnn zindd 3impia + syl2anr 3com23 ) CUCJZFAJZEUEJZEKZFBLZEFDMZBLZNZWOWPWQXBUAUFZKZFBLZXCWTBL + ZNOFBLZOWTBLZNUBUFZKZFBLZXIWTBLZNZXJKZFBLZXJWTBLZNZXIPUGLZKZFBLZXRWTBLZNZ + XBWOWPUHZUAUBEXCONZXEXGXFXHYDXDOFBYDXDOKOXCOQUDUIRXCOWTBSTXCXINZXEXKXFXLY + EXDXJFBXCXIQRXCXIWTBSTXCXRNZXEXTXFYAYFXDXSFBXCXRQRXCXRWTBSTXCXJNZXEXOXFXP + YGXDXNFBXCXJQRXCXJWTBSTXCENZXEWSXFXAYHXDWRFBXCEQRXCEWTBSTYCXGCUJMZXHWPXGY + INWOABCFYIGYIUKZHULUMYCWTAJZXHYINACDFGIUNZABCWTYIGYJHULUOUPYCXIUSJZXMYBUQ + XMYBYCYMUHZXKWTCURMZLZXLWTYOLZNXKXLWTYOSYNXTYPYAYQYNXTXJPKZUGLZFBLZXKYRFB + LZYOLZYPYNXSYSFBYNXIUTJZPUTJXSYSNYMUUCYCXIVAUMVBXIPVCVDRYNWOXJUEJZYRUEJZW + PYTUUBNWOWPYMVEYMUUDYCXIVFUMPUEJUUEYNVGPVHVKWOWPYMVIAYOBCXJYRFGHYOUKZVJVL + YNUUAWTXKYOYCUUAWTNYMABCDFGHIVMVNVOVPYNCWAJZYMYKYAYQNWOUUGWPYMCVQVRYCYMVS + YCYKYMYLVNAYOBCXIWTGHUUFVTWBTWCWDYCXIWEJZXMXQUQXMXQYCUUHUHZXKDMZXLDMZNXKX + LDWFUUIXOUUJXPUUKUUIWOUUDWPXOUUJNWOWPUUHVEUUHUUDYCXIWGUMWOWPUUHVIABCDXJFG + HIWHWBUUHUUHYKXPUUKNYCUUHWIYLABCDXIWTGHIWJWMTWCWDWKWLWN $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# From 246ed89bfd8097a4dd0c88ff088ddc66098d7eb4 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 23 Dec 2024 21:23:59 -0700 Subject: [PATCH 38/49] copy mulgnnass from set.mm to iset.mm --- iset.mm | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/iset.mm b/iset.mm index 116b73eb9..360f3a2a6 100644 --- a/iset.mm +++ b/iset.mm @@ -147050,6 +147050,33 @@ since the target of the homomorphism (operator ` O ` in our model) need HIWHWBUUHUUHYKXPUUKNYCUUHWIYLABCDXIWTGHIWJWMTWCWDWKWLWN $. $} + ${ + $d m n B $. $d m n G $. $d m n N $. $d m n .x. $. $d m n X $. + $d n M $. + mulgass.b $e |- B = ( Base ` G ) $. + mulgass.t $e |- .x. = ( .g ` G ) $. + $( Product of group multiples, for positive multiples in a semigroup. + (Contributed by Mario Carneiro, 13-Dec-2014.) (Revised by AV, + 29-Aug-2021.) $) + mulgnnass $p |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> + ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) $= + ( vn wcel cn cmul co wceq wi c1 oveq1 oveq1d eqeq12d imbi2d vm csgrp nncn + w3a cv caddc mulid2d 3ad2ant1 sgrpmgm mulgnncl syl3an1 3coml mulg1 eqtr4d + cmgm syl wa cplusg cfv cc adantr simpr1 nncnd adddirp1d nnmulcl 3ad2antr1 + simpr3 simpr2 eqid mulgnndir syl13anc eqtrd mulgnnp1 sylan2 syl5ibr nnind + ex a2d 3expd com4r 3imp2 ) CUBJZDKJZEKJZFAJZDELMZFBMZDEFBMZBMZNZWCWDWEWBW + JWCWDWEWBWJWDWEWBUDZIUEZELMZFBMZWLWHBMZNZOWKPELMZFBMZPWHBMZNZOWKUAUEZELMZ + FBMZXAWHBMZNZOWKXAPUFMZELMZFBMZXFWHBMZNZOWKWJOIUADWLPNZWPWTWKXKWNWRWOWSXK + WMWQFBWLPELQRWLPWHBQSTWLXANZWPXEWKXLWNXCWOXDXLWMXBFBWLXAELQRWLXAWHBQSTWLX + FNZWPXJWKXMWNXHWOXIXMWMXGFBWLXFELQRWLXFWHBQSTWLDNZWPWJWKXNWNWGWOWIXNWMWFF + BWLDELQRWLDWHBQSTWKWRWHWSWKWQEFBWDWEWQENWBWDEEUCUGUHRWKWHAJZWSWHNWBWDWEXO + WBCUOJWDWEXOCUIABCEFGHUJUKULZABCWHGHUMUPUNXAKJZWKXEXJXQWKXEXJOXEXJXQWKUQZ + XCWHCURUSZMZXDWHXSMZNXCXDWHXSQXRXHXTXIYAXRXHXBEUFMZFBMZXTXRXGYBFBXRXAEXQX + AUTJWKXAUCVAXREXQWDWEWBVBZVCVDRXRWBXBKJZWDWEYCXTNXQWDWEWBVGXQWEWDYEWBXAEV + EVFYDXQWDWEWBVHAXSBCXBEFGHXSVIZVJVKVLWKXQXOXIYANXPAXSBCXAWHGHYFVMVNSVOVQV + RVPVSVTWA $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# From b4a174343b350856acbfbe6586102a8f030a4b6e Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 23 Dec 2024 21:24:27 -0700 Subject: [PATCH 39/49] copy mulgnn0ass from set.mm to iset.mm --- iset.mm | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/iset.mm b/iset.mm index 360f3a2a6..eeb74f668 100644 --- a/iset.mm +++ b/iset.mm @@ -147075,6 +147075,23 @@ since the target of the homomorphism (operator ` O ` in our model) need AUTJWKXAUCVAXREXQWDWEWBVBZVCVDRXRWBXBKJZWDWEYCXTNXQWDWEWBVGXQWEWDYEWBXAEV EVFYDXQWDWEWBVHAXSBCXBEFGHXSVIZVJVKVLWKXQXOXIYANXPAXSBCXAWHGHYFVMVNSVOVQV RVPVSVTWA $. + + $( Product of group multiples, generalized to ` NN0 ` . (Contributed by + Mario Carneiro, 13-Dec-2014.) $) + mulgnn0ass $p |- ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> + ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) $= + ( wcel cn0 wa cn cmul co wceq cc0 adantr mulg0 oveq1d oveq1 csgrp mndsgrp + cmnd w3a simprl simprr simpr3 mulgnnass syl13anc expr c0g cfv eqid simpr1 + syl nn0cnd mul01d oveq2d 3ad2antr1 eqtrd 3eqtr4d oveq2 eqeq12d syl5ibrcom + mulgnn0z wo simpr2 elnn0 sylib mpjaod ex mul02d mulgnn0cl 3adant3r1 ) CUC + IZDJIZEJIZFAIZUDZKZDLIZDEMNZFBNZDEFBNZBNZOZDPOZVTWAWFVTWAKZELIZWFEPOZVTWA + WIWFVTWAWIKZKCUAIZWAWIVRWFVTWLWKVOWLVSCUBQQVTWAWIUEVTWAWIUFVTVRWKVOVPVQVR + UGZQABCDEFGHUHUIUJWHWFWJDPMNZFBNZDPFBNZBNZOZVTWRWAVTWPCUKULZWOWQVTVRWPWSO + WMABCFWSGWSUMZHRUOZVTWNPFBVTDVTDVOVPVQVRUNZUPUQSVTWQDWSBNZWSVTWPWSDBXAURV + OVQVPXCWSOVRABCDWSGHWTVEUSUTVAQWJWCWOWEWQWJWBWNFBEPDMVBSWJWDWPDBEPFBTURVC + VDVTWIWJVFZWAVTVQXDVOVPVQVRVGZEVHVIQVJVKVTWFWGPEMNZFBNZPWDBNZOVTWPWSXGXHX + AVTXFPFBVTEVTEXEUPVLSVTWDAIZXHWSOVOVQVRXIVPABCEFGHVMVNABCWDWSGWTHRUOVAWGW + CXGWEXHWGWBXFFBDPEMTSDPWDBTVCVDVTVPWAWGVFXBDVHVIVJ $. $} From 7c43ff938b0b0cf28afebfb88706d1f99d020695 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 23 Dec 2024 21:25:02 -0700 Subject: [PATCH 40/49] copy mulgass from set.mm to iset.mm --- iset.mm | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/iset.mm b/iset.mm index eeb74f668..48000da54 100644 --- a/iset.mm +++ b/iset.mm @@ -147092,6 +147092,36 @@ since the target of the homomorphism (operator ` O ` in our model) need VDVTWIWJVFZWAVTVQXDVOVPVQVRVGZEVHVIQVJVKVTWFWGPEMNZFBNZPWDBNZOVTWPWSXGXHX AVTXFPFBVTEVTEXEUPVLSVTWDAIZXHWSOVOVQVRXIVPABCEFGHVMVNABCWDWSGWTHRUOVAWGW CXGWEXHWGWBXFFBDPEMTSDPWDBTVCVDVTVPWAWGVFXBDVHVIVJ $. + + $( Product of group multiples, generalized to ` ZZ ` . (Contributed by + Mario Carneiro, 13-Dec-2014.) $) + mulgass $p |- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> + ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) $= + ( wcel cz wa cn0 cneg cmul co wceq ad2antrr adantr cfv syl3anc w3a simpr1 + cgrp wo cr elznn0 simprbi syl simpr2 cmnd grpmnd simprl simprr mulgnn0ass + simplr3 syl13anc zcnd mulneg1d oveq1d simpr3 eqtr3d cminusg fveq2 zmulcld + ex simpl eqid mulgneg fveq2d mulgcl grpinvinv syldan eqtrd eqeq12d syl5ib + imp mulneg2d oveq2d mulgneg2 eqtr4d 3eqtr3d mul2negd nn0z ad2antll ccased + negnegd mp2and ) CUCIZDJIZEJIZFAIZUAZKZDLIZDMZLIZUDZELIZEMZLIZUDZDENOZFBO + ZDEFBOZBOZPZWMWIWQWHWIWJWKUBZWIDUEIWQDUFUGUHWMWJXAWHWIWJWKUIZWJEUEIXAEUFU + GUHWMWNWRWPWTXFWMWNWRKZXFWMXIKCUJIZWNWRWKXFWHXJWLXICUKZQWMWNWRULWMWNWRUMW + IWJWKWHXIUOABCDEFGHUNUPVEWMWPWRKZXFWMXLXBMZFBOZWOXDBOZPZXFWMXLKZWOENOZFBO + ZXNXOXQXRXMFBWMXRXMPXLWMDEWMDXGUQZWMEXHUQZURRUSXQXJWPWRWKXSXOPWHXJWLXLXKQ + WMWPWRULWMWPWRUMWMWKXLWHWIWJWKUTZRABCWOEFGHUNUPVAWMXPXFXPXNCVBSZSZXOYCSZP + WMXFXNXOYCVCWMYDXCYEXEWMYDXCYCSZYCSZXCWMXNYFYCWMWHXBJIZWKXNYFPWHWLVFZWMDE + XGXHVDZYBABCYCXBFGHYCVGZVHTVIWHWLXCAIZYGXCPWMWHYHWKYLYIYJYBABCXBFGHVJTACY + CXCGYKVKVLVMWMYEXEYCSZYCSZXEWMXOYMYCWMWHWIXDAIZXOYMPYIXGWMWHWJWKYOYIXHYBA + BCEFGHVJTZABCYCDXDGHYKVHTVIWHWLXEAIZYNXEPWMWHWIYOYQYIXGYPABCDXDGHVJTACYCX + EGYKVKVLVMVNVOVPZVLVEWMWNWTKZXFWMYSXPXFWMYSKZDWSNOZFBOZDWSFBOZBOZXNXOYTXJ + WNWTWKUUBUUDPWHXJWLYSXKQWMWNWTULWMWNWTUMWMWKYSYBRABCDWSFGHUNUPYTUUAXMFBWM + UUAXMPYSWMDEXTYAVQRUSWMUUDXOPYSWMUUDDXDYCSZBOZXOWMUUCUUEDBWMWHWJWKUUCUUEP + YIXHYBABCYCEFGHYKVHTVRWMWHWIYOXOUUFPYIXGYPABCYCDXDGHYKVSTVTRWAYRVLVEWMWPW + TKZXFWMUUGKZWOWSNOZFBOZWOUUCBOZXCXEUUHXJWPWTWKUUJUUKPWHXJWLUUGXKQWMWPWTUL + WMWPWTUMWMWKUUGYBRZABCWOWSFGHUNUPWMUUJXCPUUGWMUUIXBFBWMDEXTYAWBUSRUUHUUKD + UUCYCSZBOZXEUUHWHWIUUCAIZUUKUUNPWMWHUUGYIRZWMWIUUGXGRUUHWHWSJIZWKUUOUUPWT + UUQWMWPWSWCWDZUULABCWSFGHVJTABCYCDUUCGHYKVSTUUHUUMXDDBUUHWSMZFBOZUUMXDUUH + WHUUQWKUUTUUMPUUPUURUULABCYCWSFGHYKVHTUUHUUSEFBWMUUSEPUUGWMEYAWFRUSVAVRVM + WAVEWEWG $. $} From 3e9c6a0162f21088a8de63122e77d54922d49d3a Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 23 Dec 2024 21:25:30 -0700 Subject: [PATCH 41/49] copy mulgassr from set.mm to iset.mm --- iset.mm | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/iset.mm b/iset.mm index 48000da54..969822d87 100644 --- a/iset.mm +++ b/iset.mm @@ -147122,6 +147122,14 @@ since the target of the homomorphism (operator ` O ` in our model) need UUQWMWPWSWCWDZUULABCWSFGHVJTABCYCDUUCGHYKVSTUUHUUMXDDBUUHWSMZFBOZUUMXDUUH WHUUQWKUUTUUMPUUPUURUULABCYCWSFGHYKVHTUUHUUSEFBWMUUSEPUUGWMEYAWFRUSVAVRVM WAVEWEWG $. + + $( Reversed product of group multiples. (Contributed by Paul Chapman, + 17-Apr-2009.) (Revised by AV, 30-Aug-2021.) $) + mulgassr $p |- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> + ( ( N x. M ) .x. X ) = ( M .x. ( N .x. X ) ) ) $= + ( cgrp wcel cz w3a wa cmul co wceq cc zcn 3ad2ant2 3ad2ant1 adantl oveq1d + mulcomd mulgass eqtrd ) CIJZDKJZEKJZFAJZLZMZEDNOZFBODENOZFBODEFBOBOUKULUM + FBUJULUMPUFUJEDUHUGEQJUIERSUGUHDQJUIDRTUCUAUBABCDEFGHUDUE $. $} From 8fd677f17865023815a8187b8c56963078052244 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 23 Dec 2024 21:40:48 -0700 Subject: [PATCH 42/49] Add mulgmodid to iset.mm Stated as in set.mm. The proof needs real->rational modifications in modulus theorems but is otherwise the set.mm proof. --- iset.mm | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/iset.mm b/iset.mm index 969822d87..d6ef8052f 100644 --- a/iset.mm +++ b/iset.mm @@ -147132,6 +147132,32 @@ since the target of the homomorphism (operator ` O ` in our model) need FBUJULUMPUFUJEDUHUGEQJUIERSUGUHDQJUIDRTUCUAUBABCDEFGHUDUE $. $} + ${ + mulgmodid.b $e |- B = ( Base ` G ) $. + mulgmodid.o $e |- .0. = ( 0g ` G ) $. + mulgmodid.t $e |- .x. = ( .g ` G ) $. + $( Casting out multiples of the identity element leaves the group multiple + unchanged. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, + 30-Aug-2021.) $) + mulgmodid $p |- ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) + /\ ( X e. B /\ ( M .x. X ) = .0. ) ) + -> ( ( N mod M ) .x. X ) = ( N .x. X ) ) $= + ( wcel cz wa co wceq cfv cq adantl 3ad2ant2 oveq1d cgrp w3a cmo cdiv cmul + cn cfl cneg cplusg cmin caddc cc0 clt wbr zq adantr nngt0 modqval syl3anc + nnq cc zcn nnz znq zmulcld zcnd negsubd simp1 simpl znegcld 3ad2ant3 eqid + flqcld mulgdir syl13anc 3eqtr2d nncn mulneg2d mulgassr oveq2 mulgz 3eqtrd + syl2anc eqtr3d oveq2d id mulgcl syl3an grprid ) CUAKZELKZDUFKZMZFAKZDFBNZ + GOZMZUBZEDUCNZFBNZEFBNZDEDUDNZUGPZUENZUHZFBNZCUIPZNZXAGXGNZXAWRWTEXDUJNZF + BNEXEUKNZFBNZXHWRWSXJFBWMWJWSXJOZWQWMEQKZDQKZULDUMUNZXMWKXNWLEUOUPWLXOWKD + UTRWLXPWKDUQREDURUSSTWRXKXJFBWMWJXKXJOWQWMEXDWKEVAKWLEVBUPWMXDWMDXCWLDLKZ + WKDVCRZWMXBEDVDZVMZVEVFVGSTWRWJWKXELKWNXLXHOWJWMWQVHZWMWJWKWQWKWLVIZSWRXD + WRDXCWMWJXQWQXRSZWMWJXCLKWQXTSVEVJWQWJWNWMWNWPVIZVKZAXGBCEXEFHJXGVLZVNVOV + PWRXFGXAXGWRDXCUHZUENZFBNZXFGWRYHXEFBWMWJYHXEOWQWMDXCWLDVAKWKDVQRWMXCXTVF + VRSTWRYIYGWOBNZYGGBNZGWRWJYGLKZXQWNYIYJOYAWRXCWRXBWMWJXBQKWQXSSVMVJZYCYEA + BCYGDFHJVSVOWQWJYJYKOZWMWPYNWNWOGYGBVTRVKWRWJYLYKGOYAYMABCYGGHJIWAWCWBWDW + EWRWJXAAKZXIXAOYAWJWJWMWKWQWNYOWJWFYBYDABCEFHJWGWHAXGCXAGHYFIWIWCWB $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# From 90035086a5a3493f80d417a93ea3893435199603 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 23 Dec 2024 21:43:37 -0700 Subject: [PATCH 43/49] copy mulgsubdir from set.mm to iset.mm --- iset.mm | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/iset.mm b/iset.mm index d6ef8052f..5df99e646 100644 --- a/iset.mm +++ b/iset.mm @@ -147158,6 +147158,23 @@ since the target of the homomorphism (operator ` O ` in our model) need EWRWJXAAKZXIXAOYAWJWJWMWKWQWNYOWJWFYBYDABCEFHJWGWHAXGCXAGHYFIWIWCWB $. $} + ${ + mulgsubdir.b $e |- B = ( Base ` G ) $. + mulgsubdir.t $e |- .x. = ( .g ` G ) $. + mulgsubdir.d $e |- .- = ( -g ` G ) $. + $( Subtraction of a group element from itself. (Contributed by Mario + Carneiro, 13-Dec-2014.) $) + mulgsubdir $p |- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> + ( ( M - N ) .x. X ) = ( ( M .x. X ) .- ( N .x. X ) ) ) $= + ( cgrp wcel cz co cfv wceq eqid zcnd 3adant3r1 mulgcl w3a wa caddc cplusg + cneg znegcl mulgdir syl3anr2 simpr1 simpr2 negsubd oveq1d cminusg mulgneg + cmin oveq2d 3adant3r2 grpsubval syl2anc eqtr4d 3eqtr3d ) CKLZDMLZFMLZGALZ + UAUBZDFUEZUCNZGBNZDGBNZVGGBNZCUDOZNZDFUONZGBNVJFGBNZENZVDVCVBVGMLVEVIVMPF + UFAVLBCDVGGHIVLQZUGUHVFVHVNGBVFDFVFDVBVCVDVEUIRVFFVBVCVDVEUJRUKULVFVMVJVO + CUMOZOZVLNZVPVFVKVSVJVLVBVDVEVKVSPVCABCVRFGHIVRQZUNSUPVFVJALZVOALZVPVTPVB + VCVEWBVDABCDGHITUQVBVDVEWCVCABCFGHITSAVLCVREVJVOHVQWAJURUSUTVA $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# From e7bb0ff414c6783237376b823a5282584a91fc8f Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 23 Dec 2024 21:44:20 -0700 Subject: [PATCH 44/49] copy mhmmulg from set.mm to iset.mm --- iset.mm | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/iset.mm b/iset.mm index 5df99e646..25b065bf1 100644 --- a/iset.mm +++ b/iset.mm @@ -147175,6 +147175,34 @@ since the target of the homomorphism (operator ` O ` in our model) need VCVEWBVDABCDGHITUQVBVDVEWCVCABCFGHITSAVLCVREVJVOHVQWAJURUSUTVA $. $} + ${ + $d m n B $. $d m n F $. $d m n G $. $d m n H $. $d n N $. $d m n X $. + $d m n .x. $. $d m n .X. $. + mhmmulg.b $e |- B = ( Base ` G ) $. + mhmmulg.s $e |- .x. = ( .g ` G ) $. + mhmmulg.t $e |- .X. = ( .g ` H ) $. + $( A homomorphism of monoids preserves group multiples. (Contributed by + Mario Carneiro, 14-Jun-2015.) $) + mhmmulg $p |- ( ( F e. ( G MndHom H ) /\ N e. NN0 /\ X e. B ) -> + ( F ` ( N .x. X ) ) = ( N .X. ( F ` X ) ) ) $= + ( wcel co cfv wceq wi cc0 oveq1 eqeq12d eqid vn vm cn0 cmhm wa cv fvoveq1 + c1 caddc imbi2d c0g mhm0 adantr adantl fveq2d cbs mhmf ffvelcdmda 3eqtr4d + mulg0 syl cplusg cmnd mhmrcl1 ad2antrr simplr mulgnn0p1 syl3anc mulgnn0cl + simpr simpll an32s mhmlin mhmrcl2 syl5ibr expcom a2d nn0ind 3impib 3com12 + eqtrd ) GUCLZDEFUDMLZHALZGHBMDNZGHDNZCMZOZWBWCWDWHWCWDUEZUAUFZHBMDNZWJWFC + MZOZPWIQHBMZDNZQWFCMZOZPWIUBUFZHBMZDNZWRWFCMZOZPWIWRUHUIMZHBMZDNZXCWFCMZO + ZPWIWHPUAUBGWJQOZWMWQWIXHWKWOWLWPWJQHDBUGWJQWFCRSUJWJWROZWMXBWIXIWKWTWLXA + WJWRHDBUGWJWRWFCRSUJWJXCOZWMXGWIXJWKXEWLXFWJXCHDBUGWJXCWFCRSUJWJGOZWMWHWI + XKWKWEWLWGWJGHDBUGWJGWFCRSUJWIEUKNZDNZFUKNZWOWPWCXMXNOWDEFDXNXLXLTZXNTZUL + UMWIWNXLDWDWNXLOWCABEHXLIXOJUTUNUOWIWFFUPNZLZWPXNOWCAXQHDAXQEFDIXQTZUQURZ + XQCFWFXNXSXPKUTVAUSWRUCLZWIXBXGWIYAXBXGPXBXGWIYAUEZWTWFFVBNZMZXAWFYCMZOWT + XAWFYCRYBXEYDXFYEYBXEWSHEVBNZMZDNZYDYBXDYGDYBEVCLZYAWDXDYGOWCYIWDYAEFDVDZ + VEWIYAVJZWCWDYAVFZAYFBEWRHIJYFTZVGVHUOYBWCWSALZWDYHYDOWCWDYAVKWCYAWDYNWCY + AUEZWDUEYIYAWDYNWCYIYAWDYJVEWCYAWDVFYOWDVJABEWRHIJVIVHVLYLAYFYCEFDWSHIYMY + CTZVMVHWAYBFVCLZYAXRXFYEOWCYQWDYAEFDVNVEYKWIXRYAXTUMXQYCCFWRWFXSKYPVGVHSV + OVPVQVRVSVT $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# From 13452575180ff17bd9d157f3ef9fcd5d86f53a4c Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 23 Dec 2024 22:21:25 -0700 Subject: [PATCH 45/49] add mulgpropd to mmil.html --- mmil.raw.html | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index df49ec298..feb42bfda 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -10642,6 +10642,13 @@ the set.mm proof uses mulgnngsum and gsum0 + + mulgpropd + none + presumably would be provable with ` G e. _V ` and ` H e. _V ` + hypotheses added + + df-cnfld and all theorems using CCfld none From 0800fc9d93f8e487088975cf0d4f6f27d4e67d39 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 23 Dec 2024 23:01:31 -0700 Subject: [PATCH 46/49] copy submmulgcl from set.mm to iset.mm --- iset.mm | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/iset.mm b/iset.mm index 25b065bf1..565319ac2 100644 --- a/iset.mm +++ b/iset.mm @@ -147203,6 +147203,18 @@ since the target of the homomorphism (operator ` O ` in our model) need OVPVQVRVSVT $. $} + ${ + $d x y G $. $d x y N $. $d x y S $. $d x .xb $. $d x y X $. + submmulgcl.t $e |- .xb = ( .g ` G ) $. + $( Closure of the group multiple (exponentiation) operation in a submonoid. + (Contributed by Mario Carneiro, 13-Jan-2015.) $) + submmulgcl $p |- ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) -> + ( N .xb X ) e. S ) $= + ( vx vy csubmnd cfv wcel cbs cplusg cmnd c0g eqid submrcl submss submcl + cv subm0cl mulgnn0subcl ) ACIJKGHCLJZCMJZABCDNECOJZUCPZFUDPZACQUCACUFRUDA + CGTHTUGSUEPZACUEUHUAUB $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# From 8855ff949afd1a01c0d90393b1826ac3a187ca11 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 23 Dec 2024 23:04:48 -0700 Subject: [PATCH 47/49] add submmulg to mmil.html --- mmil.raw.html | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index feb42bfda..8e3185bb0 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -10649,6 +10649,12 @@ hypotheses added + + submmulg + none + the set.mm proof uses ressplusg + + df-cnfld and all theorems using CCfld none From 9cd66e0c1a78da814dd6c5fe82c072e6a086fdcc Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Tue, 24 Dec 2024 06:46:52 -0700 Subject: [PATCH 48/49] add pwsmulg to mmil.html --- mmil.raw.html | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index 8e3185bb0..dd436d92c 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -10655,6 +10655,12 @@ the set.mm proof uses ressplusg + + pwsmulg + none + the set.mm proof uses pwspjmhm and pwsmnd + + df-cnfld and all theorems using CCfld none From a446db88443aee2847f57420df1cd4a58fc31d01 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sat, 28 Dec 2024 07:34:23 -0800 Subject: [PATCH 49/49] Correct mulgsubdir comment in set.mm and iset.mm --- iset.mm | 4 ++-- set.mm | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/iset.mm b/iset.mm index 565319ac2..cd6ffc5a9 100644 --- a/iset.mm +++ b/iset.mm @@ -147162,8 +147162,8 @@ since the target of the homomorphism (operator ` O ` in our model) need mulgsubdir.b $e |- B = ( Base ` G ) $. mulgsubdir.t $e |- .x. = ( .g ` G ) $. mulgsubdir.d $e |- .- = ( -g ` G ) $. - $( Subtraction of a group element from itself. (Contributed by Mario - Carneiro, 13-Dec-2014.) $) + $( Distribution of group multiples over subtraction for group elements, + ~ subdir analog. (Contributed by Mario Carneiro, 13-Dec-2014.) $) mulgsubdir $p |- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( M - N ) .x. X ) = ( ( M .x. X ) .- ( N .x. X ) ) ) $= ( cgrp wcel cz co cfv wceq eqid zcnd 3adant3r1 mulgcl w3a wa caddc cplusg diff --git a/set.mm b/set.mm index e48c0fd99..01f5fc4da 100644 --- a/set.mm +++ b/set.mm @@ -231123,8 +231123,8 @@ since the target of the homomorphism (operator ` O ` in our model) need mulgsubdir.b $e |- B = ( Base ` G ) $. mulgsubdir.t $e |- .x. = ( .g ` G ) $. mulgsubdir.d $e |- .- = ( -g ` G ) $. - $( Subtraction of a group element from itself. (Contributed by Mario - Carneiro, 13-Dec-2014.) $) + $( Distribution of group multiples over subtraction for group elements, + ~ subdir analog. (Contributed by Mario Carneiro, 13-Dec-2014.) $) mulgsubdir $p |- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( M - N ) .x. X ) = ( ( M .x. X ) .- ( N .x. X ) ) ) $= ( cgrp wcel cz co cfv wceq eqid zcnd 3adant3r1 mulgcl w3a wa caddc cplusg