From c2fe8d462e4203e92a789765cd80bda91cf01dc7 Mon Sep 17 00:00:00 2001 From: Wolf Lammen <30736367+wlammen@users.noreply.github.com> Date: Mon, 25 Nov 2024 05:21:54 +0100 Subject: [PATCH] syl5eq -> eqtrid # 40 (#4438) --- set.mm | 92 +++++++++++++++++++++++++++++----------------------------- 1 file changed, 46 insertions(+), 46 deletions(-) diff --git a/set.mm b/set.mm index 193fb5289..ca1b8d5fa 100644 --- a/set.mm +++ b/set.mm @@ -571032,7 +571032,7 @@ curry M LIndF ( R freeLMod I ) ) ) $= breq2d bitr2d 3jcad rexri sylibr sqcl crn ctg ccnfld ctopn eqid dvmptdivc tgioo2 cres asinf sstri feqresmpt dvreasin eqtr3di sq1 3impib sylbi negex wf 0le1 dvmptc ctopon cnfldtopon toponmax mp1i cin df-ss mpbi dvexp ax-mp - cn 2nn 2m1e1 oveq2i exp1 syl5eq dvmptres3 dvmptsub df-neg mpteq2i eqtr4di + cn 2nn 2m1e1 oveq2i exp1 eqtrid dvmptres3 dvmptsub df-neg mpteq2i eqtr4di eqtri dvsqrt gt0ne0d sqr00d ex necon3d mpd 2ne0 divcan5d mulne0d divrec2d dvmptmul dvmptadd mulid2d divassd addcomd 2timesd negsubd sqsqrtd divdird negeqd eqtr4d addassd 3eqtrrd oveq1 mulassd divrecd 3eqtr3d mul12d sqge0d @@ -571258,7 +571258,7 @@ curry M LIndF ( R freeLMod I ) ) ) $= cmnf simprrr xrre syl22anc pm4.71rd bitr4d df-rab eqtr4di 3eqtr4rd ltnled ex wn biimprd imdistani wral readdcld lt2sqd breq2d mpbid 3adant3 ltletrd bitrd sqge0 addge01d 3expa ralrimiva rabeq0 sylibr eqtr3id iffalse eqtr4d - syl pm2.61dan eqtr3d syl5eq ) DHIZJDKLZCUAZHIZUBZEUUSUCZUDZUUTGUAZHIZUUSM + syl pm2.61dan eqtr3d eqtrid ) DHIZJDKLZCUAZHIZUBZEUUSUCZUDZUUTGUAZHIZUUSM NOZUVDMNOZUEOZDMNOZKLZPZPZGUFZUUSUGUHZDKLZUVIUVFUIOZUJUHZUKZUVQUSOZQULZUV CAUAZHIZBUAZHIZPZUWAMNOZUWCMNOZUEOZUVIKLZPZABUMZUVBUDZUUSUVDUWKLZGUFZUVME UWKUVBFUNUUSUOIUWLUWNRCUPZGUUSUOUWKUQURUWMUVLGUWMUUSUVDUTUWKIUUTUVEPZUVJP @@ -571311,7 +571311,7 @@ curry M LIndF ( R freeLMod I ) ) ) $= dmarea itgeq2dv rexrd rexr elioo2 absltd notbid lenltd bitr4d anim1i eqle ioossre 3syl eqtr3d subidd negeqi sylan9eqr mp2an 0xr iccid ovolsn syldan neg0 ex wne ltnled simpl1 leltned syl6bir pm2.61dne itgss negeq id itgeq1 - iooid itg0 sq0 oveq2i mul01i eqtr2i eqtr4id syl5eq crp biimp3ar elrpd cdv + iooid itg0 sq0 oveq2i mul01i eqtr2i eqtr4id eqtrid crp biimp3ar elrpd cdv 0red rpre exp4b ltled rpge0 lt2sqd posdifd crn ctg ccnfld ctopn ax-resscn rpxr rpcn rpne0 asincl 1cnd mulcld addcld eqid tgioo2 cnt iccntr dvmptntr areacirclem1 weq 3eqtr4rd ccncf 2cn sstri ssid 3pm3.2i cncfmptc mp1i cres @@ -571634,7 +571634,7 @@ curry M LIndF ( R freeLMod I ) ) ) $= cocnv $p |- ( ( Fun F /\ Fun G ) -> ( ( F o. G ) o. `' G ) = ( F |` ran G ) ) $= ( wfun ccom ccnv crn cres coass cid wceq funcocnv2 adantl coeq2d resco wrel - wa funrel coi1 syl reseq1d adantr eqtr3id eqtrd syl5eq ) ACZBCZPZABDBEZDABU + wa funrel coi1 syl reseq1d adantr eqtr3id eqtrd eqtrid ) ACZBCZPZABDBEZDABU HDZDZABFZGZABUHHUGUJAIUKGZDZULUGUIUMAUFUIUMJUEBKLMUGUNAIDZUKGZULAIUKNUEUPUL JUFUEUOAUKUEAOUOAJAQARSTUAUBUCUD $. @@ -572912,7 +572912,7 @@ curry M LIndF ( R freeLMod I ) ) ) $= cxr jca cdiv wi simpr rphalfcld oveq2 iuneq2d sseq2d rexbidv rspcv wne wf crab simprbi ad2antrl ssrab2 ssfi sylancl oveq1 ineq1d incom eqtrdi dfin5 wex weq neeq1d rabn0 bitrdi rgen cima mpbird wfn elpreima imaeq2d eleq12d - elrab id adantr syl2anc cbviunv ad4antlr iunss sylibr syl5eq sylan syl2an + elrab id adantr syl2anc cbviunv ad4antlr iunss sylibr eqtrid sylan syl2an sstrd syld eleq1 ac6sfi cdm ccnv w3a fdm feq2d ffn baibd ralbidva ralrab2 3jca simpr2 frnd ffnd simpr1 fnfi rnfi sylanbrc rpxr blssm iunin1 simplrr crn sseqtrdi 0ss sseq1 mpbiri a1i simpr3 imbi12d rspccva ad5antr cnvimass @@ -572975,7 +572975,7 @@ curry M LIndF ( R freeLMod I ) ) ) $= 3syl simprr eqid rnmpt wi simplbi ssrexv syl ss2abdv eqsstrid ovex dfiun3 unieq eqtr4di sseq2d ssabral sseq1 bitr3id anbi12d syl12anc rexlimdvaa wf rspcev wex oveq1 eqeq2d ac6sfi adantrl adantl frn wfo simplrl dffn4 sylib - wfn ffn fofi syl2anc sylanbrc simprrl adantr uniiun iuneq2 syl5eq sseqtrd + wfn ffn fofi syl2anc sylanbrc simprrl adantr uniiun iuneq2 eqtrid sseqtrd ad2antll eleq2d rexrn eliun 3bitr4g eqrdv sseqtrrd iuneq1 exlimddv impbid ralbidv bitrd ) CEUBLMFENOZDFUCLMFAJPZAPZHPZCUDLZUGZQZNZJEUERUFZSZHUHUIFB PZUJZNZGPZYBTZAESZGYGUIZOZBRSZHUHUIAJCDEFHIUKXQYFYOHUHXQYFYOXQYDYOJYEXQXR @@ -573362,7 +573362,7 @@ counterexample is the discrete extended metric (assigning distinct equivbnd2 $p |- ( ph -> ( D e. ( TotBnd ` Y ) <-> D e. ( Bnd ` Y ) ) ) $= ( ctotbnd cfv wcel cbnd totbndbnd wa simpr cxp cres cmet wss adantr sylan bnd2lem metres2 syl2anc eqeltrid crp cv co cmul cle wbr anim12dan adantlr - sselda syldan wceq oveqi ovres syl5eq adantl 3brtr4d equivbnd equivtotbnd + sselda syldan wceq oveqi ovres eqtrid adantl 3brtr4d equivbnd equivtotbnd oveq2d biimpar bndmet ex impbid2 ) AEKUAUBZUCZEKUDUBZUCZEKUEAWDWBAWDUFZBC FDEKAWDDWCUCZDWAUCZWEBCGEDKAWDUGWEDHKKUHZUIZKUJUBZRWEHJUJUBZUCZKJUKZWIWJU CAWLWDLULAIWKUCWDWMMEIJKSUNUMZHKJUOUPUQAGURUCWDOULWEBUSZKUCZCUSZKUCZUFZUF @@ -573392,7 +573392,7 @@ counterexample is the discrete extended metric (assigning distinct prdsbnd $p |- ( ph -> D e. ( Bnd ` B ) ) $= ( vm vk vw vf vg vz cmet cfv wcel cxp cc0 cv cicc co wf wrex cbnd cprds cr cmpt cds cbs cvv eqid fvexd bndmet syl prdsmet wfn wceq dffn5 oveq2d - sylib syl5eq fveq2d 3eltr4d wral cfn wex isbnd3 simprbi ralrimiva oveq2 + sylib eqtrid fveq2d 3eltr4d wral cfn wex isbnd3 simprbi ralrimiva oveq2 wa feq3d ac6sfi syl2anc crn csn cun clt csup wss frn adantl 0red adantr snssd unssd c0 wne wfo ffn dffn4 fofi snfi unfi sylancl ssun2 c0ex snid syl2an sselii ne0i mp1i wor w3a ltso fisupcl mpan syl3anc sseldd simprl @@ -573452,7 +573452,7 @@ counterexample is the discrete extended metric (assigning distinct prdstotbnd $p |- ( ph -> D e. ( TotBnd ` B ) ) $= ( vy vv vr vf vz vw vg cmet cfv wcel cbl ciun wceq cpw cfn cin wrex crp cv co wral ctotbnd cmpt cprds cds cbs cvv eqid wa totbndmet syl prdsmet - fvexd wfn dffn5 sylib oveq2d syl5eq fveq2d 3eltr4d wex adantr istotbnd3 + fvexd wfn dffn5 sylib oveq2d eqtrid fveq2d 3eltr4d wex adantr istotbnd3 simprbi r19.21bi df-rex rexv bitr4i an32s ralrimiva eleq1 iuneq1 eqeq1d wf anbi12d ac6sfi syl2anc cixp wss elfpw simplbi ralimi ad2antll ss2ixp fnfi fndmd prdsbas rgenw ax-mp eqtr4di ad2antrr sseqtrrd ixpfi sylanbrc @@ -573511,7 +573511,7 @@ counterexample is the discrete extended metric (assigning distinct prdsbnd2 $p |- ( ph -> ( C e. ( TotBnd ` A ) <-> C e. ( Bnd ` A ) ) ) $= ( va vr ctotbnd cfv wcel cbnd totbndbnd wi c0 wceq bndmet 0totbnd syl5ibr cmet a1i wne cv wex n0 wa cbl co wss cr wrex simprr wb cmpt cprds cds cbs - cvv eqid fvexd prdsmet wfn dffn5 sylib oveq2d syl5eq fveq2d 3eltr4d simpr + cvv eqid fvexd prdsmet wfn dffn5 sylib oveq2d eqtrid fveq2d 3eltr4d simpr adantr bnd2lem syl2an simprl sseldd ssbnd syl2anc mpbid cxp cres resabs1d xpss12 eqtr4di crp simpll cc0 clt wbr ne0d cxmet cxr ad2antrr metxmet syl rexrd xbln0 syl3anc elrpd cress cfn ovex 2fveq3 sqxpeqd reseq12d oveq123d @@ -573674,7 +573674,7 @@ counterexample is the discrete extended metric (assigning distinct msmet adantl sqxpeqd reseq12d 3eltr4d totbndbnd cnfldbas ressbas2 bnd2lem wi eleqtrrd syl5 cabs cmin ccom cntotbnd a1i sseq2d biimpa xpss12 syl2anc ex resabs1d adantr cnfldds ressds reseq1d eqtr4d 3bitr4d pm5.21ndd pwsval - wb prdsbnd2 syl5eq ) AUDHZCUBIZUEZJAUFUGZUHKZCXGUILZUJUGZMKZDDLZNZDUKKZIX + wb prdsbnd2 eqtrid ) AUDHZCUBIZUEZJAUFUGZUHKZCXGUILZUJUGZMKZDDLZNZDUKKZIX MDULKZIBXNIBXOIXFUAUCDXJOKZXMXKXIXHUAUMZXIKZMKZXROKZXTLZNZCXTPXJXJQXPQXTQ YBQXKQXFXGUHUNXDXEUOZXGPIZXICUPXFJAUFURZCXGPUQUSXMQXFXQCIZUEZXGMKZXGOKZYI LZNZYIRKZYBXTRKYGXGUTIZYKYLIYGJUTIAPIZYMVAXDYNXEYFAUDVBVCVDZAJPVEVFYKXGYI @@ -573882,7 +573882,7 @@ counterexample is the discrete extended metric (assigning distinct ( vu cxmet cfv wcel wa co wceq syl2anc vv vx vy cismty wss cres cima wf1o cv wf1 isismty simprbda adantrr f1of1 syl simprr f1ores biimpa wi anim12d wral imp oveq1 fveq2 oveq1d eqeq12d oveq2 oveq2d rspc2v adantlrl adantlll - ssel an32s oveqi ovres syl5eq adantl fvres ad2antrl ad2antll oveq12d wfun + ssel an32s oveqi ovres eqtrid adantl fvres ad2antrl ad2antll oveq12d wfun cxp f1ofun f1odm sseq2d biimparc funfvima2 eleqtrrdi adantrl ovresd eqtrd cdm adantlrr 3eqtr4d ralrimivva wb xmetres2 eqeltrid ad2ant2rl simplr crn mpdan imassrn eqsstri f1ofo forn 3syl sseqtrid fveq2i eleqtrdi mpbir2and @@ -574150,7 +574150,7 @@ whose corresponding balls have no finite subcover (i.e. in the set snid opelxp mpbiran2 fveq2 xpeq12d eleq2d rspcev sylan2br eliun 3adant3 sneq sylibr syl eqeltrd ssriv ssdomg mp2 cen nn0ennn nnenom entri endom cn ax-mp vex xpsnen cfn cpw inss2 ffvelrnda sselid csdm sylancr ffvelrn - ralrimiva syl2an oveq1 syl5eq oveq2 ineq2d c2 cexp adantl elpwid oveq2d + ralrimiva syl2an oveq1 eqtrid oveq2 ineq2d c2 cexp adantl elpwid oveq2d eqtrd cdiv ovex syl2anc adantr syl3anc sylib heiborlem1 sdomdom endomtr isfinite iunctb simp1d peano2nn0 iunin2 cbviunv iuneq1d iuneq2d rspccva sylbi domtr eqeq2d fveq2d df-ov eqtr4di inss1 simp2d sseldd ovmpo cxmet @@ -574210,7 +574210,7 @@ whose corresponding balls have no finite subcover (i.e. in the set heiborlem4 $p |- ( ( ph /\ A e. NN0 ) -> ( S ` A ) G A ) $= ( vk cn0 wcel cfv wbr cv wi cc0 c1 caddc co wceq fveq2 breq12d imbi2d id cmin cif cmpt cseq fveq1i cz 0z seq1 ax-mp eqtri cvv w3a relopabiv - 0nn0 brrelex1i syl iftrue eqid fvmptg sylancr syl5eq eqbrtrd wa df-br + 0nn0 brrelex1i syl iftrue eqid fvmptg sylancr eqtrid eqbrtrd wa df-br cin cop c2nd wral df-ov eqtr4di fvex vex op2ndd oveq1d oveq12d eleq1d ineq12d anbi12d rspccv syl5bi seqp1 nn0uz eleq2s oveq1i 3eqtr4g eqeq1 oveq1 ifbieq2d peano2nn0 cn wn nn0p1nn nnne0 neneqd iffalse 3syl ovex @@ -574523,7 +574523,7 @@ the next (since the empty set has a finite subcover, the rspccva expcom adantl ac6sfi adantrl w3a crn simp3l frnd mopnuni 3ad2ant1 oveq1 wss sseqtrd cmopn fvexi uniex elpw2 sylibr simp2l wfo wfn ffn dffn4 sylib sylan2 syl2anc elind eleq2d rexrn eliun 3bitr4g eqrdv simp3r uniiun - iuneq2 syl5eq syl simp2r 3eqtr2rd iuneq1 rspceeqv 3expia adantrrr exlimdv + iuneq2 eqtrid syl simp2r 3eqtr2rd iuneq1 rspceeqv 3expia adantrrr exlimdv fofi mpd rexlimdvaa syld ralrimdva pwex inex1 com eqid simpl weq iuneq2dv oveq2d nn0ennn nnenom entri axcc4 syl6 elpwi cab copab pweqd ineq1d feq3d cmpo wn biimpar adantrr cbviunv id sseqtrrid fss syl2anr ffvelrnda elpwid @@ -574948,7 +574948,7 @@ the next (since the empty set has a finite subcover, the ( vk cfn wcel ccnfld csca cfv cr cds cbs cmet cvv eqid wceq cress csn cxp co cprds cabs cmin ccom cres cmpt fconstmpt oveq2i wss ax-resscn cnfldbas cc ressbas2 ax-mp reex cnfldds ressds reseq1i fvexd id cv wa ovex prdsmet - a1i remet resssca pwsval mpan fveq2d syl5eq cmap pwsbas eqtrd 3eltr4d ) B + a1i remet resssca pwsval mpan fveq2d eqtrid cmap pwsbas eqtrd 3eltr4d ) B IJZKLMZBKNUAUDZUBUCZUEUDZOMZWDPMZQMACQMVTHWFWEWBWAUFUGUHZNNUCZUIZBNRWDRWC HBWBUJWAUEHBWBUKULWFSNUPUMNWBPMTUNNUPWBKWBSZUOUQURZWGWBOMZWHNRJZWGWLTUSNW GKWBRWJUTVAURVBWESVTKLVCVTVDWBRJZVTHVEBJVFZKNUAVGZVIWINQMJWOWIWISVJVIVHVT @@ -574963,7 +574963,7 @@ the next (since the empty set has a finite subcover, the ( F ( Rn ` I ) G ) <_ ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) ) ) $= ( vk wcel co cfv cle wbr cr cvv adantr vz vr wa crrn chash cmul cabs cmin csqrt cv ccom cxp cres cmpt crn cc0 csn cun cxr clt csup csca cress cprds - ccnfld cds wceq ovex reex eqid resssca ax-mp pwsval sylancr fveq2d syl5eq + ccnfld cds wceq ovex reex eqid resssca ax-mp pwsval sylancr fveq2d eqtrid cfn oveqd cbs fconstmpt oveq2i a1i ralrimiva simprl cmap cc wss ax-resscn cnfldbas ressbas2 pwsbas eleqtrd simprr cnfldds ressds reseq1i prdsdsval3 fvexd eqtrd wral rrndstprj1 an32s sylanl1 wb rgenw breq1 ralrnmptw sylibr @@ -575142,7 +575142,7 @@ the next (since the empty set has a finite subcover, the iccbnd $p |- ( ( A e. RR /\ B e. RR ) -> M e. ( Bnd ` J ) ) $= ( vx vy vr cr wcel wa cfv cv co cle wbr wral cmin cc cmet wrex cbnd cnmet cabs ccom cxp cres cicc iccssre eqsstrid ax-resscn sstrdi metres2 sylancr - wss eqeltrid resubcl ancoms oveqi wceq ovres adantl syl5eq anim12dan eqid + wss eqeltrid resubcl ancoms oveqi wceq ovres adantl eqtrid anim12dan eqid sselda cnmetdval syl eqtrd caddc w3a simprr eleqtrdi elicc2 adantr simp1d wb mpbid syl2anc simpll simprl simplr simp3d lesub1dd subled simp2d letrd readdcld lesub2dd lesubadd2d absdifled mpbir2and eqbrtrd ralrimivva breq2 @@ -575381,7 +575381,7 @@ the next (since the empty set has a finite subcover, the (New usage is discouraged.) $) idrval $p |- ( G e. A -> U = ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) ) $= - ( wcel cgi cfv cv co wceq wa wral crio gidval syl5eq ) ECIDEJKBLZALZEMUAN + ( wcel cgi cfv cv co wceq wa wral crio gidval eqtrid ) ECIDEJKBLZALZEMUAN UATEMUANOAFPBFQHABECFGRS $. $} @@ -575547,7 +575547,7 @@ the next (since the empty set has a finite subcover, the E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) ) ) $= ( wcel cdm wceq cxp wf cv co wral wrex w3a wi a1i wb cmndo wa cmagm cexid - crn cin mndomgmid rngopidOLD syl syl5eq fdm dmeqd dmxpid eqtr2di 3ad2ant1 + crn cin mndomgmid rngopidOLD syl eqtrid fdm dmeqd dmxpid eqtr2di 3ad2ant1 eqid ismndo1 xpid11 biimpri feq23 mpancom raleqbi1dv rexeqbi1dv 3anbi123d raleq bibi2d syl5ibrcom pm5.21ndd ) EDHZFEIZIZJZEUAHZFFKZFELZAMZBMZENZCMZ ENVPVQVSENENJZCFOZBFOZAFOZVRVQJVQVPENVQJUBZBFOZAFPZQZVMVLRVIVMFEUEZVKGVME @@ -575578,7 +575578,7 @@ the next (since the empty set has a finite subcover, the by Jeff Madsen, 16-Jun-2011.) $) exidcl $p |- ( ( G e. ( Magma i^i ExId ) /\ A e. X /\ B e. X ) -> ( A G B ) e. X ) $= - ( cmagm cexid cin wcel w3a co cdm wa crn rngopidOLD syl5eq eleq2d anbi12d + ( cmagm cexid cin wcel w3a co cdm wa crn rngopidOLD eqtrid eleq2d anbi12d pm5.32i inss1 sseli eqid clmgmOLD syl3an1 3expb sylbi 3impb wceq 3ad2ant1 eleqtrrd ) CFGHZIZADIZBDIZJABCKZCLLZDULUMUNUOUPIZULUMUNMZMULAUPIZBUPIZMZM UQULURVAULUMUSUNUTULDUPAULDCNUPECOPZQULDUPBVBQRSULUSUTUQULCFIUSUTUQUKFCFG @@ -575595,7 +575595,7 @@ the next (since the empty set has a finite subcover, the exidreslem $p |- ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> ( U e. dom dom H /\ A. x e. dom dom H ( ( U H x ) = x /\ ( x H U ) = x ) ) ) $= - ( wcel wss cdm co wceq wa wral cxp sylib syl5eq dmeqd cmagm cexid cin w3a + ( wcel wss cdm co wceq wa wral cxp sylib eqtrid dmeqd cmagm cexid cin w3a cv cres dmeqi xpss12 anidms wfo wf opidon2OLD fof fdm 3syl sseq2d syl5ibr imp ssdmres dmxpid eqtrdi eleq2d biimp3ar cmpidelt sylan2 anassrs adantrl ssel2 wb oveqi ovres eqeq1d ancoms anbi12d adantl ralrimiva 3impa 3adant3 @@ -586156,7 +586156,7 @@ This axiom is _logically_ redundant in the (logically complete) sum_ k e. ( ( M + K ) ... ( N + K ) ) B ) $= ( vw cfz co csu cv wcel cc csb caddc nfcv nfcsb1v csbeq1a cbvsumi cmin wa wi nfv nfel1 weq eleq1w anbi2d eleq1d imbi12d chvarfv csbeq1 fsumshft cvv - nfim ovexd csbied sumeq2sdv eqtrd syl5eq ) AGHOPZBDQVGDNRZBUAZNQZGFUBPHFU + nfim ovexd csbied sumeq2sdv eqtrd eqtrid ) AGHOPZBDQVGDNRZBUAZNQZGFUBPHFU BPOPZCEQZVGBVIDNNBUCDVHBUDZDVHBUEZUFAVJVKDERZFUGPZBUAZEQVLAVIVQNEFGHIJKAD RVGSZUHZBTSZUIAVHVGSZUHZVITSZUIDNWBWCDWBDUJDVITVMUKVADNULZVSWBVTWCWDVRWAA DNVGUMUNWDBVITVNUOUPLUQDVHVPBURUSAVKVQCEADVPBCUTAVOFUGVBMVCVDVEVF $. @@ -586543,7 +586543,7 @@ inference form (e.g., E. v e. V ( N ` ( s u. { v } ) ) = V ) } ) $= ( vw cfv cv wceq cbs clspn clss fveq2 wcel clsh wne csn cun wrex crab cvv wa elex eqtr4di neeq2d eqeq12d rexeqbidv anbi12d rabeqbidv df-lshyp fvexi - fveq1d rabex fvmpt syl syl5eq ) FGUAZCFUBNZHOZEUCZVFAOUDUEZDNZEPZAEUFZUIZ + fveq1d rabex fvmpt syl eqtrid ) FGUAZCFUBNZHOZEUCZVFAOUDUEZDNZEPZAEUFZUIZ HBUGZLVDFUHUAVEVMPFGUJMFVFMOZQNZUCZVHVNRNZNZVOPZAVOUFZUIZHVNSNZUGVMUHUBVN FPZWAVLHWBBWCWBFSNBVNFSTKUKWCVPVGVTVKWCVOEVFWCVOFQNEVNFQTIUKZULWCVSVJAVOE WDWCVRVIVOEWCVHVQDWCVQFRNDVNFRTJUKUSWDUMUNUOUPMAHUQVLHBBFSKURUTVAVBVC $. @@ -586784,7 +586784,7 @@ inference form (e.g., A = ran ( v e. ( V \ { .0. } ) |-> ( N ` { v } ) ) ) $= ( vw wcel cfv csn crn cbs c0g clspn fveq2 clsa cdif cv cmpt cvv wceq elex eqtr4di sneqd difeq12d fveq1d mpteq12dv rneqd df-lsatoms c0 cun rnex p0ex - fvexi unex wf wss eqid fvrn0 a1i fmpti frn ax-mp ssexi fvmpt syl syl5eq ) + fvexi unex wf wss eqid fvrn0 a1i fmpti frn ax-mp ssexi fvmpt syl eqtrid ) EFMZBEUANZADGOZUBZAUCZOZCNZUDZPZKVMEUEMVNWAUFEFUGLEALUCZQNZWBRNZOZUBZVRWB SNZNZUDZPWAUEUAWBEUFZWIVTWJAWFWHVPVSWJWCDWEVOWJWCEQNDWBEQTHUHWJWDGWJWDERN GWBERTJUHUIUJWJVRWGCWJWGESNCWBESTIUHUKULUMLAUNWACPZUOOZUPZWKWLCCESIUSUQUR @@ -587352,7 +587352,7 @@ inference form (e.g., ( t C. u /\ -. E. s e. S ( t C. s /\ s C. u ) ) ) } ) $= ( vw clcv cfv cv wcel wa wpss wrex clss copab cvv wceq elex fveq2 eqtr4di wn eleq2d anbi12d rexeqdv notbid anbi2d opabbidv df-lcv cxp xpex opabssxp - fvexi ssexi fvmpt 3syl syl5eq ) ADFMNZCOZEPZBOZEPZQZVDVFRZVDHOZRVJVFRQZHE + fvexi ssexi fvmpt 3syl eqtrid ) ADFMNZCOZEPZBOZEPZQZVDVFRZVDHOZRVJVFRQZHE SZUGZQZQZCBUAZJAFGPFUBPVCVPUCKFGUDLFVDLOZTNZPZVFVRPZQZVIVKHVRSZUGZQZQZCBU AVPUBMVQFUCZWEVOCBWFWAVHWDVNWFVSVEVTVGWFVREVDWFVRFTNEVQFTUEIUFZUHWFVREVFW GUHUIWFWCVMVIWFWBVLWFVKHVREWGUJUKULUIUMLBCHUNVPEEUOEEEFTIURZWHUPVNCBEEUQU @@ -588101,7 +588101,7 @@ Functionals and kernels of a left vector space (or module) = ( ( r .X. ( f ` x ) ) .+^ ( f ` y ) ) } ) $= ( vw wcel cvv cv co wceq wral cmap crab elex clfn cvsca cplusg csca cmulr cfv fveq2 eqtr4di fveq2d oveq12d oveqd eqidd oveq123d raleqbidv rabeqbidv - cbs eqeq12d df-lfl ovex rabex fvmpt syl5eq syl ) LMUDLUEUDZINUFZAUFZFUGZB + cbs eqeq12d df-lfl ovex rabex fvmpt eqtrid syl ) LMUDLUEUDZINUFZAUFZFUGZB UFZDUGZHUFZURZVQVRWBURZGUGZVTWBURZEUGZUHZBKUIZAKUIZNJUIZHJKUJUGZUKZUHLMUL VPILUMURWMUBUCLVQVRUCUFZUNURZUGZVTWNUOURZUGZWBURZVQWDWNUPURZUQURZUGZWFWTU OURZUGZUHZBWNVHURZUIZAXFUIZNWTVHURZUIZHXIXFUJUGZUKWMUEUMWNLUHZXJWKHXKWLXL @@ -588661,7 +588661,7 @@ Functionals and kernels of a left vector space (or module) by Mario Carneiro, 24-Jun-2014.) $) lkrfval $p |- ( W e. X -> K = ( f e. F |-> ( `' f " { .0. } ) ) ) $= ( vw wcel cvv cv cfv clfn csca c0g eqtr4di ccnv cima cmpt wceq elex fveq2 - csn clk fveq2d sneqd imaeq2d mpteq12dv df-lkr mptfvmpt syl5eq syl ) EFMEN + csn clk fveq2d sneqd imaeq2d mpteq12dv df-lkr mptfvmpt eqtrid syl ) EFMEN MZDBCBOUAZGUGZUBZUCZUDEFUEUQDEUHPVAKBLUTQUHBLOZQPZURVBRPZSPZUGZUBZUCCNEEV BEUDZBVCVGCUTVHVCEQPCVBEQUFJTVHVFUSURVHVEGVHVEASPGVHVDASVHVDERPAVBERUFHTU IITUJUKULLBUMJUNUOUP $. @@ -589447,7 +589447,7 @@ Functionals and kernels of a left vector space (or module) wb sseq1d biimpa eqssd mpbid wne clsh simprr lkrshp syl3anc simplr simprl lshpcmp eqlkr2 syl121anc sylbid pm2.61da2ne lkrscss fveq2 sseq2d biimprcd ex syl6 rexlimdv impbid pm5.32da lflvscl eleq1a pm4.71rd rexbidva r19.42v - bitr2di bitrd abbidv syl5eq ) AGIUAZDUBZIUAZUCZDFUDXNFUEZXPTZDUFXNGJEUBZU + bitr2di bitrd abbidv eqtrid ) AGIUAZDUBZIUAZUCZDFUDXNFUEZXPTZDUFXNGJEUBZU GZUHZCUIZUJZUKZEHULZDUFXPDFUMAXRYEDAXRXQYETZYEAXQXPYEAXQTZXPYEYGXPYEUPXNJ BUQUAZUGZUHZGYJYGXNYJUKZTZYEXPYLYHHUEZXNGYJYBUJZUKZYEAYMXQYKAKUNUEZYMAKUO UEZYPRKURUSZBHKYHMPYHUTZVAUSZVBYLXNYJYNYGYKVCYLBCFGHJKYHLMNPQYSAYPXQYKYRV @@ -589570,7 +589570,7 @@ Functionals and kernels of a left vector space (or module) ( vw wcel cvv cnx cbs cfv cop cplusg csca ctp cvsca csn cun wceq elex cld cv clfn cof cxp cres coppr cmulr cmpo fveq2 eqtr4di opeq2d fveq2d sqxpeqd co ofeqd reseq12d tpeq123d eqidd xpeq1d oveq123d mpoeq123dv sneqd uneq12d - df-ldual tpex snex unex fvmpt syl5eq 3syl ) ANOUHNUIUHZBUJUKULZJUMZUJUNUL + df-ldual tpex snex unex fvmpt eqtrid 3syl ) ANOUHNUIUHZBUJUKULZJUMZUJUNUL ZDUMZUJUOULZLUMZUPZUJUQULZFUMZURZUSZUTUFNOVAWMBNVBULXDTUGNWNUGVCZVDULZUMZ WPXEUOULZUNULZVEZXFXFVFZVGZUMZWRXHVHULZUMZUPZXAIHXHUKULZXFHVCZXEUKULZIVCU RZVFZXHVIULZVEZVPZVJZUMZURZUSXDUIVBXENUTZXPWTYGXCYHXGWOXMWQXOWSYHXFJWNYHX @@ -589734,7 +589734,7 @@ Functionals and kernels of a left vector space (or module) $( Scalar multiplication for the dual of a vector space. (Contributed by NM, 19-Oct-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) $) ldualsmul $p |- ( ph -> ( X .xb Y ) = ( Y .x. X ) ) $= - ( co coppr cfv cmulr eqid ldualsca fveq2d syl5eq oveqd opprmul eqtrdi ) A + ( co coppr cfv cmulr eqid ldualsca fveq2d eqtrid oveqd opprmul eqtrdi ) A JKDUAJKFUBUCZUDUCZUAKJEUAADUMJKADCUDUCUMQACULUDABCFULIHLULUEZOPRUFUGUHUIG FUMEULJKMNUNUMUEUJUK $. $} @@ -590920,7 +590920,7 @@ Functionals and kernels of a left vector space (or module) /\ x = ( ( x ./\ y ) .\/ ( x ./\ ( ._|_ ` y ) ) ) ) } ) $= ( wcel co cfv wceq cbs fveq2 vp cvv w3a copab elex ccmtN cmee coc eqtr4di cv cjn eleq2d oveqd eqidd fveq1d oveq123d eqeq2d 3anbi123d df-cmtN df-3an - opabbidv opabbii cxp fvexi xpex opabssxp ssexi eqeltri fvmpt syl5eq syl + opabbidv opabbii cxp fvexi xpex opabssxp ssexi eqeltri fvmpt eqtrid syl wa ) GCOGUBOZEAUJZDOZBUJZDOZVNVNVPHPZVNVPIQZHPZFPZRZUCZABUDZRGCUEVMEGUFQW DNUAGVNUAUJZSQZOZVPWFOZVNVNVPWEUGQZPZVNVPWEUHQZQZWIPZWEUKQZPZRZUCZABUDWDU BUFWEGRZWQWCABWRWGVOWHVQWPWBWRWFDVNWRWFGSQDWEGSTJUIZULWRWFDVPWSULWRWOWAVN @@ -591689,7 +591689,7 @@ X C ( ._|_ ` Y ) ) ) $= /\ x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) } ) $= ( vp wcel cvv cv wa wbr copab cfv cbs wrex wn wceq elex ccvr cplt eqtr4di w3a fveq2 eleq2d anbi12d breqd rexeqbidv notbid 3anbi123d opabbidv 3anass - df-covers opabbii cxp fvexi xpex opabssxp ssexi eqeltri fvmpt syl5eq syl + df-covers opabbii cxp fvexi xpex opabssxp ssexi eqeltri fvmpt eqtrid syl ) HDMHNMZFAOZEMZBOZEMZPZVJVLGQZVJCOZGQZVPVLGQZPZCEUAZUBZUHZABRZUCHDUDVIFH UESWCKLHVJLOZTSZMZVLWEMZPZVJVLWDUFSZQZVJVPWIQZVPVLWIQZPZCWEUAZUBZUHZABRWC NUEWDHUCZWPWBABWQWHVNWJVOWOWAWQWFVKWGVMWQWEEVJWQWEHTSEWDHTUIIUGZUJWQWEEVL @@ -591922,7 +591922,7 @@ X C ( ._|_ ` Y ) ) ) $= $( The set of atoms in a poset. (Contributed by NM, 18-Sep-2011.) $) pats $p |- ( K e. D -> A = { x e. B | .0. C x } ) $= ( vp wcel wbr cfv cp0 ccvr cbs fveq2 eqtr4di cv crab wceq elex catm breqd - cvv breq1d bitrd rabeqbidv df-ats fvexi rabex fvmpt syl5eq syl ) FEMFUGMZ + cvv breq1d bitrd rabeqbidv df-ats fvexi rabex fvmpt eqtrid syl ) FEMFUGMZ BGAUAZDNZACUBZUCFEUDUQBFUEOUTKLFLUAZPOZURVAQOZNZAVAROZUBUTUGUEVAFUCZVDUSA VECVFVEFROCVAFRSHTVFVDVBURDNUSVFVCDVBURVFVCFQODVAFQSJTUFVFVBGURDVFVBFPOGV AFPSITUHUIUJLAUKUSACCFRHULUMUNUOUP $. @@ -593222,7 +593222,7 @@ X C ( ._|_ ` Y ) ) ) $= cv elab nfv wi rsp eleq1a syl6 rexlimd syl5bi ssrdv glbconN sylan2 rabbii fvex df-rab eqtri nfan wb rspa cops hlop opoccl sylan syl opcon2b syl3an1 pm4.71rd 3expa eqcom bitr3di bitrd anassrs rexbida r19.42v bitr2di abbidv - pm5.32da cbvabv eqtrdi syl5eq fveq2d eqtrd ) HUAOZCBOZEGUBZPZAUIZCQZEGRZA + pm5.32da cbvabv eqtrdi eqtrid fveq2d eqtrd ) HUAOZCBOZEGUBZPZAUIZCQZEGRZA SZFTZNUIZITZWROZNBUCZDTZITZWOCITZQZEGRZASZDTZITWMWKWRBUDWSXEQWMNWRBWTWROW TCQZEGRZWMWTBOZWQXLAWTNUEWOWTQWPXKEGWOWTCUFUGUJWMXKXMEGWLEGUHZXMEUKWMEUIG OZWLXKXMULWLEGUMCBWTUNUOUPUQURNBWRDFHIJKLMUSUTWNXDXJIWNXCXIDWNXCXMXACQZEG @@ -595994,7 +595994,7 @@ projective geometry (where it is either given as an axiom or stated as 16-Jun-2012.) $) llnset $p |- ( K e. D -> N = { x e. B | E. p e. A p C x } ) $= ( vk cv cfv ccvr catm cbs fveq2 eqtr4di wcel cvv wrex crab wceq elex clln - wbr breqd rexeqbidv rabeqbidv df-llines fvexi rabex fvmpt syl5eq syl ) FE + wbr breqd rexeqbidv rabeqbidv df-llines fvexi rabex fvmpt eqtrid syl ) FE UAFUBUAZGHNZANZDUHZHBUCZACUDZUEFEUFURGFUGOVCLMFUSUTMNZPOZUHZHVDQOZUCZAVDR OZUDVCUBUGVDFUEZVHVBAVICVJVIFROCVDFRSITVJVFVAHVGBVJVGFQOBVDFQSKTVJVEDUSUT VJVEFPODVDFPSJTUIUJUKAMHULVBACCFRIUMUNUOUPUQ $. @@ -596403,7 +596403,7 @@ projective geometry (where it is either given as an axiom or stated as 16-Jun-2012.) $) lplnset $p |- ( K e. A -> P = { x e. B | E. y e. N y C x } ) $= ( vk cv cfv ccvr clln cbs fveq2 eqtr4di wcel cvv wrex crab wceq elex clpl - wbr breqd rexeqbidv rabeqbidv df-lplanes fvexi rabex fvmpt syl5eq syl ) G + wbr breqd rexeqbidv rabeqbidv df-lplanes fvexi rabex fvmpt eqtrid syl ) G CUAGUBUAZFBNZANZEUHZBHUCZADUDZUEGCUFURFGUGOVCLMGUSUTMNZPOZUHZBVDQOZUCZAVD ROZUDVCUBUGVDGUEZVHVBAVIDVJVIGRODVDGRSITVJVFVABVGHVJVGGQOHVDGQSKTVJVEEUSU TVJVEGPOEVDGPSJTUIUJUKAMBULVBADDGRIUMUNUOUPUQ $. @@ -597211,7 +597211,7 @@ projective geometry (where it is either given as an axiom or stated as NM, 1-Jul-2012.) $) lvolset $p |- ( K e. A -> V = { x e. B | E. y e. P y C x } ) $= ( vk cv cfv ccvr clpl cbs fveq2 eqtr4di wcel cvv wbr wrex crab wceq clvol - elex breqd rexeqbidv rabeqbidv df-lvols fvexi rabex fvmpt syl5eq syl ) GC + elex breqd rexeqbidv rabeqbidv df-lvols fvexi rabex fvmpt eqtrid syl ) GC UAGUBUAZHBNZANZEUCZBFUDZADUEZUFGCUHURHGUGOVCLMGUSUTMNZPOZUCZBVDQOZUDZAVDR OZUEVCUBUGVDGUFZVHVBAVIDVJVIGRODVDGRSITVJVFVABVGFVJVGGQOFVDGQSKTVJVEEUSUT VJVEGPOEVDGPSJTUIUJUKAMBULVBADDGRIUMUNUOUPUQ $. @@ -598763,7 +598763,7 @@ projective geometry (where it is either given as an axiom or stated as $( Lemma for ~ dalemdnee . (Contributed by NM, 10-Aug-2012.) $) dalem4 $p |- ( ( ph /\ D =/= T ) -> D =/= E ) $= ( wne wa co chlt wcel cbs cfv w3a wn dalemswapyz adantr clat dalemkelat - wbr wceq dalempjqeb dalemsjteb eqid latmcom syl5eq neeq1d biimpa dalem3 + wbr wceq dalempjqeb dalemsjteb eqid latmcom eqtrid neeq1d biimpa dalem3 syl3anc syl2anc dalemkehl dalemqea dalemrea hlatjcl dalemtjueb 3netr4d biid ) ADIUIZUJZHILUKZEFLUKZOUKZIJLUKZFGLUKZOUKZDKWBMULUMZCMUNUOZUMUJHB UMIBUMJBUMUPEBUMFBUMZGBUMZUPUPRPUMQPUMUJCWCNVBUQCWFNVBUQCJHLUKNVBUQUPCW @@ -598818,7 +598818,7 @@ projective geometry (where it is either given as an axiom or stated as NM, 21-Jul-2012.) $) dalem6 $p |- ( ph -> S .<_ W ) $= ( co chlt wcel cbs cfv wa w3a wbr dalemrot biid eqid dalem5 dalemqrprot - wn syl eqtr4id oveq1d syl5eq breqtrrd ) AGEFJUEZDJUEZCJUEZNLAKUFUGCKUHU + wn syl eqtr4id oveq1d eqtrid breqtrrd ) AGEFJUEZDJUEZCJUEZNLAKUFUGCKUHU IUGUJEBUGFBUGDBUGUKHBUGIBUGGBUGUKUKVEMUGHIJUEZGJUEZMUGUJCVDLULURCFDJUEL ULURCDEJUEZLULURUKCVGLULURCIGJUELULURCGHJUELULURUKCEHJUELULCFIJUELULCDG JUELULUKUKUKZGVFLULABCDEFGHIJKLMOPQRSTUBUCUMVJBCEFDHIGJKLMVFVEVHVJUNRST @@ -598829,7 +598829,7 @@ projective geometry (where it is either given as an axiom or stated as NM, 21-Jul-2012.) $) dalem7 $p |- ( ph -> T .<_ W ) $= ( co chlt wcel cbs cfv wa w3a wbr dalemrot biid eqid dalem6 dalemqrprot - wn syl eqtr4id oveq1d syl5eq breqtrrd ) AHEFJUEZDJUEZCJUEZNLAKUFUGCKUHU + wn syl eqtr4id oveq1d eqtrid breqtrrd ) AHEFJUEZDJUEZCJUEZNLAKUFUGCKUHU IUGUJEBUGFBUGDBUGUKHBUGIBUGGBUGUKUKVEMUGHIJUEZGJUEZMUGUJCVDLULURCFDJUEL ULURCDEJUEZLULURUKCVGLULURCIGJUELULURCGHJUELULURUKCEHJUELULCFIJUELULCDG JUELULUKUKUKZHVFLULABCDEFGHIJKLMOPQRSTUBUCUMVJBCEFDHIGJKLMVFVEVHVJUNRST @@ -598943,7 +598943,7 @@ projective geometry (where it is either given as an axiom or stated as dalem11 $p |- ( ph -> E .<_ X ) $= ( co chlt wcel cbs cfv wa w3a wn dalemrot biid eqid dalem10 dalemqrprot wbr eqtr4id wceq dalemkehl dalemtea dalemuea dalemsea hlatjrot syl13anc - syl oveq12d syl5eq breqtrrd ) AJEFKUIZDKUIZHIKUIZGKUIZNUIZPMALUJUKZCLUL + syl oveq12d eqtrid breqtrrd ) AJEFKUIZDKUIZHIKUIZGKUIZNUIZPMALUJUKZCLUL UMUKUNEBUKFBUKDBUKUOHBUKZIBUKZGBUKZUOUOVPOUKVROUKUNCVOMVBUPCFDKUIMVBUPC DEKUIZMVBUPUOCVQMVBUPCIGKUIMVBUPCGHKUIZMVBUPUOCEHKUIMVBCFIKUIMVBCDGKUIM VBUOUOUOZJVSMVBABCDEFGHIKLMOQRSTUAUBUEUFUQWFBCJEFDHIGKLMNOVSVPVRWFURTUA @@ -598964,7 +598964,7 @@ projective geometry (where it is either given as an axiom or stated as dalem12 $p |- ( ph -> F .<_ X ) $= ( co chlt wcel cbs cfv wa w3a wn dalemrot biid eqid dalem11 dalemqrprot wbr eqtr4id wceq dalemkehl dalemtea dalemuea dalemsea hlatjrot syl13anc - syl oveq12d syl5eq breqtrrd ) AJEFKUIZDKUIZHIKUIZGKUIZNUIZPMALUJUKZCLUL + syl oveq12d eqtrid breqtrrd ) AJEFKUIZDKUIZHIKUIZGKUIZNUIZPMALUJUKZCLUL UMUKUNEBUKFBUKDBUKUOHBUKZIBUKZGBUKZUOUOVPOUKVROUKUNCVOMVBUPCFDKUIMVBUPC DEKUIZMVBUPUOCVQMVBUPCIGKUIMVBUPCGHKUIZMVBUPUOCEHKUIMVBCFIKUIMVBCDGKUIM VBUOUOUOZJVSMVBABCDEFGHIKLMOQRSTUAUBUEUFUQWFBCEFDHIGJKLMNOVSVPVRWFURTUA @@ -599310,7 +599310,7 @@ projective geometry (where it is either given as an axiom or stated as dalem24 $p |- ( ( ph /\ Y = Z /\ ps ) -> -. G .<_ Y ) $= ( wceq w3a wbr wn co cp0 cfv cv oveq1i col wcel cbs chlt dalemkehl hlol syl 3ad2ant1 dalemccea 3ad2ant3 dalempea eqid hlatjcl syl3anc dalemddea - dalemsea dalemyeb latmmdir syl13anc syl5eq hlatjcom dalemply dalem-ccly + dalemsea dalemyeb latmmdir syl13anc eqtrid hlatjcom dalemply dalem-ccly 2atjm syl132anc eqtrd dalemsly 3adant3 dalem-ddly oveq12d wne dalempnes oveq1d cal wb hlatl atnem0 mpbid 3eqtrd dalem23 atnle mpbird ) AQRUKZBU LZKQNUMUNZKQOUOZMUPUQZUKZXCXESURZELUOZQOUOZTURZHLUOZQOUOZOUOZEHOUOZXFXC @@ -599899,7 +599899,7 @@ projective geometry (where it is either given as an axiom or stated as ( wceq w3a cv co chlt wcel cbs cfv wa wbr wn dalemswapyz 3ad2ant1 simp2 wne eqcomd dalemswapyzps biid eqid dalem55 syl3anc dalemkelat dalemkehl dalemccea 3ad2ant3 dalempea hlatjcl dalemddea dalemsea latmcom dalemqea - clat syl5eq dalemtea oveq12d oveq1d dalemrea dalemuea 3eqtr4d ) ATUAUQZ + clat eqtrid dalemtea oveq12d oveq1d dalemrea dalemuea 3eqtr4d ) ATUAUQZ BURZUCUSZIOUTZUBUSZFOUTZRUTZWRJOUTZWTGOUTZRUTZOUTZIJOUTZRUTZXFXFWRKOUTZ WTHOUTZRUTZOUTZUARUTZRUTZLMOUTZXGRUTXODRUTWQPVAVBZEPVCVDZVBVEICVBZJCVBZ KCVBZURFCVBZGCVBZHCVBZURURUASVBTSVBVEEXGQVFVGEJKOUTQVFVGEKIOUTQVFVGUREF @@ -600204,7 +600204,7 @@ Cambridge University Press (1988). Unlike them, we do not assume that ( cv wceq wrex cab cfv catm vk wcel cvv wne wbr crab elex clines cjn cple co wa fveq2 eqtr4di breqd breq2d rabeqbidv eqeq2d anbi2d rexeqbidv abbidv oveqd bitrd df-lines fvexi csn df-sn snex eqeltrri simpr ss2abi ab2rexex2 - ssexi fvmpt syl5eq syl ) DBUBDUCUBZFIOZHOZUDZGOZJOZVRVSCUKZEUEZJAUFZPZULZ + ssexi fvmpt eqtrid syl ) DBUBDUCUBZFIOZHOZUDZGOZJOZVRVSCUKZEUEZJAUFZPZULZ HAQZIAQZGRZPDBUGVQFDUHSWJNUADVTWAWBVRVSUAOZUISZUKZWKUJSZUEZJWKTSZUFZPZULZ HWPQZIWPQZGRWJUCUHWKDPZXAWIGXBWTWHIWPAXBWPDTSAWKDTUMMUNZXBWSWGHWPAXCXBWRW FVTXBWQWEWAXBWOWDJWPAXCXBWOWBWMEUEWDXBWNEWBWMXBWNDUJSEWKDUJUMKUNUOXBWMWCW