From bf1fda49dde9b9f6ee0f4a8448911e18699eb94a Mon Sep 17 00:00:00 2001 From: avekens Date: Fri, 5 Jan 2024 09:07:57 +0100 Subject: [PATCH] Miscellaneous Enhancement of comment for df-rn (Definition of `ran`), see also discussion in PR #3741 Conventions: * Revision of section "Distinctness or freeness": order of elements in a $d-condition (see also discussion in PR #3573) Mathboxes: * ~mptima moved from GS's mathbox to main * ~fproj and ~fimaproj moved from TA's mathbox to main * ~offval0 removed from AV's mathbox (duplicate of ~offval3) Usage of ~fpar and ~fsplit, see also discussion in PR #3735 * Example ~ex-fpar for ~fpar added * combination ~fsplitfpar of ~ fsplit and ~ fpar added * connection to function operation map ` oF ` added (~offsplitfpar) --- changes-set.txt | 3 + set.mm | 268 +++++++++++++++++++++++++++++++----------------- 2 files changed, 178 insertions(+), 93 deletions(-) diff --git a/changes-set.txt b/changes-set.txt index 9705bf4901..d0f61c613e 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -83,6 +83,9 @@ make a github issue.) DONE: Date Old New Notes + 4-Jan-24 fimaproj [same] moved from TA's mathbox to main set.mm + 4-Jan-24 fproj [same] moved from TA's mathbox to main set.mm + 4-Jan-24 mptima [same] moved from GS's mathbox to main set.mm 29-Dec-23 uzidd [same] moved from GS's mathbox to main set.mm 28-Dec-23 eqri [same] moved from TA's mathbox to main set.mm 28-Dec-23 domep dmep moved from SF's mathbox to main set.mm diff --git a/set.mm b/set.mm index ec97caf55e..b8794a313f 100644 --- a/set.mm +++ b/set.mm @@ -50978,8 +50978,12 @@ We have not yet defined relations ( ~ df-rel ), but here we introduce a few ` F = { <. 2 , 6 >. , <. 3 , 9 >. } -> ran F = { 6 , 9 } ` ( ~ ex-rn ). Contrast with domain (defined in ~ df-dm ). For alternate definitions, see ~ dfrn2 , ~ dfrn3 , and ~ dfrn4 . The notation " ` ran ` " is used - by Enderton; other authors sometimes use script R or script W. - (Contributed by NM, 1-Aug-1994.) $) + by Enderton; other authors sometimes use script R or script W. The range + of a function is often also called "the image of the function" (see + definition in [Lang] p. ix), which can be justified by ~ imadmrn . Not + to be confused with "codomain" (see ~ df-f ), which may be a + superset/superclass of the range (see ~ frn ). (Contributed by NM, + 1-Aug-1994.) $) df-rn $a |- ran A = dom `' A $. $( Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] @@ -54243,6 +54247,15 @@ the restriction (of the relation) to the singleton containing this wa ) CEZBFZRDEGAFZQCHZDITCHZDIABJAKUAUBDSTCLMCDABNCDAOP $. $} + ${ + $d A x $. $d C x $. + $( Image of a function in maps-to notation. (Contributed by Glauco + Siliprandi, 23-Oct-2021.) $) + mptima $p |- ( ( x e. A |-> B ) " C ) = ran ( x e. ( A i^i C ) |-> B ) $= + ( cmpt cima cres crn cin df-ima resmpt3 rneqi eqtri ) ABCEZDFNDGZHABDICEZ + HNDJOPABDCKLM $. + $} + ${ $d x y A $. $( Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38. @@ -74230,8 +74243,9 @@ of related elements (Contributed by Alexander van der Vekens, $( Merge two functions in parallel. Use as the second argument of a composition with a binary operation to build compound functions such as ` ( x e. ( 0 [,) +oo ) , y e. RR |-> ` - ` ( ( sqrt `` x ) + ( sin `` y ) ) ) ` . (Contributed by NM, - 17-Sep-2007.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) $) + ` ( ( sqrt `` x ) + ( sin `` y ) ) ) ` , see also ~ ex-fpar . + (Contributed by NM, 17-Sep-2007.) (Proof shortened by Mario Carneiro, + 28-Apr-2015.) $) fpar $p |- ( ( F Fn A /\ G Fn B ) -> H = ( x e. A , y e. B |-> <. ( F ` x ) , ( G ` y ) >. ) ) $= ( cvv cxp ccom cin csn ciun cop inxp inv1 xpeq12i xpsn 3eqtri wfn wa c1st @@ -74286,6 +74300,61 @@ of related elements (Contributed by Alexander van der Vekens, OWECAWMWNWDVSWMWLVRWLVRWMVMZXIVGVHVITTTVJWAVKWAWCLVTVLABWAVNVOABWDVPVQ $. $} + ${ + $d A a p $. $d A a x y $. $d F a x y $. $d G a x y $. $d H a $. + $d S a $. + fsplitfpar.h $e |- H = ( ( `' ( 1st |` ( _V X. _V ) ) + o. ( F o. ( 1st |` ( _V X. _V ) ) ) ) + i^i ( `' ( 2nd |` ( _V X. _V ) ) + o. ( G o. ( 2nd |` ( _V X. _V ) ) ) ) ) $. + fsplitfpar.s $e |- S = ( `' ( 1st |` _I ) |` A ) $. + $( Merge two functions with a common argument in parallel. Combination of + ~ fsplit and ~ fpar . (Contributed by AV, 3-Jan-2024.) $) + fsplitfpar $p |- ( ( F Fn A /\ G Fn A ) + -> ( H o. S ) = ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) ) $= + ( va vy wfn wa cfv cop wceq wral wcel cvv a1i adantl vp ccom cv cmpt cres + c1st cid ccnv fsplit reseq1i eqtri fveq1i fvres eqidd weq id opeq12d elex + opex fvmptd eqtrd fveq2d co df-ov cmpo fpar adantr fveq2 simpr ovmpod wss + syl5eqr eqid fnmpt mprg ssv fnssres mp2an mpbir fvco2 sylan fvmpt 3eqtr4d + fneq1i ralrimiva wb cxp crn ralrimivva fnmpo fneq1d mpbird sylancl sylibr + syl cin wrex rneqi cima mptima df-ima rnmpt 3eqtr3i elinel2 simpl opelxpd + cab wi eleq1 ex rexlimiv abssi eqsstrid fnco syl3anc eqfnfv syl2anc ) DBK + EBKLZFCUBZABAUCZDMZXTEMZNZUDZOZIUCZXSMZYFYDMZOZIBPZXRYIIBXRYFBQZLZYFCMZFM + ZYFDMZYFEMZNZYGYHYLYNYFYFNZFMZYQYLYMYRFYLYMYFARXTXTNZUDZBUEZMZYRYMUUCOYLY + FCUUBCUFUGUEUHZBUEZUUBHUUDUUABAUIUJUKULSYKUUCYROXRYKUUCYFUUAMYRYFBUUAUMYK + AYFYTYRRUUARYKUUAUNAIUOZYTYROYKUUFXTYFXTYFUUFUPZUUGUQTYFBURYRRQZYKYFYFUSZ + SUTVATVAVBYLYSYFYFFVCYQYFYFFVDYLAJYFYFBBYAJUCZEMZNZYQFRXRFAJBBUULVEZOYKAJ + BBDEFGVFZVGUUFJIUOZLZUULYQOYLUUPYAYOUUKYPUUFYAYOOUUOXTYFDVHZVGUUOUUKYPOUU + FUUJYFEVHTUQTXRYKVIZUURYQRQYLYOYPUSZSVJVLVAXRCBKZYKYGYNOUUTXRUUTIRYRUDZBU + EZBKZUVARKZBRVKZUVCUUHUVDIRIRYRUVARUVAVMVNZUUHYFRQZUUISVOBVPZRBUVAVQZVRBC + UVBCUUEUVBHUUDUVABIUIUJUKZWDZVSSBFCYFVTWAYKYHYQOXRAYFYCYQBYDUUFYAYOYBYPUU + QXTYFEVHUQYDVMZUUSWBTWCWEXRXSBKZYDBKZYEYJWFXRFBBWGZKZUUTCWHZUVOVKUVMXRUVP + UUMUVOKZXRUULRQZJBPABPUVRXRUVSAJBBUVSXRXTBQZUUJBQLLYAUUKUSSWIAJBBUULUUMRU + UMVMWJWOXRUVOFUUMUUNWKWLXRUVCUUTXRUVDUVEUVCXRUUHIRPUVDXRUUHIRUUHXRUVGLUUI + SWEUVFWOUVHUVIWMUVKWNXRUVQUAUCZYROZIRBWPZWQZUAXGZUVOUVQUVBWHZUWECUVBUVJWR + UVABWSIUWCYRUDZWHUWFUWEIRYRBWTUVABXAIUAUWCYRUWGUWGVMXBXCUKUWEUVOVKXRUWDUA + UVOUWBUWAUVOQZIUWCYFUWCQYKUWBUWHXHYFRBXDYKUWBUWHYKUWBLZUWHYRUVOQZUWIYFYFB + BYKUWBXEZUWKXFUWBUWHUWJWFYKUWAYRUVOXITWLXJWOXKXLSXMUVOBFCXNXOXRYCRQZABPUV + NXRUWLABUWLXRUVTLYAYBUSSWEABYCYDRUVLVNWOIBXSYDXPXQWL $. + + $d C a $. $d O a $. $d V a $. $d W a $. + $( Express the function operation map ` oF ` by the functions defined in + ~ fsplit and ~ fpar . (Contributed by AV, 4-Jan-2024.) $) + offsplitfpar $p |- ( ( ( F Fn A /\ G Fn A ) /\ ( F e. V /\ G e. W ) + /\ ( O Fn C /\ ( ran F X. ran G ) C_ C ) ) + -> ( O o. ( H o. S ) ) = ( F oF O G ) ) $= + ( va wfn wa wcel crn ccom cfv cmpt co cxp wss w3a cop cof wceq fsplitfpar + cv coeq2d 3ad2ant1 wf dffn3 biimpi adantr 3ad2ant3 simpl3r fnfvelrn sylan + simp1l simp1r opelxpd sseldd cofmpt eqcomi mpteq2i syl6eq cdm cin offval3 + df-ov fndm ineqan12d inidm mpteq1d sylan9eqr eqcomd 3adant3 3eqtrd ) DAMZ + EAMZNZDHOEIONZGBMZDPZEPZUAZBUBZNZUCZGFCQZQZGLALUHZDRZWLERZUDZSZQZLAWMWNGT + ZSZDEGUETZWAWBWKWQUFWHWAWJWPGLACDEFJKUGUIUJWIWQLAWOGRZSWSWILAWOBGPZGWHWAB + XBGUKZWBWCXCWGWCXCBGULUMUNUOWIWLAOZNZWFBWOWCWGWAWBXDUPXEWMWNWDWEWIVSXDWMW + DOVSVTWBWHUSAWLDUQURWIVTXDWNWEOVSVTWBWHUTAWLEUQURVAVBVCLAXAWRWRXAWMWNGVJV + DVEVFWAWBWSWTUFWHWAWBNWTWSWBWAWTLDVGZEVGZVHZWRSWSLGDEHIVIWALXHAWRWAXHAAVH + AVSVTXFAXGAADVKAEVKVLAVMVFVNVOVPVQVR $. + $} + $( The ` 2nd ` (second component of an ordered pair) function restricted to a function ` F ` is a function from ` F ` into the codomain of ` F ` . (Contributed by Alexander van der Vekens, 4-Feb-2018.) $) @@ -74654,6 +74723,60 @@ of related elements (Contributed by Alexander van der Vekens, EIXEWE $. $} + ${ + $d A a b x y z $. $d B a b x y z $. $d F a b c x y z $. + $d G a b c x y z $. $d X a b c z $. $d Y a b c z $. + fvproj.h $e |- H = ( x e. A , y e. B |-> <. ( F ` x ) , ( G ` y ) >. ) $. + ${ + fvproj.x $e |- ( ph -> X e. A ) $. + fvproj.y $e |- ( ph -> Y e. B ) $. + $( Value of a function on pairs, given two projections ` F ` and ` G ` . + (Contributed by Thierry Arnoux, 30-Dec-2019.) $) + fvproj $p |- ( ph -> ( H ` <. X , Y >. ) = <. ( F ` X ) , ( G ` Y ) >. ) + $= + ( va vb cop cfv wceq cv fveq2 co df-ov wcel opeq1d opeq2d cbvmpov eqtri + cmpo opex ovmpo syl2anc syl5eqr ) AIJPHQIJHUAZIFQZJGQZPZIJHUBAIDUCJEUCU + MUPRLMNOIJDENSZFQZOSZGQZPZUPHUNUTPUQIRURUNUTUQIFTUDUSJRUTUOUNUSJGTUEHBC + DEBSZFQZCSZGQZPZUHNODEVAUHKBCNODEVFVAURVEPVBUQRVCURVEVBUQFTUDVDUSRVEUTU + RVDUSGTUEUFUGUNUOUIUJUKUL $. + $} + + ${ + $d H a b c x y z $. $d ph a b c z $. + fimaproj.f $e |- ( ph -> F Fn A ) $. + fimaproj.g $e |- ( ph -> G Fn B ) $. + fimaproj.x $e |- ( ph -> X C_ A ) $. + fimaproj.y $e |- ( ph -> Y C_ B ) $. + $( Image of a cartesian product for a function on pairs, given two + projections ` F ` and ` G ` . (Contributed by Thierry Arnoux, + 30-Dec-2019.) $) + fimaproj $p |- ( ph -> ( H " ( X X. Y ) ) = ( ( F " X ) X. ( G " Y ) ) ) + $= + ( vz wcel cfv wceq wa vc va vb cxp cima wrex wfn wss c1st c2nd cop opex + cv wb cmpo vex op1std fveq2d op2ndd opeq12d mpompt eqtr4i fnmpti xpss12 + cmpt syl2anc sylancr simp-4r simplr opelxpi simpllr simpr sseldd fvproj + fvelimab ad5antr 1st2nd2 ad5antlr 3eqtr4d fveqeq2 rspcev wfun ad3antrrr + fnfun syl xp2nd ad3antlr fvelima r19.29a adantr xp1st adantl cvv fvmpt2 + ad2antrr sylancl fnfvima syl3anc eqeltrd eqeltrrd r19.29an bitr4d eqrdv + impbida ) AUAHIJUDZUEZFIUEZGJUEZUDZAUAUMZXFQZPUMZHRZXJSZPXEUFZXJXIQZAHD + EUDZUGXEXQUHZXKXOUNPXQXLUIRZFRZXLUJRZGRZUKZHXTYBULZHBCDEBUMZFRZCUMZGRZU + KZUOPXQYCVEKBCPDEYCYIXLYEYGUKSZXTYFYBYHYJXSYEFYEYGXLBUPZCUPZUQURYJYAYGG + YEYGXLYKYLUSURUTVAVBZVCAIDUHZJEUHZXRNOIDJEVDVFZPXQXEXJHVOVGAXPXOAXPTZUB + UMZFRZXJUIRZSZXOUBIYQYRIQZTZUUATZUCUMZGRZXJUJRZSZXOUCJUUDUUEJQZTZUUHTZY + RUUEUKZXEQZUULHRZXJSZXOUUKUUBUUIUUMYQUUBUUAUUIUUHVHZUUDUUIUUHVIZYRUUEIJ + VJVFUUKYSUUFUKYTUUGUKZUUNXJUUKYSYTUUFUUGUUCUUAUUIUUHVKUUJUUHVLUTUUKBCDE + FGHYRUUEKUUKIDYRAYNXPUUBUUAUUIUUHNVPUUPVMUUKJEUUEAYOXPUUBUUAUUIUUHOVPUU + QVMVNXPXJUURSAUUBUUAUUIUUHXJXGXHVQVRVSXNUUOPUULXEXLUULXJHVTWAVFUUDGWBZU + UGXHQZUUHUCJUFUUDGEUGZUUSAUVAXPUUBUUAMWCEGWDWEXPUUTAUUBUUAXJXGXHWFWGUCU + UGJGWHVFWIYQFWBZYTXGQZUUAUBIUFYQFDUGZUVBAUVDXPLWJDFWDWEXPUVCAXJXGXHWKWL + UBYTIFWHVFWIAXNXPPXEAXLXEQZTZXNTZXMXJXIUVFXNVLUVGXMYCXIUVGXLXQQYCWMQXMY + CSUVGXEXQXLAXRUVEXNYPWOAUVEXNVIZVMYDPXQYCWMHYMWNWPUVGXTXGQZYBXHQZYCXIQU + VGUVDYNXSIQZUVIAUVDUVEXNLWOAYNUVEXNNWOUVGUVEUVKUVHXLIJWKWEDIFXSWQWRUVGU + VAYOYAJQZUVJAUVAUVEXNMWOAYOUVEXNOWOUVGUVEUVLUVHXLIJWFWEEJGYAWQWRXTYBXGX + HVJVFWSWTXAXDXBXC $. + $} + $} + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= @@ -422153,24 +422276,30 @@ varying definitions (some start from 0, others start from 1), but details). Similarly, ` F/_ x A ` is read ` x ` is not free in (class) ` A ` , see ~ df-nfc . -
  • "$d x y $." should be read "Assume x and y are distinct +
  • "$d ` x y ` $." should be read "Assume ` x ` and ` y ` are distinct variables."
    • -
  • "$d x ` ph ` $." should be read "Assume x does not occur in phi $." - Sometimes a theorem is proved using - ` F/ x ph ` ( ~ df-nf ) in place of - "$d ` x ph ` $." when a more general result is desired; +
  • "$d ` ph x ` $." should be read "Assume ` x ` does not occur in + ` phi `." Sometimes a theorem is proved using ` F/ x ph ` ( ~ df-nf ) + in place of "$d ` ph x ` $." when a more general result is desired; ~ ax-5 can be used to derive the $d version. For an example of how to get from the $d version back to the $e version, see the proof of ~ euf from ~ eu6 .
    • -
  • "$d x A $." should be read "Assume x is not a variable occurring in - class A."
    • +
  • "$d ` A x ` $." should be read "Assume ` x ` is not a variable + occurring in class ` A `."
    • + +
  • "$d ` A x ` $. $d ` ps x ` $. + $e |- ` ( x = A -> ( ph <-> ps ) ) ` $." is an idiom often used instead + of explicit substitution, meaning "Assume ` psi ` results from the + proper substitution of ` A ` for ` x ` in ` phi `."
    • -
  • "$d x A $. $d x ps $. $e |- ` ( x = A -> ( ph <-> ps ) ) ` $." - is an idiom - often used instead of explicit substitution, meaning "Assume psi results - from the proper substitution of A for x in phi."
    • +
  • Class and wff variables should appear at the beginning of distinct + variable conditions, and setvars should be in alphabetical order. + E.g., "$d ` Z x y ` $.", "$d ` ps a x ` $.". This convention should + be applied for new theorems (formerly, the class and wff variables + mostly appear at the end) and will be assured by a formatter in the + future.
  • " ` |- ( -. A. x x = y -> ... ` " occurs early in some cases, and should be read "If x and y are distinct @@ -424628,6 +424757,35 @@ Norman Megill (2007) section 1.1.3. Megill then states, "A number of WO $. $} + ${ + $d x y A $. $d x y B $. $d x y F $. $d x y G $. + ex-fpar.h $e |- H = ( ( `' ( 1st |` ( _V X. _V ) ) + o. ( F o. ( 1st |` ( _V X. _V ) ) ) ) + i^i ( `' ( 2nd |` ( _V X. _V ) ) + o. ( G o. ( 2nd |` ( _V X. _V ) ) ) ) ) $. + ex-fpar.a $e |- A = ( 0 [,) +oo ) $. + ex-fpar.b $e |- B = RR $. + ex-fpar.f $e |- F = ( sqrt |` A ) $. + ex-fpar.g $e |- G = ( sin |` B ) $. + $( Formalized example provided in the comment for ~ fpar . (Contributed by + AV, 3-Jan-2024.) $) + ex-fpar $p |- ( ( X e. A /\ Y e. B ) + -> ( X ( + o. H ) Y ) = ( ( sqrt ` X ) + ( sin ` Y ) ) ) $= + ( caddc cfv csqrt csin wfn wceq cc cr vx vy wcel wa ccom co cop df-ov cxp + cv cmpo cres cc0 cpnf cico wss sqrtf ffn ax-mp rge0ssre ax-resscn fnssres + wf sstri reseq2i fneq1i sylibr mp2an wb id fneq12d mpbir sinf fpar fnmpoi + a1i opex opelxpi fvco2 sylancr simpl simpr fvproj fveq2d fveq1i oveqan12d + fvres syl5eq syl5eqr 3eqtrd ) FAUCZGBUCZUDZFGMEUEZUFFGUGZWNNZFONZGPNZMUFZ + FGWNUHWMWPWOENZMNZFCNZGDNZUGZMNZWSWMEABUIZQWOXFUCWPXARUAUBABUAUJCNZUBUJDN + ZUGZECAQZDBQZEUAUBABXIUKRXJOAULZUMUNUOUFZQZOSQZXMSUPZXNSSOVCXOUQSSOURUSXM + TSUTVAVDXOXPUDOXMULZXMQXNSXMOVBXMXLXQAXMOIVEVFVGVHCXLRZXJXNVIKXRAXMCXLXRV + JAXMRXRIVPVKUSVLXKPBULZTQZPSQZTSUPZXTSSPVCYAVMSSPURUSVAYAYBUDPTULZTQXTSTP + VBTXSYCBTPJVEVFVGVHDXSRZXKXTVILYDBTDXSYDVJBTRYDJVPVKUSVLUAUBABCDEHVNVHZXG + XHVQVOFGABVRXFMEWOVSVTWMWTXDMWMUAUBABCDEFGYEWKWLWAWKWLWBWCWDWMXEXBXCMUFWS + XBXCMUHWKWLXBWQXCWRMWKXBFXLNWQFCXLKWEFAOWGWHWLXCGXSNWRGDXSLWEGBPWGWHWFWIW + JWH $. + $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# @@ -472569,60 +472727,6 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- $) - ${ - $d A a b x y z $. $d B a b x y z $. $d F a b c x y z $. - $d G a b c x y z $. $d X a b c z $. $d Y a b c z $. - fvproj.h $e |- H = ( x e. A , y e. B |-> <. ( F ` x ) , ( G ` y ) >. ) $. - ${ - fvproj.x $e |- ( ph -> X e. A ) $. - fvproj.y $e |- ( ph -> Y e. B ) $. - $( Value of a function on pairs, given two projections ` F ` and ` G ` . - (Contributed by Thierry Arnoux, 30-Dec-2019.) $) - fvproj $p |- ( ph -> ( H ` <. X , Y >. ) = <. ( F ` X ) , ( G ` Y ) >. ) - $= - ( va vb cop cfv wceq cv fveq2 co df-ov wcel opeq1d opeq2d cbvmpov eqtri - cmpo opex ovmpo syl2anc syl5eqr ) AIJPHQIJHUAZIFQZJGQZPZIJHUBAIDUCJEUCU - MUPRLMNOIJDENSZFQZOSZGQZPZUPHUNUTPUQIRURUNUTUQIFTUDUSJRUTUOUNUSJGTUEHBC - DEBSZFQZCSZGQZPZUHNODEVAUHKBCNODEVFVAURVEPVBUQRVCURVEVBUQFTUDVDUSRVEUTU - RVDUSGTUEUFUGUNUOUIUJUKUL $. - $} - - ${ - $d H a b c x y z $. $d ph a b c z $. - fimaproj.f $e |- ( ph -> F Fn A ) $. - fimaproj.g $e |- ( ph -> G Fn B ) $. - fimaproj.x $e |- ( ph -> X C_ A ) $. - fimaproj.y $e |- ( ph -> Y C_ B ) $. - $( Image of a cartesian product for a function on pairs, given two - projections ` F ` and ` G ` . (Contributed by Thierry Arnoux, - 30-Dec-2019.) $) - fimaproj $p |- ( ph -> ( H " ( X X. Y ) ) = ( ( F " X ) X. ( G " Y ) ) ) - $= - ( vz wcel cfv wceq wa vc va vb cxp cima wrex wfn wss c1st c2nd cop opex - cv wb cmpo vex op1std fveq2d op2ndd opeq12d mpompt eqtr4i fnmpti xpss12 - cmpt syl2anc sylancr simp-4r simplr opelxpi simpllr simpr sseldd fvproj - fvelimab ad5antr 1st2nd2 ad5antlr 3eqtr4d fveqeq2 rspcev wfun ad3antrrr - fnfun syl xp2nd ad3antlr fvelima r19.29a adantr xp1st adantl cvv fvmpt2 - ad2antrr sylancl fnfvima syl3anc eqeltrd eqeltrrd r19.29an bitr4d eqrdv - impbida ) AUAHIJUDZUEZFIUEZGJUEZUDZAUAUMZXFQZPUMZHRZXJSZPXEUFZXJXIQZAHD - EUDZUGXEXQUHZXKXOUNPXQXLUIRZFRZXLUJRZGRZUKZHXTYBULZHBCDEBUMZFRZCUMZGRZU - KZUOPXQYCVEKBCPDEYCYIXLYEYGUKSZXTYFYBYHYJXSYEFYEYGXLBUPZCUPZUQURYJYAYGG - YEYGXLYKYLUSURUTVAVBZVCAIDUHZJEUHZXRNOIDJEVDVFZPXQXEXJHVOVGAXPXOAXPTZUB - UMZFRZXJUIRZSZXOUBIYQYRIQZTZUUATZUCUMZGRZXJUJRZSZXOUCJUUDUUEJQZTZUUHTZY - RUUEUKZXEQZUULHRZXJSZXOUUKUUBUUIUUMYQUUBUUAUUIUUHVHZUUDUUIUUHVIZYRUUEIJ - VJVFUUKYSUUFUKYTUUGUKZUUNXJUUKYSYTUUFUUGUUCUUAUUIUUHVKUUJUUHVLUTUUKBCDE - FGHYRUUEKUUKIDYRAYNXPUUBUUAUUIUUHNVPUUPVMUUKJEUUEAYOXPUUBUUAUUIUUHOVPUU - QVMVNXPXJUURSAUUBUUAUUIUUHXJXGXHVQVRVSXNUUOPUULXEXLUULXJHVTWAVFUUDGWBZU - UGXHQZUUHUCJUFUUDGEUGZUUSAUVAXPUUBUUAMWCEGWDWEXPUUTAUUBUUAXJXGXHWFWGUCU - UGJGWHVFWIYQFWBZYTXGQZUUAUBIUFYQFDUGZUVBAUVDXPLWJDFWDWEXPUVCAXJXGXHWKWL - UBYTIFWHVFWIAXNXPPXEAXLXEQZTZXNTZXMXJXIUVFXNVLUVGXMYCXIUVGXLXQQYCWMQXMY - CSUVGXEXQXLAXRUVEXNYPWOAUVEXNVIZVMYDPXQYCWMHYMWNWPUVGXTXGQZYBXHQZYCXIQU - VGUVDYNXSIQZUVIAUVDUVEXNLWOAYNUVEXNNWOUVGUVEUVKUVHXLIJWKWEDIFXSWQWRUVGU - VAYOYAJQZUVJAUVAUVEXNMWOAYOUVEXNOWOUVGUVEUVLUVHXLIJWFWEEJGYAWQWRXTYBXGX - HVJVFWSWTXAXDXBXC $. - $} - $} - ${ $d A a b c x y z $. $d F a b x y $. $d G b x y $. $d H a b c x y z $. $d J x y z $. $d K x y z $. $d L a b c x y z $. $d M a b c x y z $. @@ -667327,14 +667431,6 @@ not even needed (it can be any class). (Contributed by Glauco (Contributed by Glauco Siliprandi, 23-Oct-2021.) $) dmresss $p |- dom ( A |` B ) C_ dom A $= ( cres cdm cin dmres inss2 eqsstri ) ABCDBADZEIABFBIGH $. - ${ - $d A x $. $d C x $. - $( Image of a function in maps-to notation. (Contributed by Glauco - Siliprandi, 23-Oct-2021.) $) - mptima $p |- ( ( x e. A |-> B ) " C ) = ran ( x e. ( A i^i C ) |-> B ) $= - ( cmpt cima cres crn cin df-ima resmpt3 rneqi eqtri ) ABCEZDFNDGZHABDICEZ - HNDJOPABDCKLM $. - $} ${ dmmptssf.1 $e |- F/_ x A $. @@ -744833,20 +744929,6 @@ Differences between (left) modules and (left) vector spaces -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- $) - ${ - $d F f g x $. $d G f g x $. $d R f g x $. $d V f g $. $d W f g $. - $( Value of an operation applied to two functions. (Contributed by AV, - 15-May-2020.) $) - offval0 $p |- ( ( F e. V /\ G e. W ) -> ( F oF R G ) - = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) ) $= - ( vf vg wcel wa cvv cv cdm cin cfv co cmpt wceq dmeq fveq1 cof cmpo df-of - ineqan12d oveqan12d mpteq12dv adantl elex adantr dmexg inex1g mptexg 3syl - a1i ovmpod ) CEIZDFIZJZGHCDKKAGLZMZHLZMZNZALZUSOZVDVAOZBPZQZACMZDMZNZVDCO - ZVDDOZBPZQZBUAZKVPGHKKVHUBRURABGHUCUNUSCRZVADRZJZVHVORURVSAVCVGVKVNVQVRUT - VIVBVJUSCSVADSUDVQVRVEVLVFVMBVDUSCTVDVADTUEUFUGUPCKIUQCEUHUIUQDKIUPDFUHUG - URVIKIZVKKIVOKIUPVTUQCEUJUIVIVJKUKAVKVNKULUMUO $. - $} - ${ $d F x $. $d V x $. $d W x $. $d Z x $. $( If the range of a function does not contain the zero, the support of the @@ -745283,14 +745365,14 @@ The natural logarithm on complex numbers (extension) $} ${ - $d F f g x $. $d G f g x $. $d V f g $. $d W f g $. + $d F f g x $. $d G f g x $. $d V f g x $. $d W f g x $. $( The quotient of two functions into the complex numbers. (Contributed by AV, 15-May-2020.) $) fdivval $p |- ( ( F e. V /\ G e. W ) -> ( F /_f G ) = ( ( F oF / G ) |` ( G supp 0 ) ) ) $= ( vf vg vx wcel wa cvv cv cdiv co cc0 csupp cres cfdiv wceq adantl elex cof cmpo df-fdiv a1i oveq12 oveq1 reseq12d adantr wfun cdm cin cfv funmpt - cmpt offval0 funeqd mpbiri ovex resfunexg sylancl ovmpod ) ACHZBDHZIZEFAB + cmpt offval3 funeqd mpbiri ovex resfunexg sylancl ovmpod ) ACHZBDHZIZEFAB JJEKZFKZLUAZMZVFNOMZPZABVGMZBNOMZPZQJQEFJJVJUBRVDEFUCUDVEARZVFBRZIZVJVMRV DVPVHVKVIVLVEAVFBVGUEVOVIVLRVNVFBNOUFSUGSVBAJHVCACTUHVCBJHVBBDTSVDVKUIZVL JHVMJHVDVQGAUJBUJUKZGKZAULVSBULLMZUNZUIGVRVTUMVDVKWAGLABCDUOUPUQBNOURVKVL