From 268641b66e4a8cfdbca8571ca4c0e38e397acca6 Mon Sep 17 00:00:00 2001 From: avekens Date: Wed, 6 Nov 2024 17:29:11 +0100 Subject: [PATCH] Revision for .r * Usage of df-mulr discouraged * new theorems ~starvndxnplusgndx , ~starvndxnmulrndx extracted from proofs for ~hlhilslem , ~hlhilsbase , +hlhilsplus , ~hlhilsmul * proof of ~zlmsca shortened * ~zlmlem , ~zlmbas, +zlmplusg, ~zlmmulr revised * ~znbaslem , ~znbas2 , +znadd , ~znmul revised * ~hlhilslem , ~hlhilsbase , +hlhilsplus , ~hlhilsmul revised --- discouraged | 43 +++++++++++ set.mm | 205 ++++++++++++++++++++++++++++++++++++++++++---------- 2 files changed, 210 insertions(+), 38 deletions(-) diff --git a/discouraged b/discouraged index 56d78883e8..7d1dc4604a 100644 --- a/discouraged +++ b/discouraged @@ -4897,6 +4897,15 @@ "df-mr" is used by "mulsrpr". "df-mul" is used by "axmulf". "df-mul" is used by "mulcnsr". +"df-mulr" is used by "hlhilsmulOLD". +"df-mulr" is used by "mulrid". +"df-mulr" is used by "mulrndx". +"df-mulr" is used by "opsrmulrOLD". +"df-mulr" is used by "resvmulrOLD". +"df-mulr" is used by "sramulrOLD". +"df-mulr" is used by "tngmulrOLD". +"df-mulr" is used by "zlmmulrOLD". +"df-mulr" is used by "znmulOLD". "df-ni" is used by "dmaddpi". "df-ni" is used by "dmmulpi". "df-ni" is used by "elni". @@ -7320,6 +7329,9 @@ "hlex" is used by "axhilex-zf". "hlex" is used by "h2hcau". "hlex" is used by "h2hlm". +"hlhilslemOLD" is used by "hlhilsbaseOLD". +"hlhilslemOLD" is used by "hlhilsmulOLD". +"hlhilslemOLD" is used by "hlhilsplusOLD". "hlim0" is used by "hsn0elch". "hlimadd" is used by "chscllem4". "hlimcaui" is used by "chscllem2". @@ -13914,6 +13926,12 @@ "zfinf" is used by "axinfndlem1". "zfpair" is used by "axprALT". "zfun" is used by "axunndlem1". +"zlmlemOLD" is used by "zlmbasOLD". +"zlmlemOLD" is used by "zlmmulrOLD". +"zlmlemOLD" is used by "zlmplusgOLD". +"znbaslemOLD" is used by "znaddOLD". +"znbaslemOLD" is used by "znbas2OLD". +"znbaslemOLD" is used by "znmulOLD". "zrdivrng" is used by "dvrunz". New usage of "00sr" is discouraged (4 uses). New usage of "0bdop" is discouraged (2 uses). @@ -15616,6 +15634,7 @@ New usage of "df-mpq" is discouraged (3 uses). New usage of "df-mq" is discouraged (2 uses). New usage of "df-mr" is discouraged (2 uses). New usage of "df-mul" is discouraged (2 uses). +New usage of "df-mulr" is discouraged (9 uses). New usage of "df-ni" is discouraged (7 uses). New usage of "df-nlfn" is discouraged (1 uses). New usage of "df-nmcv" is discouraged (1 uses). @@ -16648,6 +16667,10 @@ New usage of "hldir" is discouraged (1 uses). New usage of "hlex" is discouraged (3 uses). New usage of "hlexch4N" is discouraged (0 uses). New usage of "hlhils1N" is discouraged (0 uses). +New usage of "hlhilsbaseOLD" is discouraged (0 uses). +New usage of "hlhilslemOLD" is discouraged (3 uses). +New usage of "hlhilsmulOLD" is discouraged (0 uses). +New usage of "hlhilsplusOLD" is discouraged (0 uses). New usage of "hlim0" is discouraged (1 uses). New usage of "hlim2" is discouraged (0 uses). New usage of "hlimadd" is discouraged (1 uses). @@ -19094,6 +19117,14 @@ New usage of "zfinf" is discouraged (2 uses). New usage of "zfpair" is discouraged (1 uses). New usage of "zfregs2VD" is discouraged (0 uses). New usage of "zfun" is discouraged (1 uses). +New usage of "zlmbasOLD" is discouraged (0 uses). +New usage of "zlmlemOLD" is discouraged (3 uses). +New usage of "zlmmulrOLD" is discouraged (0 uses). +New usage of "zlmplusgOLD" is discouraged (0 uses). +New usage of "znaddOLD" is discouraged (0 uses). +New usage of "znbas2OLD" is discouraged (0 uses). +New usage of "znbaslemOLD" is discouraged (3 uses). +New usage of "znmulOLD" is discouraged (0 uses). New usage of "zrdivrng" is discouraged (1 uses). Proof modification of "0cnALT" is discouraged (82 steps). Proof modification of "0cnALT2" is discouraged (49 steps). @@ -20152,6 +20183,10 @@ Proof modification of "hbsbwOLD" is discouraged (15 steps). Proof modification of "helloworld" is discouraged (29 steps). Proof modification of "hhssbnOLD" is discouraged (39 steps). Proof modification of "hirstL-ax3" is discouraged (34 steps). +Proof modification of "hlhilsbaseOLD" is discouraged (20 steps). +Proof modification of "hlhilslemOLD" is discouraged (94 steps). +Proof modification of "hlhilsmulOLD" is discouraged (20 steps). +Proof modification of "hlhilsplusOLD" is discouraged (20 steps). Proof modification of "icccmpALT" is discouraged (71 steps). Proof modification of "id1" is discouraged (2 steps). Proof modification of "idALT" is discouraged (26 steps). @@ -20891,3 +20926,11 @@ Proof modification of "zfcndreg" is discouraged (29 steps). Proof modification of "zfcndrep" is discouraged (258 steps). Proof modification of "zfcndun" is discouraged (72 steps). Proof modification of "zfregs2VD" is discouraged (128 steps). +Proof modification of "zlmbasOLD" is discouraged (18 steps). +Proof modification of "zlmlemOLD" is discouraged (161 steps). +Proof modification of "zlmmulrOLD" is discouraged (18 steps). +Proof modification of "zlmplusgOLD" is discouraged (18 steps). +Proof modification of "znaddOLD" is discouraged (13 steps). +Proof modification of "znbas2OLD" is discouraged (13 steps). +Proof modification of "znbaslemOLD" is discouraged (77 steps). +Proof modification of "znmulOLD" is discouraged (13 steps). diff --git a/set.mm b/set.mm index a95b1d9be2..738094b65c 100644 --- a/set.mm +++ b/set.mm @@ -200340,7 +200340,8 @@ C_ dom ( S sSet <. I , E >. ) ) $= df-plusg $a |- +g = Slot 2 $. $( Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by - Mario Carneiro, 14-Aug-2015.) $) + Mario Carneiro, 14-Aug-2015.) Use its index-independent form ~ mulrid + instead. (New usage is discouraged.) $) df-mulr $a |- .r = Slot 3 $. $( Define the involution function of a *-ring. (Contributed by NM, @@ -200594,6 +200595,20 @@ base set is not the slot for the ring (multiplication) operation in an ( cnx cstv cfv cbs wne c4 c1 1re 1lt4 gtneii starvndx basendx neeq12i mpbir ) ABCZADCZEFGEGFHIJOFPGKLMN $. + $( The slot for the involution function is not the slot for the base set in + an extensible structure. Formerly part of proof for ~ ressstarv . + (Contributed by AV, 18-Oct-2024.) $) + starvndxnplusgndx $p |- ( *r ` ndx ) =/= ( +g ` ndx ) $= + ( cnx cstv cfv cplusg wne c4 c2 2lt4 gtneii starvndx plusgndx neeq12i mpbir + 2re ) ABCZADCZEFGEGFNHIOFPGJKLM $. + + $( The slot for the involution function is not the slot for the base set in + an extensible structure. Formerly part of proof for ~ ressstarv . + (Contributed by AV, 18-Oct-2024.) $) + starvndxnmulrndx $p |- ( *r ` ndx ) =/= ( .r ` ndx ) $= + ( cnx cstv cfv cmulr wne c4 3re 3lt4 gtneii starvndx mulrndx neeq12i mpbir + c3 ) ABCZADCZEFNENFGHIOFPNJKLM $. + ${ ressmulr.1 $e |- S = ( R |`s A ) $. ${ @@ -261685,12 +261700,26 @@ According to Wikipedia ("Integer", 25-May-2019, ${ zlmbas.w $e |- W = ( ZMod ` G ) $. ${ - zlmlem.2 $e |- E = Slot N $. - zlmlem.3 $e |- N e. NN $. - zlmlem.4 $e |- N < 5 $. + zlmlem.2 $e |- E = Slot ( E ` ndx ) $. + zlmlem.3 $e |- ( E ` ndx ) =/= ( Scalar ` ndx ) $. + zlmlem.4 $e |- ( E ` ndx ) =/= ( .s ` ndx ) $. $( Lemma for ~ zlmbas and ~ zlmplusg . (Contributed by Mario Carneiro, - 2-Oct-2015.) $) + 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) $) zlmlem $p |- ( E ` G ) = ( E ` W ) $= + ( cvv wcel cfv wceq cnx csca zring cop csts co cvsca setsnid c0 eqtr4id + cmg eqtri eqid zlmval fveq2d czlm str0 eqcomi fveqprc pm2.61i ) BHIZBAJ + ZCAJZKULUMBLMJZNOPQZLRJZBUBJZOPQZAJZUNUMUPAJUTNUOABEFSURUQAUPEGSUCULCUS + AURBHCDURUDUEUFUAAUGBCTTAJALAJEUHUIDUJUK $. + $} + + ${ + zlmlemOLD.2 $e |- E = Slot N $. + zlmlemOLD.3 $e |- N e. NN $. + zlmlemOLD.4 $e |- N < 5 $. + $( Obsolete version of ~ zlmlem as of 3-Nov-2024. Lemma for ~ zlmbas and + ~ zlmplusg . (Contributed by Mario Carneiro, 2-Oct-2015.) + (New usage is discouraged.) (Proof modification is discouraged.) $) + zlmlemOLD $p |- ( E ` G ) = ( E ` W ) $= ( cvv cfv cnx zring cop csts co c5 clt c6 wbr c0 wcel wceq cvsca cmg cr csca ndxid ndxarg nnrei eqeltri eqbrtri ltneii scandx neeqtrri 5lt6 5re setsnid lttri mp2an vscandx eqtri eqid zlmval fveq2d eqtr4id str0 fvprc @@ -261704,35 +261733,58 @@ According to Wikipedia ("Integer", 25-May-2019, ${ zlmbas.2 $e |- B = ( Base ` G ) $. $( Base set of a ` ZZ ` -module. (Contributed by Mario Carneiro, - 2-Oct-2015.) $) + 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) $) zlmbas $p |- B = ( Base ` W ) $= - ( cbs cfv c1 df-base 1nn 1lt5 zlmlem eqtri ) ABFGCFGEFBHCDIJKLM $. + ( cbs cfv baseid cnx scandxnbasendx necomi cvsca vscandxnbasendx zlmlem + csca eqtri ) ABFGCFGEFBCDHIOGIFGZJKILGQMKNP $. + + $( Obsolete version of ~ zlmbas as of 3-Nov-2024. Base set of a + ` ZZ ` -module. (Contributed by Mario Carneiro, 2-Oct-2015.) + (New usage is discouraged.) (Proof modification is discouraged.) $) + zlmbasOLD $p |- B = ( Base ` W ) $= + ( cbs cfv c1 df-base 1nn 1lt5 zlmlemOLD eqtri ) ABFGCFGEFBHCDIJKLM $. $} ${ zlmplusg.2 $e |- .+ = ( +g ` G ) $. $( Group operation of a ` ZZ ` -module. (Contributed by Mario Carneiro, - 2-Oct-2015.) $) + 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) $) zlmplusg $p |- .+ = ( +g ` W ) $= - ( cplusg cfv c2 df-plusg 2nn 2lt5 zlmlem eqtri ) ABFGCFGEFBHCDIJKLM $. + ( cplusg cfv plusgid csca scandxnplusgndx necomi cvsca vscandxnplusgndx + cnx zlmlem eqtri ) ABFGCFGEFBCDHNIGNFGZJKNLGQMKOP $. + + $( Obsolete version of ~ zlmbas as of 3-Nov-2024. Group operation of a + ` ZZ ` -module. (Contributed by Mario Carneiro, 2-Oct-2015.) + (New usage is discouraged.) (Proof modification is discouraged.) $) + zlmplusgOLD $p |- .+ = ( +g ` W ) $= + ( cplusg cfv c2 df-plusg 2nn 2lt5 zlmlemOLD eqtri ) ABFGCFGEFBHCDIJKLM + $. $} ${ zlmmulr.2 $e |- .x. = ( .r ` G ) $. $( Ring operation of a ` ZZ ` -module (if present). (Contributed by - Mario Carneiro, 2-Oct-2015.) $) + Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) $) zlmmulr $p |- .x. = ( .r ` W ) $= - ( cmulr cfv c3 df-mulr 3nn 3lt5 zlmlem eqtri ) ABFGCFGEFBHCDIJKLM $. + ( cmulr cfv mulrid cnx csca scandxnmulrndx necomi cvsca vscandxnmulrndx + zlmlem eqtri ) ABFGCFGEFBCDHIJGIFGZKLIMGQNLOP $. + + $( Obsolete version of ~ zlmbas as of 3-Nov-2024. Ring operation of a + ` ZZ ` -module (if present). (Contributed by Mario Carneiro, + 2-Oct-2015.) (New usage is discouraged.) + (Proof modification is discouraged.) $) + zlmmulrOLD $p |- .x. = ( .r ` W ) $= + ( cmulr cfv c3 df-mulr 3nn 3lt5 zlmlemOLD eqtri ) ABFGCFGEFBHCDIJKLM $. $} $( Scalar ring of a ` ZZ ` -module. (Contributed by Mario Carneiro, - 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) $) + 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) (Proof shortened by AV, + 2-Nov-2024.) $) zlmsca $p |- ( G e. V -> ZZring = ( Scalar ` W ) ) $= - ( wcel cnx csca cfv zring cop csts co cvsca cmg scaid wne c5 c6 5re crg - 5lt6 ltneii scandx vscandx neeq12i mpbir wceq zringring setsid mpan2 eqid - setsnid zlmval fveq2d 3eqtr4a ) ABEZAFGHZIJKLZGHZURFMHZANHZJKLZGHICGHVAUT - GUROUQUTPQRPQRSUAUBUQQUTRUCUDUEUFULUPITEIUSUGUHBIGTAOUIUJUPCVBGVAABCDVAUK - UMUNUO $. + ( wcel cnx csca cfv zring cop csts cvsca cmg scaid vscandxnscandx setsnid + co necomi crg wceq zringring setsid mpan2 eqid zlmval fveq2d 3eqtr4a ) AB + EZAFGHZIJKQZGHZUJFLHZAMHZJKQZGHICGHUMULGUJNULUIORPUHISEIUKTUABIGSANUBUCUH + CUNGUMABCDUMUDUEUFUG $. ${ zlmvsca.2 $e |- .x. = ( .g ` G ) $. @@ -261951,13 +262003,27 @@ According to Wikipedia ("Integer", 25-May-2019, $} ${ - znbaslem.e $e |- E = Slot K $. - znbaslem.k $e |- K e. NN $. - znbaslem.l $e |- K < ; 1 0 $. + znbaslem.e $e |- E = Slot ( E ` ndx ) $. + znbaslem.n $e |- ( E ` ndx ) =/= ( le ` ndx ) $. $( Lemma for ~ znbas . (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, - 13-Jun-2019.) (Revised by AV, 9-Sep-2021.) $) + 13-Jun-2019.) (Revised by AV, 9-Sep-2021.) (Revised by AV, + 3-Nov-2024.) $) znbaslem $p |- ( N e. NN0 -> ( E ` U ) = ( E ` Y ) ) $= + ( cn0 wcel cfv cnx cple cop csts co setsnid eqid znval2 fveq2d eqtr4id + ) DKLZBCMBNOMZEOMZPQRZCMECMUFUECBIJSUDEUGCABUFDEFGHUFTUAUBUC $. + $} + + ${ + znbaslemOLD.e $e |- E = Slot K $. + znbaslemOLD.k $e |- K e. NN $. + znbaslemOLD.l $e |- K < ; 1 0 $. + $( Obsolete version of ~ znbaslem as of 3-Nov-2024. Lemma for ~ znbas . + (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario + Carneiro, 14-Aug-2015.) (Revised by AV, 13-Jun-2019.) (Revised by + AV, 9-Sep-2021.) (New usage is discouraged.) + (Proof modification is discouraged.) $) + znbaslemOLD $p |- ( N e. NN0 -> ( E ` U ) = ( E ` Y ) ) $= ( cn0 wcel cfv cnx cple cop csts wne ndxid cc0 cdc ltneii ndxarg plendx co c1 nnrei neeq12i mpbir setsnid eqid znval2 fveq2d eqtr4id ) EMNZBCOB PQOZFQOZRSUGZCOFCOUSURCBCDJKUAPCOZURTDUHUBUCZTDVBDKUILUDVADURVBCDJKUEUF @@ -261966,21 +262032,46 @@ According to Wikipedia ("Integer", 25-May-2019, $( The base set of ` Z/nZ ` is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, - 13-Jun-2019.) $) + 13-Jun-2019.) (Revised by AV, 3-Nov-2024.) $) znbas2 $p |- ( N e. NN0 -> ( Base ` U ) = ( Base ` Y ) ) $= - ( cbs c1 df-base 1nn 1lt10 znbaslem ) ABHICDEFGJKLM $. + ( cbs baseid cnx cple cfv plendxnbasendx necomi znbaslem ) ABHCDEFGIJKLJH + LMNO $. + + $( Obsolete version of ~ znbas2 as of 3-Nov-2024. The base set of ` Z/nZ ` + is the same as the quotient ring it is based on. (Contributed by Mario + Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) + (New usage is discouraged.) (Proof modification is discouraged.) $) + znbas2OLD $p |- ( N e. NN0 -> ( Base ` U ) = ( Base ` Y ) ) $= + ( cbs c1 df-base 1nn 1lt10 znbaslemOLD ) ABHICDEFGJKLM $. $( The additive structure of ` Z/nZ ` is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by - AV, 13-Jun-2019.) $) + AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.) $) znadd $p |- ( N e. NN0 -> ( +g ` U ) = ( +g ` Y ) ) $= - ( cplusg c2 df-plusg 2nn 2lt10 znbaslem ) ABHICDEFGJKLM $. + ( cplusg plusgid cnx cple cfv plendxnplusgndx necomi znbaslem ) ABHCDEFGI + JKLJHLMNO $. + + $( Obsolete version of ~ znadd as of 3-Nov-2024. The additive structure of + ` Z/nZ ` is the same as the quotient ring it is based on. (Contributed + by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) + (New usage is discouraged.) (Proof modification is discouraged.) $) + znaddOLD $p |- ( N e. NN0 -> ( +g ` U ) = ( +g ` Y ) ) $= + ( cplusg c2 df-plusg 2nn 2lt10 znbaslemOLD ) ABHICDEFGJKLM $. $( The multiplicative structure of ` Z/nZ ` is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) - (Revised by AV, 13-Jun-2019.) $) + (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.) $) znmul $p |- ( N e. NN0 -> ( .r ` U ) = ( .r ` Y ) ) $= - ( cmulr c3 df-mulr 3nn 3lt10 znbaslem ) ABHICDEFGJKLM $. + ( cmulr mulrid cnx cple cfv plendxnmulrndx necomi znbaslem ) ABHCDEFGIJKL + JHLMNO $. + + $( Obsolete version of ~ znadd as of 3-Nov-2024. The multiplicative + structure of ` Z/nZ ` is the same as the quotient ring it is based on. + (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, + 13-Jun-2019.) (New usage is discouraged.) + (Proof modification is discouraged.) $) + znmulOLD $p |- ( N e. NN0 -> ( .r ` U ) = ( .r ` Y ) ) $= + ( cmulr c3 df-mulr 3nn 3lt10 znbaslemOLD ) ABHICDEFGJKLM $. $( The ` ZZ ` ring homomorphism of ` Z/nZ ` is inherited from the quotient ring it is based on. (Contributed by Mario Carneiro, 14-Jun-2015.) @@ -644761,13 +644852,26 @@ fixed reference functional determined by this vector (corresponding to hlhilslem.r $e |- R = ( Scalar ` U ) $. hlhilslem.k $e |- ( ph -> ( K e. HL /\ W e. H ) ) $. ${ - hlhilslem.f $e |- F = Slot N $. - hlhilslem.1 $e |- N e. NN $. - hlhilslem.2 $e |- N < 4 $. + hlhilslem.f $e |- F = Slot ( F ` ndx ) $. + hlhilslem.n $e |- ( F ` ndx ) =/= ( *r ` ndx ) $. hlhilslem.c $e |- C = ( F ` E ) $. - $( Lemma for ~ hlhilsbase2 . (Contributed by Mario Carneiro, - 28-Jun-2015.) $) + $( Lemma for ~ hlhilsbase etc. (Contributed by Mario Carneiro, + 28-Jun-2015.) (Revised by AV, 6-Nov-2024.) $) hlhilslem $p |- ( ph -> C = ( F ` R ) ) $= + ( cnx cfv eqid cstv chg cop csts co setsnid eqtri csca hlhilsca eqtr4di + fveq2d syl5eq ) ABERUASZIHUBSSZUCUDUEZFSZCFSBEFSUPQUNUMFEOPUFUGAUOCFAUO + DUHSCAUODEUNGHIJLNKUNTUOTUIMUJUKUL $. + $} + + ${ + hlhilslemOLD.f $e |- F = Slot N $. + hlhilslemOLD.1 $e |- N e. NN $. + hlhilslemOLD.2 $e |- N < 4 $. + hlhilslemOLD.c $e |- C = ( F ` E ) $. + $( Obsolete version of ~ hlhilslem as of 6-Nov-2024. Lemma for + ~ hlhilsbase . (Contributed by Mario Carneiro, 28-Jun-2015.) + (New usage is discouraged.) (Proof modification is discouraged.) $) + hlhilslemOLD $p |- ( ph -> C = ( F ` R ) ) $= ( cfv cnx cstv chg cop csts co ndxid wne c4 nnrei ltneii ndxarg neeq12i starvndx mpbir setsnid eqtri csca eqid hlhilsca eqtr4di fveq2d syl5eq ) ABEUAUBTZJHUCTTZUDUEUFZFTZCFTBEFTVGSVEVDFEFIPQUGUAFTZVDUHIUIUHIUIIQUJRU @@ -644778,26 +644882,51 @@ fixed reference functional determined by this vector (corresponding to hlhilsbase.c $e |- C = ( Base ` E ) $. $( The scalar base set of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, - 28-Jun-2015.) $) + 28-Jun-2015.) (Revised by AV, 6-Nov-2024.) $) hlhilsbase $p |- ( ph -> C = ( Base ` R ) ) $= - ( cbs c1 df-base 1nn 1lt4 hlhilslem ) ABCDEOFGPHIJKLMQRSNT $. + ( cbs baseid cnx cstv cfv starvndxnbasendx necomi hlhilslem ) ABCDEOFGH + IJKLMPQRSQOSTUANUB $. + + $( Obsolete version of ~ hlhilsbase as of 6-Nov-2024. The scalar base + set of the final constructed Hilbert space. (Contributed by NM, + 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) + (New usage is discouraged.) (Proof modification is discouraged.) $) + hlhilsbaseOLD $p |- ( ph -> C = ( Base ` R ) ) $= + ( cbs c1 df-base 1nn 1lt4 hlhilslemOLD ) ABCDEOFGPHIJKLMQRSNT $. $} ${ hlhilsplus.a $e |- .+ = ( +g ` E ) $. $( Scalar addition for the final constructed Hilbert space. (Contributed - by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) $) + by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) + (Revised by AV, 6-Nov-2024.) $) hlhilsplus $p |- ( ph -> .+ = ( +g ` R ) ) $= - ( cplusg c2 df-plusg 2nn 2lt4 hlhilslem ) ABCDEOFGPHIJKLMQRSNT $. + ( cplusg plusgid cnx cstv cfv starvndxnplusgndx necomi hlhilslem ) ABCD + EOFGHIJKLMPQRSQOSTUANUB $. + + $( Obsolete version of ~ hlhilsplus as of 6-Nov-2024. The scalar + addition for the final constructed Hilbert space. (Contributed by NM, + 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) + (New usage is discouraged.) (Proof modification is discouraged.) $) + hlhilsplusOLD $p |- ( ph -> .+ = ( +g ` R ) ) $= + ( cplusg c2 df-plusg 2nn 2lt4 hlhilslemOLD ) ABCDEOFGPHIJKLMQRSNT $. $} ${ hlhilsmul.m $e |- .x. = ( .r ` E ) $. $( Scalar multiplication for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, - 28-Jun-2015.) $) + 28-Jun-2015.) (Revised by AV, 6-Nov-2024.) $) hlhilsmul $p |- ( ph -> .x. = ( .r ` R ) ) $= - ( cmulr c3 df-mulr 3nn 3lt4 hlhilslem ) ACBDEOFGPHIJKLMQRSNT $. + ( cmulr mulrid cnx cstv cfv starvndxnmulrndx necomi hlhilslem ) ACBDEOF + GHIJKLMPQRSQOSTUANUB $. + + $( Obsolete version of ~ hlhilsmul as of 6-Nov-2024. The scalar + multiplication for the final constructed Hilbert space. (Contributed + by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) + (New usage is discouraged.) (Proof modification is discouraged.) $) + hlhilsmulOLD $p |- ( ph -> .x. = ( .r ` R ) ) $= + ( cmulr c3 df-mulr 3nn 3lt4 hlhilslemOLD ) ACBDEOFGPHIJKLMQRSNT $. $} $}