From 0303bf91285ad455f71663cb9fd4c1e0778fed2f Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 9 Oct 2023 20:58:57 -0700 Subject: [PATCH] Finish removing +c from set.mm (#3558) * Revise dmdprdpr and dprdpr in set.mm Change from +c to a pair of ordered pairs in stating the theorems and in the proofs. Other than that the proofs are unchanged. * Remove xpscfcda from set.mm No longer used and replaced by xpscf * Remove xpsfrnel2cda from set.mm No longer used and replaced by xpsfrnel2 * Remove xpsc1 from set.mm No longer used and replaced by fvpr1o * Remove xpsc0 from set.mm No longer used and replaced by fvpr0o * Remove xpscfn from set.mm No longer used and replaced by fnpr2o * Revise df-xps in set.mm Change the definition to use a pair of ordered pairs instead of +c . This is the same as what had been a theorem dfxpspr so remove that theorem and update its one usage to refer to df-xps . * Remove xpscg from set.mm No longer used. * Remove xpsc from set.mm No longer used. * Remove cdadju from set.mm As there is no +c left we can just recommend |_| . * Remove cdaval from set.mm Move most of its comment to a section header for the Cardinal number arithmetic section (with some tweaks to the wording). cdaval has no more usages so we can just refer people to df-dju instead. * Remove df-cda and +c from set.mm No longer used. Remove the definition and the syntax and recommend df-dju instead. --- changes-set.txt | 14 +++ discouraged | 5 - set.mm | 253 +++++++++++------------------------------------- 3 files changed, 68 insertions(+), 204 deletions(-) diff --git a/changes-set.txt b/changes-set.txt index e31c434ccf..2f1a716d6e 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -26,6 +26,20 @@ make a github issue.) DONE: Date Old New Notes 6-Oct-23 vtocl2d [same] moved from TA's mathbox to main set.mm + 4-Oct-23 df-cda df-dju use |_| instead of +c + 4-Oct-23 cdaval df-dju use |_| instead of +c + 4-Oct-23 cdadju --- use |_| instead of +c + 4-Oct-23 xpsc --- +c is no longer used or needed + 4-Oct-23 xpscg --- +c is no longer used or needed + 4-Oct-23 dfxpspr df-xps changes from +c to a pair of ordered pairs + 4-Oct-23 df-xps [same] changes from +c to a pair of ordered pairs + 4-Oct-23 xpscfn fnpr2o changes from +c to a pair of ordered pairs + 4-Oct-23 xpsc0 fvpr0o changes from +c to a pair of ordered pairs + 4-Oct-23 xpsc1 fvpr1o changes from +c to a pair of ordered pairs + 4-Oct-23 xpsfrnel2cda xpsfrnel2 changes from +c to a pair of ordered pairs + 4-Oct-23 xpscfcda xpscf changes from +c to a pair of ordered pairs + 4-Oct-23 dprdpr [same] changes from +c to a pair of ordered pairs + 4-Oct-23 dmdprdpr [same] changes from +c to a pair of ordered pairs 2-Oct-23 xpsfeqcda xpsfeq changes from +c to a pair of ordered pairs 2-Oct-23 xpscfv fvprif changes from +c to a pair of ordered pairs 2-Oct-23 xpsfvalcda xpsfval changes from +c to a pair of ordered pairs diff --git a/discouraged b/discouraged index ea24fa1bcd..f429a11cc5 100755 --- a/discouraged +++ b/discouraged @@ -2975,8 +2975,6 @@ "ccshOLD" is used by "0csh0OLD". "ccshOLD" is used by "cshfnOLD". "ccshOLD" is used by "cshnzOLD". -"cdaval" is used by "cdadju". -"cdaval" is used by "xpsc". "cdj3lem1" is used by "cdj3i". "cdj3lem1" is used by "cdj3lem2b". "cdj3lem2" is used by "cdj3i". @@ -4410,7 +4408,6 @@ "df-c" is used by "opelcn". "df-c" is used by "wuncn". "df-cbn" is used by "iscbn". -"df-cda" is used by "cdaval". "df-ch" is used by "isch". "df-ch0" is used by "df0op2". "df-ch0" is used by "elch0". @@ -14253,7 +14250,6 @@ New usage of "ccats1swrdeqOLD" is discouraged (2 uses). New usage of "ccats1swrdeqbiOLD" is discouraged (0 uses). New usage of "ccats1swrdeqrexOLD" is discouraged (1 uses). New usage of "ccshOLD" is discouraged (3 uses). -New usage of "cdaval" is discouraged (2 uses). New usage of "cdj1i" is discouraged (0 uses). New usage of "cdj3i" is discouraged (0 uses). New usage of "cdj3lem1" is discouraged (2 uses). @@ -14746,7 +14742,6 @@ New usage of "df-bnj19" is discouraged (5 uses). New usage of "df-bra" is discouraged (3 uses). New usage of "df-c" is discouraged (12 uses). New usage of "df-cbn" is discouraged (1 uses). -New usage of "df-cda" is discouraged (1 uses). New usage of "df-ch" is discouraged (1 uses). New usage of "df-ch0" is discouraged (8 uses). New usage of "df-chj" is discouraged (1 uses). diff --git a/set.mm b/set.mm index 7a604ce736..fb963226f4 100644 --- a/set.mm +++ b/set.mm @@ -99069,59 +99069,19 @@ our Axiom of Choice (in the form of ~ ac2 ). The proof does not depend =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Cardinal number arithmetic =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= -$) - - $c +c $. $( Cardinal number addition $) - - $( Extend class definition to include cardinal number addition. $) - ccda $a class +c $. - ${ - $d x y $. - $( Define cardinal number addition. Definition of cardinal sum in - [Mendelson] p. 258. See ~ cdaval for its value and a description. - (Contributed by NM, 24-Sep-2004.) Use ~ df-dju instead. - (New usage is discouraged.) $) - df-cda $a |- +c = ( x e. _V , y e. _V |-> - ( ( x X. { (/) } ) u. ( y X. { 1o } ) ) ) $. - $} + For cardinal arithmetic, we follow [Mendelson] p. 258. Rather than + defining operations restricted to cardinal numbers, we use disjoint + union ~ df-dju ( ` |_| ` ) for cardinal addition, Cartesian product + ~ df-xp ( ` X. ` ) for cardinal multiplication, and set exponentiation + ~ df-map ( ` ^m ` ) for cardinal exponentiation. Equinumerosity and + dominance serve the roles of equality and ordering. If we wanted to, + we could easily convert our theorems to actual cardinal number + operations via ~ carden , ~ carddom , and ~ cardsdom . The advantage + of Mendelson's approach is that we can directly use many equinumerosity + theorems that we already have available. - ${ - $d x y A $. $d x y B $. - $( Value of cardinal addition. Definition of cardinal sum in [Mendelson] - p. 258. For cardinal arithmetic, we follow Mendelson. Rather than - defining operations restricted to cardinal numbers, we use Cartesian - product and set exponentiation for cardinal multiplication and - exponentiation. We also use a disjoint union for cardinal addition (the - preferred disjoint union is ~ df-dju ( ` |_| ` ) although some existing - theorems use ~ df-cda ( ` +c ` ) which is very similar). Equinumerosity - and dominance serve the roles of equality and ordering. If we wanted - to, we could easily convert our theorems to actual cardinal number - operations via ~ carden , ~ carddom , and ~ cardsdom . The advantage of - Mendelson's approach is that we can directly use many equinumerosity - theorems that we already have available. (Contributed by NM, - 24-Sep-2004.) (Revised by Mario Carneiro, 15-Sep-2013.) Use ~ df-dju - instead. (New usage is discouraged.) $) - cdaval $p |- ( ( A e. V /\ B e. W ) -> ( A +c B ) = - ( ( A X. { (/) } ) u. ( B X. { 1o } ) ) ) $= - ( vx vy wcel cvv ccda csn cxp c1o cun wceq elex wa xpexg mpan2 cv xpeq1 - co c0 p0ex anim12i unexb sylib uneq1d uneq2d df-cda ovmpog mpd3an3 syl2an - snex ) ACGAHGZBHGZABIUAAUBJZKZBLJZKZMZNZBDGACOBDOUNUOUTHGZVAUNUOPUQHGZUSH - GZPVBUNVCUOVDUNUPHGVCUCAUPHHQRUOURHGVDLUMBURHHQRUDUQUSUEUFEFABHHESZUPKZFS - ZURKZMUTIUQVHMHVEANVFUQVHVEAUPTUGVGBNVHUSUQVGBURTUHEFUIUJUKUL $. - $} - - $( Our two definitions for disjoint union produce equinumerous sets. This is - intended as a transition aid as we move from ` +c ` to ` |_| ` . - (Contributed by Jim Kingdon, 20-Aug-2023.) $) - cdadju $p |- ( ( A e. V /\ B e. W ) -> ( A +c B ) ~~ ( A |_| B ) ) $= - ( wcel c0 csn cxp c1o cun cen wbr cin wceq cvv 0ex xpsneng mpan2 ensymd a1i - wa ccda co cdju adantr xpsnen2g mpan entr syl2anc adantl xp01disj xp01disjl - 1oex unen syl22anc cdaval df-dju 3brtr4d ) ACEZBDEZUAZAFGZHZBIGZHZJZVBAHZVD - BHZJZABUBUCABUDZKVAVCVGKLZVEVHKLVCVEMFNZVGVHMFNZVFVIKLVAVCAKLZAVGKLZVKUSVNU - TUSFOEZVNPAFCOQRUEUSVOUTUSVGAVPUSVGAKLPFAOCUFUGSUEVCAVGUHUIVAVHVEVAVHBKLZBV - EKLVHVEKLUTVQUSIOEZUTVQUMIBODUFUGUJVAVEBUTVEBKLZUSUTVRVSUMBIDOQRUJSVHBVEUHU - ISVLVAABUKTVMVAABULTVCVGVEVHUNUOABCDUPVJVINVAABUQTUR $. +$) $( Cardinal addition dominates union. (Contributed by NM, 28-Sep-2004.) (Revised by Jim Kingdon, 15-Aug-2023.) $) @@ -99191,7 +99151,8 @@ our Axiom of Choice (in the form of ~ ac2 ). The proof does not depend Russell define cardinal addition on collections of all sets equinumerous to 1 and 2 (which for us are proper classes unless we restrict them as in ~ karden ), but after applying definitions, our theorem is equivalent. - The comment for ~ cdaval explains why we use ` ~~ ` instead of =. See + Because we use a disjoint union for cardinal addition (as explained in the + comment at the top of this section), we use ` ~~ ` instead of =. See ~ dju1p1e2ALT for a shorter proof that doesn't use ~ pm54.43 . (Contributed by NM, 5-Apr-2007.) (Proof modification is discouraged.) $) dju1p1e2 $p |- ( 1o |_| 1o ) ~~ 2o $= @@ -196795,10 +196756,11 @@ topology is based on the order and not the extended metric (which would ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) ) $. $( Define a binary product on structures. (Contributed by Mario Carneiro, - 14-Aug-2015.) $) + 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.) $) df-xps $a |- Xs. = ( r e. _V , s e. _V |-> - ( `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> `' ( { x } +c { y } ) ) - "s ( ( Scalar ` r ) Xs_ `' ( { r } +c { s } ) ) ) ) $. + ( `' ( x e. ( Base ` r ) , y e. ( Base ` s ) + |-> { <. (/) , x >. , <. 1o , y >. } ) + "s ( ( Scalar ` r ) Xs_ { <. (/) , r >. , <. 1o , s >. } ) ) ) $. $} ${ @@ -197654,31 +197616,6 @@ topology is based on the order and not the extended metric (which would $} $} - $( A short expression for the pair function mapping ` 0 ` to ` A ` and ` 1 ` - to ` B ` . (Contributed by Mario Carneiro, 14-Aug-2015.) $) - xpsc $p |- `' ( { A } +c { B } ) = - ( ( { (/) } X. { A } ) u. ( { 1o } X. { B } ) ) $= - ( csn ccda co ccnv cxp c1o cun cvv wcel wceq snex cdaval mp2an cnveqi cnvun - c0 cnvxp uneq12i 3eqtri ) ACZBCZDEZFUBRCZGZUCHCZGZIZFUFFZUHFZIUEUBGZUGUCGZI - UDUIUBJKUCJKUDUILAMBMUBUCJJNOPUFUHQUJULUKUMUBUESUCUGSTUA $. - - $( A short expression for the pair function mapping ` 0 ` to ` A ` and ` 1 ` - to ` B ` . (Contributed by Mario Carneiro, 14-Aug-2015.) $) - xpscg $p |- ( ( A e. V /\ B e. W ) -> - `' ( { A } +c { B } ) = { <. (/) , A >. , <. 1o , B >. } ) $= - ( wcel wa c0 csn cxp c1o cun cop ccda co ccnv wceq cvv xpsng mpan con0 xpsc - cpr 0ex 1on uneq12 syl2an df-pr 3eqtr4g ) ACEZBDEZFGHAHZIZJHBHZIZKZGALZHZJB - LZHZKZUKUMMNOUPURUBUIULUQPZUNUSPZUOUTPUJGQEUIVAUCGAQCRSJTEUJVBUDJBTDRSULUQU - NUSUEUFABUAUPURUGUH $. - - $( The pair function is a function on ` 2o = { (/) , 1o } ` . (Contributed - by Mario Carneiro, 14-Aug-2015.) $) - xpscfn $p |- ( ( A e. V /\ B e. W ) -> `' ( { A } +c { B } ) Fn 2o ) $= - ( wcel wa csn ccda co ccnv c2o wfn c0 cop c1o cpr cvv con0 0ex 1on wne 1n0 - necomi fnprg mp3an3 mpanl12 df2o3 fneq2i sylibr xpscg fneq1d mpbird ) ACEBD - EFZAGBGHIJZKLMANOBNPZKLZUMUOMOPZLZUPMQEZOREZUMURSTUSUTFUMMOUAUROMUBUCMOABQR - CDUDUEUFKUQUOUGUHUIUMKUNUOABCDUJUKUL $. - $( Function with a domain of ` 2o ` . (Contributed by Jim Kingdon, 25-Sep-2023.) $) fnpr2o $p |- ( ( A e. V /\ B e. W ) @@ -197705,39 +197642,6 @@ topology is based on the order and not the extended metric (which would FVJVKUNVEWLWKUOUPHVNHBTWEUQPURUSCBUTVAVBVFVG $. $} - ${ - $d x A $. $d x B $. - $( The pair function maps ` 0 ` to ` A ` . (Contributed by Mario Carneiro, - 14-Aug-2015.) $) - xpsc0 $p |- ( A e. V -> ( `' ( { A } +c { B } ) ` (/) ) = A ) $= - ( vx wcel c0 csn cfv cxp c1o wfn cin wceq wfun cid cop wss cvv ax-mp a1i - ccda co ccnv cun xpsc fveq1i cdm fnconstg cv fvi elv elsni fveq2d syl5eqr - velsn sylibr ssriv xpss2 1oex fvex xpsn funsn funss mp2 funfn mpbi dmxpss - sseqtri sslin wne 1n0 necomi disjsn2 sseq0 mp2an 0ex snid fvun1 syl112anc - syl5eq wa xpsng fveq1d fvsng eqtrd mpan ) ACEZFAGZBGZUAUBUCZHZFFGZWHIZHZA - WGWKFWMJGZWIIZUDZHZWNFWJWQABUEUFWGWMWLKWPWPUGZKZWLWSLZFMZFWLEZWRWNMWLACUH - WTWGWPNZWTWPJBOHZPGZQXFNXDWPWOXEGZIZXFWIXGQWPXHQDWIXGDUIZWIEZXIXEMXIXGEXJ - XIXIOHZXEXKXIMDXIRUJUKXJXIBOXIBULUMUNDXEUOUPUQWIXGWOURSJXEUSBOUTZVAVHJXEU - SXLVBWPXFVCVDWPVEVFTXBWGXAWLWOLZQZXMFMZXBWSWOQXNWOWIVGWSWOWLVISFJVJXOJFVK - VLFJVMSXAXMVNVOTXCWGFVPVQTWLWSWMWPFVRVSVTFREZWGWNAMVPXPWGWAZWNFFAPGZHAXQF - WMXRFARCWBWCFARCWDWEWFWE $. - - $( The pair function maps ` 1 ` to ` B ` . (Contributed by Mario Carneiro, - 14-Aug-2015.) $) - xpsc1 $p |- ( B e. V -> ( `' ( { A } +c { B } ) ` 1o ) = B ) $= - ( vx wcel c1o csn cfv cxp c0 wfn cin wceq wfun cid cop wss ax-mp a1i con0 - ccda co ccnv cun xpsc fveq1i cdm cv cvv fvi elv elsni fveq2d velsn sylibr - syl5eqr ssriv xpss2 0ex fvex xpsn sseqtri funsn funss funfn mpbi fnconstg - mp2 dmxpss ssrin wne necomi disjsn2 sseq0 mp2an 1oex snid fvun2 syl112anc - 1n0 syl5eq 1on wa xpsng fveq1d fvsng eqtrd mpan ) BCEZFAGZBGZUAUBUCZHZFFG - ZWKIZHZBWIWMFJGZWJIZWOUDZHZWPFWLWSABUEUFWIWRWRUGZKZWOWNKXAWNLZJMZFWNEZWTW - PMXBWIWRNZXBWRJAOHZPGZQXHNXFWRWQXGGZIZXHWJXIQWRXJQDWJXIDUHZWJEZXKXGMXKXIE - XLXKXKOHZXGXMXKMDXKUIUJUKXLXKAOXKAULUMUPDXGUNUOUQWJXIWQURRJXGUSAOUTZVAVBJ - XGUSXNVCWRXHVDVHWRVEVFSWNBCVGXDWIXCWQWNLZQZXOJMZXDXAWQQXPWQWJVIXAWQWNVJRJ - FVKXQFJVTVLJFVMRXCXOVNVOSXEWIFVPVQSXAWNWRWOFVRVSWAFTEZWIWPBMWBXRWIWCZWPFF - BPGZHBXSFWOXTFBTCWDWEFBTCWFWGWHWG $. - $} - $( The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.) $) fvpr0o $p |- ( A e. V -> ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) = A ) $= @@ -197761,21 +197665,6 @@ topology is based on the order and not the extended metric (which would VBNZBVCVDUTVKBJZVEURUQVLUSABEUDUEQVJCLVBUTVERZSVJVAABVJVALIJLIUFULVJCLIVMUG UHUITUSUQVAVEUJZURVNCILMGCILUKUMUNUOUP $. - ${ - $d r s x y $. - $( Define a binary product on structures. (Contributed by Mario Carneiro, - 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.) $) - dfxpspr $p |- Xs. = ( r e. _V , s e. _V |-> - ( `' ( x e. ( Base ` r ) , y e. ( Base ` s ) - |-> { <. (/) , x >. , <. 1o , y >. } ) - "s ( ( Scalar ` r ) Xs_ { <. (/) , r >. , <. 1o , s >. } ) ) ) $= - ( cvv cv cbs cfv csn ccda co ccnv cmpo cprds cimas c0 cop c1o cpr wceq wa - cxps csca df-xps wcel xpscg mpoeq3ia cnveqi el2v oveq2i oveq12i a1i eqtri - ) UBDCEEABDFZGHZCFZGHZAFZIBFZIJKLZMZLZUNUCHZUNIUPIJKLZNKZOKZMDCEEABUOUQPU - RQRUSQSZMZLZVCPUNQRUPQSZNKZOKZMABCDUDDCEEVFVLVFVLTUNEUEUPEUEUAVBVIVEVKOVA - VHABUOUQUTVGURUSUOUQUFUGUHVDVJVCNVDVJTDCUNUPEEUFUIUJUKULUGUM $. - $} - ${ $d k A $. $d k B $. $d k G $. $d k X $. $d k Y $. $( Elementhood in the target space of the function ` F ` appearing in @@ -197790,37 +197679,6 @@ topology is based on the order and not the extended metric (which would WFVQVNWEVQVPCGMUGZKWFVPCEWGUHUIVPVTWBCGMUJUKVKVOVSVLAVJGDNVKABULOVJMHZVOW AVLBVJMDNWHVJGPZVLBHWHWIMGPUNVJMGUMUOVJGABUPUQOURQVNVMVQVNDRVNERIZDRIEVFI WJUSEUTVAEDVBVCVDVEVGVHVNVMVQSVNVTWBSVIQQ $. - - $( Elementhood in the target space of the function - ` ``' ( { X } +c { Y } ) ` . (Contributed by Mario Carneiro, - 15-Aug-2015.) $) - xpsfrnel2cda $p |- ( `' ( { X } +c { Y } ) e. - X_ k e. 2o if ( k = (/) , A , B ) <-> ( X e. A /\ Y e. B ) ) $= - ( csn c2o c0 wceq wcel cfv c1o wa cvv cxp cdm cun 0ex elsni sylbi ccda co - ccnv cv cif cixp wfn w3a xpsfrnel cpr prid1 df2o3 eleqtrri fndm syl5eleqr - xpsc dmeqi dmun eqtri syl6eleq elun wbr wex eldm brxp syl6eqelr simplbiim - vex exlimiv dmxpss sseli 1n0 neii pm2.21i eqcoms 3syl jaoi syl 1oex prid2 - wo jca 3ad2ant1 elex anim12i 3anass xpscfn biantrurd xpsc0 xpsc1 bi2anan9 - eleq1d bitr3d syl5bb pm5.21nii bitri ) DFZEFZUAUBUCZCGCUDZHIABUEUFJWSGUGZ - HWSKZAJZLWSKZBJZUHZDAJZEBJZMZABCWSUIXFDNJZENJZMZXIXAXCXLXEXAXJXKXAHHFZWQO - ZPZLFZWROZPZQZJZXJXAHWSPZXSXAHGYAHHLUJZGHLRUKULUMGWSUNZUOYAXNXQQZPXSWSYDD - EUPUQXNXQURUSZUTXTHXOJZHXRJZWAXJHXOXRVAYFXJYGYFHWTXNVBZCVCXJCHXNRVDYHXJCY - HHXMJWTWQJZXJHWTXMWQVEYIDWTNWTDSCVHZVFVGVITYGHXPJHLIXJXRXPHXPWRVJVKHLSXJL - HLHIZXJLHVLVMZVNVOVPVQTVRXALXSJZXKXALYAXSXALGYALYBGHLVSVTULUMYCUOYEUTYMLX - OJZLXRJZWAXKLXOXRVAYNXKYOYNLXMJYKXKXOXMLXMWQVJVKLHSYKXKYLVNVPYOLWTXQVBZCV - CXKCLXQVSVDYPXKCYPLXPJWTWRJZXKLWTXPWRVEYQEWTNWTESYJVFVGVITVQTVRWBWCXGXJXH - XKDAWDEBWDWEXFXAXCXEMZMZXLXIXAXCXEWFXLYRYSXIXLXAYRDENNWGWHXJXCXGXKXEXHXJX - BDADENWIWLXKXDEBDENWJWLWKWMWNWOWP $. - - $( Equivalent condition for the pair function to be a proper function on - ` A ` . (Contributed by Mario Carneiro, 20-Aug-2015.) $) - xpscfcda $p |- ( `' ( { X } +c { Y } ) : 2o --> A <-> - ( X e. A /\ Y e. A ) ) $= - ( vk c2o csn ccda co ccnv wf cv c0 wceq cif cixp wcel wa wfn cfv wral - ifid eleq2i ralbii anbi2i cnvex elixp ffnfv 3bitr4i xpsfrnel2cda bitr3i - ovex ) EABFZCFZGHZIZJZUODEDKZLMZAANZOPZBAPCAPQUOERZUQUOSZUSPZDETZQVAVBAPZ - DETZQUTUPVDVFVAVCVEDEUSAVBURAUAUBUCUDDEUSUOUNULUMGUKUEUFDEAUOUGUHAADBCUIU - J $. $} ${ @@ -197932,13 +197790,13 @@ topology is based on the order and not the extended metric (which would xpsval $p |- ( ph -> T = ( `' F "s U ) ) $= ( vr vs cxps co ccnv cimas cvv wcel wceq elexd cbs cfv cop c1o cpr cmpo cv c0 csca cprds fveq2 syl6eqr mpoeq12 syl2an cnveqd adantr simpl simpr - wa opeq2d preq12d oveq12d dfxpspr ovex ovmpoa syl2anc syl5eq ) AFDEUDUE - ZHUFZGUGUEZNADUHUIEUHUIVSWAUJADJQUKAEKRUKUBUCDEUHUHBCUBURZULUMZUCURZULU - MZUSBURUNUOCURUNUPZUQZUFZWBUTUMZUSWBUNZUOWDUNZUPZVAUEZUGUEWAUDWBDUJZWDE - UJZVJZWHVTWMGUGWPWGHWPWGBCLMWFUQZHWNWCLUJWEMUJWGWQUJWOWNWCDULUMLWBDULVB - OVCWOWEEULUMMWDEULVBPVCBCWCWELMWFVDVESVCVFWPWMIUSDUNZUOEUNZUPZVAUEGWPWI - IWLWTVAWPWIDUTUMZIWNWIXAUJWOWBDUTVBVGTVCWPWJWRWKWSWPWBDUSWNWOVHVKWPWDEU - OWNWOVIVKVLVMUAVCVMBCUCUBVNVTGUGVOVPVQVR $. + wa opeq2d preq12d oveq12d df-xps ovex ovmpoa syl2anc syl5eq ) AFDEUDUEZ + HUFZGUGUEZNADUHUIEUHUIVSWAUJADJQUKAEKRUKUBUCDEUHUHBCUBURZULUMZUCURZULUM + ZUSBURUNUOCURUNUPZUQZUFZWBUTUMZUSWBUNZUOWDUNZUPZVAUEZUGUEWAUDWBDUJZWDEU + JZVJZWHVTWMGUGWPWGHWPWGBCLMWFUQZHWNWCLUJWEMUJWGWQUJWOWNWCDULUMLWBDULVBO + VCWOWEEULUMMWDEULVBPVCBCWCWELMWFVDVESVCVFWPWMIUSDUNZUOEUNZUPZVAUEGWPWII + WLWTVAWPWIDUTUMZIWNWIXAUJWOWBDUTVBVGTVCWPWJWRWKWSWPWBDUSWNWOVHVKWPWDEUO + WNWOVIVKVLVMUAVCVMBCUCUBVNVTGUGVOVPVQVR $. $( The indexed structure product that appears in ~ xpsval has the same base as the target of the function ` F ` . (Contributed by Mario @@ -237131,42 +236989,43 @@ G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) $. dmdprdpr.t $e |- ( ph -> T e. ( SubGrp ` G ) ) $. $( A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.) $) - dmdprdpr $p |- ( ph -> ( G dom DProd `' ( { S } +c { T } ) <-> + dmdprdpr $p |- ( ph -> ( G dom DProd { <. (/) , S >. , <. 1o , T >. } <-> ( S C_ ( Z ` T ) /\ ( S i^i T ) = { .0. } ) ) ) $= - ( csn co cdprd wbr c0 c1o wceq wa wcel c2o ccda ccnv cdm cres cfv wss cin - wb cop cvv csubg 0ex dprdsn sylancr simpld wfn xpscfcda sylanbrc ffnd cpr - wf prid1 df2o3 eleqtrri fnressn sylancl xpsc0 opeq2d sneqd eqtrd breqtrrd - syl con0 1on 1oex prid2 xpsc1 w3a wne 1n0 necomi disjsn2 mp1i df-pr eqtri - cun a1i dmdprdsplit 3anass syl6bb ex mp2and oveq2d simprd sseq12d ineq12d - baibd fveq2d eqeq1d anbi12d bitrd ) ADBKCKUALUBZMUCZNZDXBOKZUDZMLZDXBPKZU - DZMLZFUEZUFZXGXJUGZEKZQZRZBCFUEZUFZBCUGZXNQZRADXFXCNZDXIXCNZXDXPUHZADOBUI - ZKZXFXCADYEXCNZDYEMLZBQZAOUJSBDUKUEZSZYFYHRULIOBDUJUMUNZUOAXFOOXBUEZUIZKZ - YEAXBTUPZOTSXFYNQATYIXBAYJCYISZTYIXBVAIJYIBCUQURZUSZOOPUTZTOPULVBVCVDTOXB - VEVFAYMYDAYLBOAYJYLBQIBCYIVGVLVHVIVJZVKADPCUIZKZXIXCADUUBXCNZDUUBMLZCQZAP - VMSYPUUCUUERVNJPCDVMUMUNZUOAXIPPXBUEZUIZKZUUBAYOPTSXIUUIQYRPYSTOPVOVPVCVD - TPXBVEVFAUUHUUAAUUGCPAYPUUGCQJBCYIVQVLVHVIVJZVKAYAYBRZYCAXDUUKXPAXDUUKXLX - OVRUUKXPRAXEXHXBDTEFYQOPVSXEXHUGOQAPOVTWAOPWBWCTXEXHWFZQATYSUULVCOPWDWEWG - GHWHUUKXLXOWIWJWQWKWLAXLXRXOXTAXGBXKXQAXGYGBAXFYEDMYTWMAYFYHYKWNVJZAXJCFA - XJUUDCAXIUUBDMUUJWMAUUCUUEUUFWNVJZWRWOAXMXSXNAXGBXJCUUMUUNWPWSWTXA $. + ( c0 c1o cdprd wbr csn cfv wceq wa wcel c2o cop cpr cdm co wss cin wb cvv + cres csubg 0ex dprdsn sylancr simpld wfn wf xpscf sylanbrc prid1 eleqtrri + ffnd df2o3 fnressn sylancl fvpr0o syl opeq2d sneqd breqtrrd con0 1on 1oex + eqtrd prid2 fvpr1o w3a wne 1n0 necomi disjsn2 cun df-pr eqtri dmdprdsplit + mp1i a1i 3anass syl6bb mp2and oveq2d simprd fveq2d sseq12d ineq12d eqeq1d + baibd ex anbi12d bitrd ) ADKBUAZLCUAZUBZMUCZNZDXBKOZUIZMUDZDXBLOZUIZMUDZF + PZUEZXGXJUFZEOZQZRZBCFPZUEZBCUFZXNQZRADXFXCNZDXIXCNZXDXPUGZADWTOZXFXCADYD + XCNZDYDMUDZBQZAKUHSBDUJPZSZYEYGRUKIKBDUHULUMZUNAXFKKXBPZUAZOZYDAXBTUOZKTS + XFYMQATYHXBAYICYHSZTYHXBUPIJYHBCUQURZVAZKKLUBZTKLUKUSVBUTTKXBVCVDAYLWTAYK + BKAYIYKBQIBCYHVEVFVGVHVMZVIADXAOZXIXCADYTXCNZDYTMUDZCQZALVJSYOUUAUUCRVKJL + CDVJULUMZUNAXILLXBPZUAZOZYTAYNLTSXIUUGQYQLYRTKLVLVNVBUTTLXBVCVDAUUFXAAUUE + CLAYOUUECQJBCYHVOVFVGVHVMZVIAYAYBRZYCAXDUUIXPAXDUUIXLXOVPUUIXPRAXEXHXBDTE + FYPKLVQXEXHUFKQALKVRVSKLVTWETXEXHWAZQATYRUUJVBKLWBWCWFGHWDUUIXLXOWGWHWPWQ + WIAXLXRXOXTAXGBXKXQAXGYFBAXFYDDMYSWJAYEYGYJWKVMZAXJCFAXJUUBCAXIYTDMUUHWJA + UUAUUCUUDWKVMZWLWMAXMXSXNAXGBXJCUUKUULWNWOWRWS $. dprdpr.s $e |- .(+) = ( LSSum ` G ) $. dprdpr.1 $e |- ( ph -> S C_ ( Z ` T ) ) $. dprdpr.2 $e |- ( ph -> ( S i^i T ) = { .0. } ) $. $( A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 26-Apr-2016.) $) - dprdpr $p |- ( ph -> ( G DProd `' ( { S } +c { T } ) ) = ( S .(+) T ) ) $= - ( csn co c0 c1o c2o wceq ccda ccnv cdprd cres csubg cfv xpscfcda sylanbrc - wcel wf wne cin 1n0 necomi disjsn2 mp1i cun cpr df2o3 df-pr eqtri a1i cdm - wbr wss dmdprdpr mpbir2and dprdsplit cop wfn 0ex eleqtrri fnressn sylancl - ffnd prid1 xpsc0 syl opeq2d sneqd eqtrd oveq2d cvv wa dprdsn sylancr 1oex - simprd prid2 xpsc1 con0 1on oveq12d ) AECODOUAPUBZUCPEWNQOZUDZUCPZEWNROZU - DZUCPZBPCDBPAWOWRBWNESACEUEUFZUIZDXAUIZSXAWNUJJKXACDUGUHZQRUKWOWRULQTARQU - MUNQRUOUPSWOWRUQZTASQRURZXEUSQRUTVAVBLAEWNUCVCZVDCDGUFVECDULFOTMNACDEFGHI - JKVFVGVHAWQCWTDBAWQEQCVIZOZUCPZCAWPXIEUCAWPQQWNUFZVIZOZXIAWNSVJZQSUIWPXMT - ASXAWNXDVOZQXFSQRVKVPUSVLSQWNVMVNAXLXHAXKCQAXBXKCTJCDXAVQVRVSVTWAWBAEXIXG - VDZXJCTZAQWCUIXBXPXQWDVKJQCEWCWEWFWHWAAWTERDVIZOZUCPZDAWSXSEUCAWSRRWNUFZV - IZOZXSAXNRSUIWSYCTXORXFSQRWGWIUSVLSRWNVMVNAYBXRAYADRAXCYADTKCDXAWJVRVSVTW - AWBAEXSXGVDZXTDTZARWKUIXCYDYEWDWLKRDEWKWEWFWHWAWMWA $. + dprdpr $p |- ( ph + -> ( G DProd { <. (/) , S >. , <. 1o , T >. } ) = ( S .(+) T ) ) $= + ( c0 c1o cdprd co c2o wceq cop cpr csn cres csubg cfv wcel xpscf sylanbrc + wf wne cin 1n0 necomi disjsn2 mp1i cun df2o3 df-pr eqtri a1i cdm dmdprdpr + wbr wss mpbir2and dprdsplit wfn 0ex prid1 eleqtrri fnressn sylancl fvpr0o + ffnd syl opeq2d sneqd eqtrd oveq2d cvv dprdsn sylancr simprd prid2 fvpr1o + wa 1oex con0 1on oveq12d ) AEOCUAZPDUAZUBZQREWNOUCZUDZQRZEWNPUCZUDZQRZBRC + DBRAWOWRBWNESACEUEUFZUGZDXAUGZSXAWNUJJKXACDUHUIZOPUKWOWRULOTAPOUMUNOPUOUP + SWOWRUQZTASOPUBZXEUROPUSUTVALAEWNQVBZVDCDGUFVECDULFUCTMNACDEFGHIJKVCVFVGA + WQCWTDBAWQEWLUCZQRZCAWPXHEQAWPOOWNUFZUAZUCZXHAWNSVHZOSUGWPXLTASXAWNXDVOZO + XFSOPVIVJURVKSOWNVLVMAXKWLAXJCOAXBXJCTJCDXAVNVPVQVRVSVTAEXHXGVDZXICTZAOWA + UGXBXOXPWGVIJOCEWAWBWCWDVSAWTEWMUCZQRZDAWSXQEQAWSPPWNUFZUAZUCZXQAXMPSUGWS + YATXNPXFSOPWHWEURVKSPWNVLVMAXTWMAXSDPAXCXSDTKCDXAWFVPVQVRVSVTAEXQXGVDZXRD + TZAPWIUGXCYBYCWGWJKPDEWIWBWCWDVSWKVS $. $} ${ @@ -435489,10 +435348,6 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the htmldef "CHOICE" as "CHOICE"; althtmldef "CHOICE" as "CHOICE"; latexdef "CHOICE" as "\mathrm{CHOICE}"; -htmldef "+c" as - " +c "; - althtmldef "+c" as ' +𝑐 '; - latexdef "+c" as "+_c"; htmldef "Fin1a" as "FinIa"; althtmldef "Fin1a" as "FinIa"; latexdef "Fin1a" as "\mathrm{Fin1a}";