diff --git a/changes-set.txt b/changes-set.txt index 39b9f7242f..37b7309694 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -102,6 +102,7 @@ Date Old New Notes 18-Nov-24 dfwrecs2 df-wrecs moved from BJ's mathbox to main set.mm and made the main definition 16-Nov-24 rspcdvinvd rspcdv2 moved from SP's mathbox to main set.mm +15-Nov-24 baseltedgf basendxltedgfndx 12-Nov-24 sseldi sselid compare to sselii or sseldd 11-Nov-24 mpteq12da [same] moved from GS's mathbox to main set.mm 9-Nov-24 eqsb3 eqsb1 diff --git a/discouraged b/discouraged index 045a2fe222..acbdbf641f 100644 --- a/discouraged +++ b/discouraged @@ -189,6 +189,7 @@ "1sr" is used by "axi2m1". "1sr" is used by "axicn". "1sr" is used by "supsr". +"1strstr" is used by "1strbasOLD". "1t1e1ALT" is used by "nnmul1com". "1t1e1ALT" is used by "remulinvcom". "1t1e1ALT" is used by "sn-0tie0". @@ -1672,16 +1673,17 @@ "basendx" is used by "1strstr". "basendx" is used by "2strstr". "basendx" is used by "2strstr1OLD". -"basendx" is used by "baseltedgf". "basendx" is used by "basendxltdsndx". +"basendx" is used by "basendxltedgfndx". "basendx" is used by "basendxltplendx". "basendx" is used by "basendxltplusgndx". "basendx" is used by "basendxlttsetndx". "basendx" is used by "basendxltunifndx". "basendx" is used by "basendxnmulrndx". "basendx" is used by "basendxnn". +"basendx" is used by "basendxnocndx". "basendx" is used by "catstr". -"basendx" is used by "cnfldfun". +"basendx" is used by "cnfldfunOLD". "basendx" is used by "eengstr". "basendx" is used by "grpbasex". "basendx" is used by "grpplusgx". @@ -1690,20 +1692,20 @@ "basendx" is used by "ipostr". "basendx" is used by "lmodstr". "basendx" is used by "mgpressOLD". -"basendx" is used by "odubas". +"basendx" is used by "odubasOLD". "basendx" is used by "oppcbasOLD". "basendx" is used by "otpsstr". -"basendx" is used by "rescabs". +"basendx" is used by "rescabsOLD". "basendx" is used by "rescbasOLD". "basendx" is used by "resslemOLD". "basendx" is used by "rngstr". "basendx" is used by "scandxnbasendx". -"basendx" is used by "setsmsbas". +"basendx" is used by "setsmsbasOLD". "basendx" is used by "slotsbhcdif". "basendx" is used by "slotsinbpsd". "basendx" is used by "slotslnbpsd". "basendx" is used by "starvndxnbasendx". -"basendx" is used by "thlbas". +"basendx" is used by "thlbasOLD". "basendx" is used by "topgrpstr". "basendx" is used by "trkgstr". "basendx" is used by "tuslemOLD". @@ -3271,6 +3273,17 @@ "ccatw2s1assOLD" is used by "ccat2s1fvwOLD". "ccatw2s1assOLD" is used by "ccatw2s1ccatws2OLD". "ccatw2s1ccatws2OLD" is used by "ccat2s1fvwALTOLD". +"ccondx" is used by "catstr". +"ccondx" is used by "oppcbasOLD". +"ccondx" is used by "oppchomfvalOLD". +"ccondx" is used by "prdsvalstr". +"ccondx" is used by "prstclevalOLD". +"ccondx" is used by "prstcocvalOLD". +"ccondx" is used by "resccoOLD". +"ccondx" is used by "slotsbhcdif". +"ccondx" is used by "slotsbhcdifOLD". +"ccondx" is used by "slotsdifocndx". +"ccondx" is used by "slotsdifplendx2". "cdj3lem1" is used by "cdj3i". "cdj3lem1" is used by "cdj3lem2b". "cdj3lem2" is used by "cdj3i". @@ -4724,6 +4737,7 @@ "df-cnfld" is used by "cnfldds". "df-cnfld" is used by "cnfldfun". "df-cnfld" is used by "cnfldfunALT". +"df-cnfld" is used by "cnfldfunOLD". "df-cnfld" is used by "cnfldle". "df-cnfld" is used by "cnfldmul". "df-cnfld" is used by "cnfldstr". @@ -5553,6 +5567,26 @@ "drsb1" is used by "iotaeq". "drsb1" is used by "sb2ae". "drsb1" is used by "sbco3". +"dsndx" is used by "basendxltdsndx". +"dsndx" is used by "cnfldfunOLD". +"dsndx" is used by "cnfldstr". +"dsndx" is used by "dsndxnmulrndx". +"dsndx" is used by "dsndxnn". +"dsndx" is used by "dsndxnplusgndx". +"dsndx" is used by "dsndxntsetndx". +"dsndx" is used by "eengstr". +"dsndx" is used by "imasvalstr". +"dsndx" is used by "odrngstr". +"dsndx" is used by "setsmsdsOLD". +"dsndx" is used by "slotsdifdsndx". +"dsndx" is used by "slotsdifunifndx". +"dsndx" is used by "slotsdnscsi". +"dsndx" is used by "slotsinbpsd". +"dsndx" is used by "slotslnbpsd". +"dsndx" is used by "tngdsOLD". +"dsndx" is used by "tnglemOLD". +"dsndx" is used by "trkgstr". +"dsndx" is used by "zlmdsOLD". "dtruALT2" is used by "fvprc". "dvadiaN" is used by "diarnN". "dveel1" is used by "distel". @@ -5940,7 +5974,7 @@ "e333" is used by "e33". "e3bi" is used by "en3lplem2VD". "e3bir" is used by "en3lplem2VD". -"edgfndx" is used by "baseltedgf". +"edgfndx" is used by "basendxltedgfndx". "edgfndx" is used by "edgfndxnn". "ee03" is used by "ee03an". "ee03" is used by "suctrALT2". @@ -7780,6 +7814,19 @@ "homco2" is used by "opsqrlem1". "hommval" is used by "homulcl". "hommval" is used by "homval". +"homndx" is used by "catstr". +"homndx" is used by "oppcbasOLD". +"homndx" is used by "oppchomfvalOLD". +"homndx" is used by "prdsvalstr". +"homndx" is used by "prstclevalOLD". +"homndx" is used by "prstcocvalOLD". +"homndx" is used by "rescabsOLD". +"homndx" is used by "rescbasOLD". +"homndx" is used by "resccoOLD". +"homndx" is used by "slotsbhcdif". +"homndx" is used by "slotsbhcdifOLD". +"homndx" is used by "slotsdifocndx". +"homndx" is used by "slotsdifplendx2". "homul12" is used by "hosubdi". "homulass" is used by "homul12". "homulass" is used by "honegneg". @@ -8868,6 +8915,18 @@ "ipidsq" is used by "pythi". "ipidsq" is used by "siilem1". "ipipcj" is used by "siii". +"ipndx" is used by "cchhllemOLD". +"ipndx" is used by "ipndxnbasendx". +"ipndx" is used by "ipndxnmulrndx". +"ipndx" is used by "ipndxnplusgndx". +"ipndx" is used by "ipsstr". +"ipndx" is used by "phlstr". +"ipndx" is used by "slotsdifipndx". +"ipndx" is used by "slotsdnscsi". +"ipndx" is used by "slotstnscsi". +"ipndx" is used by "sralemOLD". +"ipndx" is used by "srascaOLD". +"ipndx" is used by "sravscaOLD". "ipnm" is used by "hilnormi". "ipval" is used by "dipcl". "ipval" is used by "ipf". @@ -9036,6 +9095,12 @@ "isvciOLD" is used by "hhssnv". "isvciOLD" is used by "hilvc". "isvclem" is used by "isvcOLD". +"itvndx" is used by "eengstr". +"itvndx" is used by "lngndxnitvndx". +"itvndx" is used by "slotsinbpsd". +"itvndx" is used by "trkgstr". +"itvndx" is used by "ttglemOLD". +"itvndx" is used by "ttgvalOLD". "iunconnlem2" is used by "iunconnALT". "jaoded" is used by "suctrALT3". "joincomALT" is used by "joincom". @@ -9182,6 +9247,11 @@ "lnfnmuli" is used by "riesz3i". "lnfnsubi" is used by "lnfnconi". "lnfnsubi" is used by "riesz3i". +"lngndx" is used by "eengstr". +"lngndx" is used by "lngndxnitvndx". +"lngndx" is used by "slotslnbpsd". +"lngndx" is used by "ttglemOLD". +"lngndx" is used by "ttgvalOLD". "lno0" is used by "blocnilem". "lno0" is used by "lnomul". "lno0" is used by "lnon0". @@ -10058,6 +10128,26 @@ "mulresr" is used by "axmulrcl". "mulresr" is used by "axpre-mulgt0". "mulresr" is used by "axrrecex". +"mulrndx" is used by "basendxnmulrndx". +"mulrndx" is used by "basendxnmulrndxOLD". +"mulrndx" is used by "cnfldfunOLD". +"mulrndx" is used by "dsndxnmulrndx". +"mulrndx" is used by "ipndxnmulrndx". +"mulrndx" is used by "matscaOLD". +"mulrndx" is used by "matvscaOLD". +"mulrndx" is used by "mnringaddgdOLD". +"mulrndx" is used by "mnringbasedOLD". +"mulrndx" is used by "mnringscadOLD". +"mulrndx" is used by "mnringvscadOLD". +"mulrndx" is used by "opprlemOLD". +"mulrndx" is used by "plendxnmulrndx". +"mulrndx" is used by "plusgndxnmulrndx". +"mulrndx" is used by "rngstr". +"mulrndx" is used by "scandxnmulrndx". +"mulrndx" is used by "slotsdifunifndx". +"mulrndx" is used by "starvndxnmulrndx". +"mulrndx" is used by "tsetndxnmulrndx". +"mulrndx" is used by "vscandxnmulrndx". "mulsrpr" is used by "00sr". "mulsrpr" is used by "1idsr". "mulsrpr" is used by "distrsr". @@ -11379,6 +11469,13 @@ "ocin" is used by "pjoc1i". "ocin" is used by "pjpreeq". "ocin" is used by "ssjo". +"ocndx" is used by "basendxnocndx". +"ocndx" is used by "ipostr". +"ocndx" is used by "plendxnocndx". +"ocndx" is used by "prstcocvalOLD". +"ocndx" is used by "slotsdifocndx". +"ocndx" is used by "thlbasOLD". +"ocndx" is used by "thlleOLD". "ococ" is used by "chdmj1". "ococ" is used by "chdmj2". "ococ" is used by "chdmj3". @@ -12057,7 +12154,54 @@ "pl42lem2N" is used by "pl42lem4N". "pl42lem3N" is used by "pl42lem4N". "pl42lem4N" is used by "pl42N". +"plendx" is used by "basendxltplendx". +"plendx" is used by "cnfldfunOLD". +"plendx" is used by "cnfldstr". +"plendx" is used by "idlsrgstr". +"plendx" is used by "imasvalstr". +"plendx" is used by "ipostr". +"plendx" is used by "odrngstr". +"plendx" is used by "odubasOLD". +"plendx" is used by "opsrbaslemOLD". +"plendx" is used by "otpsstr". +"plendx" is used by "plendxnmulrndx". +"plendx" is used by "plendxnn". +"plendx" is used by "plendxnocndx". +"plendx" is used by "plendxnplusgndx". +"plendx" is used by "plendxnscandx". +"plendx" is used by "plendxnvscandx". +"plendx" is used by "prstclevalOLD". +"plendx" is used by "slotsdifdsndx". +"plendx" is used by "slotsdifplendx". +"plendx" is used by "slotsdifplendx2". +"plendx" is used by "slotsdifunifndx". +"plendx" is used by "thlleOLD". +"plendx" is used by "znbaslemOLD". "plpv" is used by "addcompr". +"plusgndx" is used by "basendxltplusgndx". +"plusgndx" is used by "basendxnplusgndxOLD". +"plusgndx" is used by "cnfldfunOLD". +"plusgndx" is used by "dsndxnplusgndx". +"plusgndx" is used by "grpbasex". +"plusgndx" is used by "grpplusgx". +"plusgndx" is used by "ipndxnplusgndx". +"plusgndx" is used by "lmodstr". +"plusgndx" is used by "mgplemOLD". +"plusgndx" is used by "mgpressOLD". +"plusgndx" is used by "oppglemOLD". +"plusgndx" is used by "plendxnplusgndx". +"plusgndx" is used by "plusgndxnmulrndx". +"plusgndx" is used by "plusgndxnn". +"plusgndx" is used by "rmodislmodOLD". +"plusgndx" is used by "rngstr". +"plusgndx" is used by "scandxnplusgndx". +"plusgndx" is used by "slotsdifunifndx". +"plusgndx" is used by "slotsinbpsd". +"plusgndx" is used by "slotslnbpsd". +"plusgndx" is used by "starvndxnplusgndx". +"plusgndx" is used by "topgrpstr". +"plusgndx" is used by "tsetndxnplusgndx". +"plusgndx" is used by "vscandxnplusgndx". "pm2.43cbi" is used by "ee233". "pm2.43cbi" is used by "ee33VD". "pmap1N" is used by "pmapglb2N". @@ -12733,6 +12877,26 @@ "sbied" is used by "wl-equsb3". "sbiedv" is used by "2sbiev". "sbtrt" is used by "sbtr". +"scandx" is used by "algstr". +"scandx" is used by "ipsstr". +"scandx" is used by "lmodstr". +"scandx" is used by "matscaOLD". +"scandx" is used by "plendxnscandx". +"scandx" is used by "psrvalstr". +"scandx" is used by "resvlemOLD". +"scandx" is used by "rmodislmodOLD". +"scandx" is used by "scandxnbasendx". +"scandx" is used by "scandxnmulrndx". +"scandx" is used by "scandxnplusgndx". +"scandx" is used by "slotsdifipndx". +"scandx" is used by "slotsdnscsi". +"scandx" is used by "slotstnscsi". +"scandx" is used by "sralemOLD". +"scandx" is used by "srascaOLD". +"scandx" is used by "vscandxnscandx". +"scandx" is used by "zlmdsOLD". +"scandx" is used by "zlmlemOLD". +"scandx" is used by "zlmtsetOLD". "setrec1lem1" is used by "setrec1lem2". "setrec1lem1" is used by "setrec1lem4". "setrec1lem1" is used by "setrec2fun". @@ -13366,6 +13530,16 @@ "ssralv2" is used by "ordelordALTVD". "st0" is used by "largei". "stadd3i" is used by "golem2". +"starvndx" is used by "cnfldfunOLD". +"starvndx" is used by "hlhilslemOLD". +"starvndx" is used by "slotsdifdsndx". +"starvndx" is used by "slotsdifplendx". +"starvndx" is used by "slotsdifunifndx". +"starvndx" is used by "srngstr". +"starvndx" is used by "starvndxnbasendx". +"starvndx" is used by "starvndxnmulrndx". +"starvndx" is used by "starvndxnplusgndx". +"starvndx" is used by "tsetndxnstarvndx". "stcl" is used by "golem1". "stcl" is used by "stadd3i". "stcl" is used by "staddi". @@ -13514,6 +13688,32 @@ "trsbc" is used by "trintALTVD". "trsbc" is used by "truniALT". "trsbc" is used by "truniALTVD". +"tsetndx" is used by "basendxlttsetndx". +"tsetndx" is used by "cnfldfunOLD". +"tsetndx" is used by "cnfldstr". +"tsetndx" is used by "dsndxntsetndx". +"tsetndx" is used by "idlsrgstr". +"tsetndx" is used by "imasvalstr". +"tsetndx" is used by "indistpsx". +"tsetndx" is used by "ipostr". +"tsetndx" is used by "odrngstr". +"tsetndx" is used by "otpsstr". +"tsetndx" is used by "psrvalstr". +"tsetndx" is used by "setsmsbasOLD". +"tsetndx" is used by "setsmsdsOLD". +"tsetndx" is used by "slotsdifplendx". +"tsetndx" is used by "slotstnscsi". +"tsetndx" is used by "symgvalstructOLD". +"tsetndx" is used by "tngdsOLD". +"tsetndx" is used by "tnglemOLD". +"tsetndx" is used by "topgrpstr". +"tsetndx" is used by "tsetndxnmulrndx". +"tsetndx" is used by "tsetndxnn". +"tsetndx" is used by "tsetndxnplusgndx". +"tsetndx" is used by "tsetndxnstarvndx". +"tsetndx" is used by "tuslemOLD". +"tsetndx" is used by "unifndxntsetndx". +"tsetndx" is used by "zlmtsetOLD". "ttglemOLD" is used by "ttgbasOLD". "ttglemOLD" is used by "ttgdsOLD". "ttglemOLD" is used by "ttgplusgOLD". @@ -13524,6 +13724,13 @@ "ubthlem3" is used by "ubth". "un0.1" is used by "sspwimpVD". "un2122" is used by "suctrALT3". +"unifndx" is used by "basendxltunifndx". +"unifndx" is used by "cnfldfunOLD". +"unifndx" is used by "cnfldstr". +"unifndx" is used by "slotsdifunifndx". +"unifndx" is used by "tuslemOLD". +"unifndx" is used by "unifndxnn". +"unifndx" is used by "unifndxntsetndx". "unop" is used by "cnvunop". "unop" is used by "counop". "unop" is used by "unopadj". @@ -13658,6 +13865,28 @@ "vd23" is used by "e23". "vd23" is used by "e32". "vmcn" is used by "hmopidmchi". +"vscandx" is used by "algstr". +"vscandx" is used by "ipsstr". +"vscandx" is used by "lmodstr". +"vscandx" is used by "matvscaOLD". +"vscandx" is used by "plendxnvscandx". +"vscandx" is used by "psrvalstr". +"vscandx" is used by "rmodislmodOLD". +"vscandx" is used by "slotsdifipndx". +"vscandx" is used by "slotsdnscsi". +"vscandx" is used by "slotsinbpsd". +"vscandx" is used by "slotslnbpsd". +"vscandx" is used by "slotstnscsi". +"vscandx" is used by "sralemOLD". +"vscandx" is used by "srascaOLD". +"vscandx" is used by "sravscaOLD". +"vscandx" is used by "vscandxnbasendx". +"vscandx" is used by "vscandxnmulrndx". +"vscandx" is used by "vscandxnplusgndx". +"vscandx" is used by "vscandxnscandx". +"vscandx" is used by "zlmdsOLD". +"vscandx" is used by "zlmlemOLD". +"vscandx" is used by "zlmtsetOLD". "vsfval" is used by "nvaddsub". "vsfval" is used by "nvm". "vsfval" is used by "nvmfval". @@ -14064,6 +14293,8 @@ New usage of "1pi" is discouraged (11 uses). New usage of "1pr" is discouraged (16 uses). New usage of "1psubclN" is discouraged (0 uses). New usage of "1sr" is discouraged (8 uses). +New usage of "1strbasOLD" is discouraged (0 uses). +New usage of "1strstr" is discouraged (1 uses). New usage of "1strwunOLD" is discouraged (0 uses). New usage of "1t1e1ALT" is discouraged (3 uses). New usage of "235t711" is discouraged (0 uses). @@ -14578,7 +14809,7 @@ New usage of "bafval" is discouraged (38 uses). New usage of "barbariALT" is discouraged (0 uses). New usage of "barocoALT" is discouraged (0 uses). New usage of "baseltedgfOLD" is discouraged (0 uses). -New usage of "basendx" is discouraged (39 uses). +New usage of "basendx" is discouraged (40 uses). New usage of "basendxnmulrndxOLD" is discouraged (0 uses). New usage of "basendxnnOLD" is discouraged (0 uses). New usage of "basendxnplusgndxOLD" is discouraged (0 uses). @@ -15152,6 +15383,7 @@ New usage of "ccatw2s1assOLD" is discouraged (2 uses). New usage of "ccatw2s1ccatws2OLD" is discouraged (1 uses). New usage of "ccatw2s1p1OLD" is discouraged (0 uses). New usage of "cchhllemOLD" is discouraged (0 uses). +New usage of "ccondx" is discouraged (11 uses). New usage of "cdeqab1" is discouraged (0 uses). New usage of "cdeqal1" is discouraged (0 uses). New usage of "cdj1i" is discouraged (0 uses). @@ -15493,6 +15725,7 @@ New usage of "cncph" is discouraged (2 uses). New usage of "cncvcOLD" is discouraged (1 uses). New usage of "cnexALT" is discouraged (0 uses). New usage of "cnfldfunALT" is discouraged (0 uses). +New usage of "cnfldfunOLD" is discouraged (0 uses). New usage of "cnfnc" is discouraged (1 uses). New usage of "cnidOLD" is discouraged (1 uses). New usage of "cnims" is discouraged (1 uses). @@ -15640,7 +15873,7 @@ New usage of "df-ch0" is discouraged (8 uses). New usage of "df-chj" is discouraged (1 uses). New usage of "df-chsup" is discouraged (1 uses). New usage of "df-cm" is discouraged (1 uses). -New usage of "df-cnfld" is discouraged (12 uses). +New usage of "df-cnfld" is discouraged (13 uses). New usage of "df-cnfn" is discouraged (2 uses). New usage of "df-cnop" is discouraged (2 uses). New usage of "df-com2" is discouraged (1 uses). @@ -15988,6 +16221,7 @@ New usage of "drnfc2OLD" is discouraged (0 uses). New usage of "drngcatALTV" is discouraged (0 uses). New usage of "drngoi" is discouraged (2 uses). New usage of "drsb1" is discouraged (3 uses). +New usage of "dsndx" is discouraged (20 uses). New usage of "dtruALT" is discouraged (0 uses). New usage of "dtruALT2" is discouraged (1 uses). New usage of "dtrucor2" is discouraged (0 uses). @@ -16873,6 +17107,7 @@ New usage of "homcl" is discouraged (0 uses). New usage of "homco1" is discouraged (1 uses). New usage of "homco2" is discouraged (1 uses). New usage of "hommval" is discouraged (2 uses). +New usage of "homndx" is discouraged (13 uses). New usage of "homul12" is discouraged (1 uses). New usage of "homulass" is discouraged (6 uses). New usage of "homulcl" is discouraged (21 uses). @@ -17103,6 +17338,7 @@ New usage of "ipdirilem" is discouraged (1 uses). New usage of "ipf" is discouraged (2 uses). New usage of "ipidsq" is discouraged (6 uses). New usage of "ipipcj" is discouraged (1 uses). +New usage of "ipndx" is discouraged (12 uses). New usage of "ipnm" is discouraged (1 uses). New usage of "ipval" is discouraged (3 uses). New usage of "ipval2" is discouraged (5 uses). @@ -17181,6 +17417,7 @@ New usage of "isvciOLD" is discouraged (3 uses). New usage of "isvclem" is discouraged (1 uses). New usage of "iswatN" is discouraged (0 uses). New usage of "itg1addlem4OLD" is discouraged (0 uses). +New usage of "itvndx" is discouraged (6 uses). New usage of "iunconnALT" is discouraged (0 uses). New usage of "iunconnlem2" is discouraged (1 uses). New usage of "ivthALT" is discouraged (0 uses). @@ -17279,6 +17516,7 @@ New usage of "lnfnli" is discouraged (3 uses). New usage of "lnfnmul" is discouraged (1 uses). New usage of "lnfnmuli" is discouraged (7 uses). New usage of "lnfnsubi" is discouraged (2 uses). +New usage of "lngndx" is discouraged (5 uses). New usage of "lnjatN" is discouraged (0 uses). New usage of "lno0" is discouraged (6 uses). New usage of "lnoadd" is discouraged (0 uses). @@ -17453,6 +17691,8 @@ New usage of "mapdval4N" is discouraged (2 uses). New usage of "mapdval5N" is discouraged (0 uses). New usage of "mappsrpr" is discouraged (2 uses). New usage of "mathbox" is discouraged (0 uses). +New usage of "matscaOLD" is discouraged (0 uses). +New usage of "matvscaOLD" is discouraged (0 uses). New usage of "max1ALT" is discouraged (0 uses). New usage of "mayete3i" is discouraged (1 uses). New usage of "mayetes3i" is discouraged (0 uses). @@ -17627,6 +17867,7 @@ New usage of "mulpipq2" is discouraged (6 uses). New usage of "mulpqf" is discouraged (5 uses). New usage of "mulpqnq" is discouraged (7 uses). New usage of "mulresr" is discouraged (4 uses). +New usage of "mulrndx" is discouraged (20 uses). New usage of "mulsrpr" is discouraged (9 uses). New usage of "n0OLD" is discouraged (0 uses). New usage of "n0lpligALT" is discouraged (0 uses). @@ -17998,6 +18239,7 @@ New usage of "occon2i" is discouraged (3 uses). New usage of "occon3" is discouraged (2 uses). New usage of "ocel" is discouraged (10 uses). New usage of "ocin" is discouraged (11 uses). +New usage of "ocndx" is discouraged (7 uses). New usage of "ocnel" is discouraged (0 uses). New usage of "ococ" is discouraged (19 uses). New usage of "ococi" is discouraged (12 uses). @@ -18008,6 +18250,7 @@ New usage of "ocsh" is discouraged (6 uses). New usage of "ocss" is discouraged (11 uses). New usage of "ocval" is discouraged (4 uses). New usage of "odfvalALT" is discouraged (0 uses). +New usage of "odubasOLD" is discouraged (0 uses). New usage of "oldmm3N" is discouraged (2 uses). New usage of "olposN" is discouraged (0 uses). New usage of "om0x" is discouraged (0 uses). @@ -18312,7 +18555,9 @@ New usage of "pl42lem1N" is discouraged (1 uses). New usage of "pl42lem2N" is discouraged (1 uses). New usage of "pl42lem3N" is discouraged (1 uses). New usage of "pl42lem4N" is discouraged (1 uses). +New usage of "plendx" is discouraged (23 uses). New usage of "plpv" is discouraged (1 uses). +New usage of "plusgndx" is discouraged (24 uses). New usage of "pm10.252" is discouraged (0 uses). New usage of "pm11.07" is discouraged (0 uses). New usage of "pm13.181OLD" is discouraged (0 uses). @@ -18375,7 +18620,9 @@ New usage of "probfinmeasbALTV" is discouraged (0 uses). New usage of "prpssnq" is discouraged (8 uses). New usage of "prstchom2ALT" is discouraged (0 uses). New usage of "prstchomval" is discouraged (3 uses). +New usage of "prstclevalOLD" is discouraged (0 uses). New usage of "prstcnidlem" is discouraged (2 uses). +New usage of "prstcocvalOLD" is discouraged (0 uses). New usage of "prstcval" is discouraged (2 uses). New usage of "prub" is discouraged (6 uses). New usage of "psrass1lemOLD" is discouraged (0 uses). @@ -18497,6 +18744,7 @@ New usage of "relopabiALT" is discouraged (0 uses). New usage of "relrngo" is discouraged (6 uses). New usage of "renegclALT" is discouraged (0 uses). New usage of "renicax" is discouraged (0 uses). +New usage of "rescabsOLD" is discouraged (0 uses). New usage of "rescbasOLD" is discouraged (0 uses). New usage of "resccoOLD" is discouraged (0 uses). New usage of "resfunexgALT" is discouraged (0 uses). @@ -18710,6 +18958,7 @@ New usage of "sbtALT" is discouraged (0 uses). New usage of "sbtT" is discouraged (0 uses). New usage of "sbtr" is discouraged (0 uses). New usage of "sbtrt" is discouraged (1 uses). +New usage of "scandx" is discouraged (20 uses). New usage of "scmateALT" is discouraged (0 uses). New usage of "seq1hcau" is discouraged (0 uses). New usage of "seqp1iOLD" is discouraged (0 uses). @@ -18721,6 +18970,8 @@ New usage of "setrec2fun" is discouraged (1 uses). New usage of "setrec2lem1" is discouraged (1 uses). New usage of "setrec2lem2" is discouraged (1 uses). New usage of "setsidvaldOLD" is discouraged (1 uses). +New usage of "setsmsbasOLD" is discouraged (0 uses). +New usage of "setsmsdsOLD" is discouraged (0 uses). New usage of "setsnidOLD" is discouraged (0 uses). New usage of "sgrpplusgaopALT" is discouraged (0 uses). New usage of "sh0" is discouraged (13 uses). @@ -18882,7 +19133,9 @@ New usage of "srabaseOLD" is discouraged (0 uses). New usage of "sradsOLD" is discouraged (0 uses). New usage of "sralemOLD" is discouraged (6 uses). New usage of "sramulrOLD" is discouraged (0 uses). +New usage of "srascaOLD" is discouraged (0 uses). New usage of "sratsetOLD" is discouraged (0 uses). +New usage of "sravscaOLD" is discouraged (0 uses). New usage of "srhmsubcALTV" is discouraged (4 uses). New usage of "srhmsubcALTVlem1" is discouraged (2 uses). New usage of "srhmsubcALTVlem2" is discouraged (1 uses). @@ -18940,6 +19193,7 @@ New usage of "sstrALT2VD" is discouraged (0 uses). New usage of "st0" is discouraged (1 uses). New usage of "stadd3i" is discouraged (1 uses). New usage of "staddi" is discouraged (0 uses). +New usage of "starvndx" is discouraged (10 uses). New usage of "stcl" is discouraged (10 uses). New usage of "stcltr1i" is discouraged (2 uses). New usage of "stcltr2i" is discouraged (1 uses). @@ -19027,6 +19281,8 @@ New usage of "tfr1ALT" is discouraged (0 uses). New usage of "tfr2ALT" is discouraged (0 uses). New usage of "tfr3ALT" is discouraged (0 uses). New usage of "thincmoALT" is discouraged (0 uses). +New usage of "thlbasOLD" is discouraged (0 uses). +New usage of "thlleOLD" is discouraged (0 uses). New usage of "tmslemOLD" is discouraged (0 uses). New usage of "tngbasOLD" is discouraged (0 uses). New usage of "tngdsOLD" is discouraged (0 uses). @@ -19055,10 +19311,12 @@ New usage of "truniALT" is discouraged (0 uses). New usage of "truniALTVD" is discouraged (0 uses). New usage of "trunorfalOLD" is discouraged (0 uses). New usage of "trunortruOLD" is discouraged (0 uses). +New usage of "tsetndx" is discouraged (26 uses). New usage of "ttgbasOLD" is discouraged (0 uses). New usage of "ttgdsOLD" is discouraged (0 uses). New usage of "ttglemOLD" is discouraged (4 uses). New usage of "ttgplusgOLD" is discouraged (0 uses). +New usage of "ttgvalOLD" is discouraged (0 uses). New usage of "ttgvscaOLD" is discouraged (0 uses). New usage of "tuslemOLD" is discouraged (0 uses). New usage of "tz6.26OLD" is discouraged (0 uses). @@ -19075,6 +19333,7 @@ New usage of "undif3VD" is discouraged (0 uses). New usage of "unfiOLD" is discouraged (0 uses). New usage of "unieqOLD" is discouraged (0 uses). New usage of "unierri" is discouraged (0 uses). +New usage of "unifndx" is discouraged (7 uses). New usage of "uniprOLD" is discouraged (0 uses). New usage of "uniprgOLD" is discouraged (0 uses). New usage of "unipwr" is discouraged (0 uses). @@ -19163,6 +19422,7 @@ New usage of "vk15.4j" is discouraged (0 uses). New usage of "vk15.4jVD" is discouraged (0 uses). New usage of "vmcn" is discouraged (1 uses). New usage of "vn0ALT" is discouraged (0 uses). +New usage of "vscandx" is discouraged (22 uses). New usage of "vsfval" is discouraged (4 uses). New usage of "vtocl3gaOLD" is discouraged (0 uses). New usage of "vtoclALT" is discouraged (0 uses). @@ -19275,9 +19535,11 @@ 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 "zlmdsOLD" 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 "zlmtsetOLD" 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). @@ -19301,6 +19563,7 @@ Proof modification of "1div0apr" is discouraged (77 steps). Proof modification of "1oexOLD" is discouraged (4 steps). Proof modification of "1p1e2apr1" is discouraged (7 steps). Proof modification of "1p2e3ALT" is discouraged (7 steps). +Proof modification of "1strbasOLD" is discouraged (22 steps). Proof modification of "1strwunOLD" is discouraged (20 steps). Proof modification of "1t1e1ALT" is discouraged (13 steps). Proof modification of "2bornot2b" is discouraged (26 steps). @@ -19755,6 +20018,7 @@ Proof modification of "cnaddcom" is discouraged (71 steps). Proof modification of "cncvcOLD" is discouraged (38 steps). Proof modification of "cnexALT" is discouraged (52 steps). Proof modification of "cnfldfunALT" is discouraged (423 steps). +Proof modification of "cnfldfunOLD" is discouraged (1101 steps). Proof modification of "cnidOLD" is discouraged (118 steps). Proof modification of "cnncvsabsnegdemo" is discouraged (74 steps). Proof modification of "cnncvsaddassdemo" is discouraged (46 steps). @@ -20465,6 +20729,8 @@ Proof modification of "lukshef-ax1" is discouraged (6 steps). Proof modification of "lukshefth1" is discouraged (88 steps). Proof modification of "lukshefth2" is discouraged (129 steps). Proof modification of "mathbox" is discouraged (1 steps). +Proof modification of "matscaOLD" is discouraged (73 steps). +Proof modification of "matvscaOLD" is discouraged (69 steps). Proof modification of "max1ALT" is discouraged (48 steps). Proof modification of "meetcomALT" is discouraged (83 steps). Proof modification of "merco1" is discouraged (57 steps). @@ -20629,6 +20895,7 @@ Proof modification of "notnotriALT" is discouraged (7 steps). Proof modification of "nsnlpligALT" is discouraged (110 steps). Proof modification of "o2p2e4OLD" is discouraged (67 steps). Proof modification of "odfvalALT" is discouraged (181 steps). +Proof modification of "odubasOLD" is discouraged (62 steps). Proof modification of "omsindsOLD" is discouraged (89 steps). Proof modification of "ondomon" is discouraged (287 steps). Proof modification of "onfrALT" is discouraged (88 steps). @@ -20700,6 +20967,8 @@ Proof modification of "problem3" is discouraged (56 steps). Proof modification of "problem4" is discouraged (310 steps). Proof modification of "problem5" is discouraged (133 steps). Proof modification of "prstchom2ALT" is discouraged (121 steps). +Proof modification of "prstclevalOLD" is discouraged (86 steps). +Proof modification of "prstcocvalOLD" is discouraged (88 steps). Proof modification of "psrass1lemOLD" is discouraged (1513 steps). Proof modification of "psrbagaddclOLD" is discouraged (392 steps). Proof modification of "psrbagconOLD" is discouraged (365 steps). @@ -20779,6 +21048,7 @@ Proof modification of "relopabiALT" is discouraged (74 steps). Proof modification of "renegcl" is discouraged (34 steps). Proof modification of "renegclALT" is discouraged (149 steps). Proof modification of "renicax" is discouraged (76 steps). +Proof modification of "rescabsOLD" is discouraged (602 steps). Proof modification of "rescbasOLD" is discouraged (106 steps). Proof modification of "resccoOLD" is discouraged (115 steps). Proof modification of "resfunexgALT" is discouraged (76 steps). @@ -20882,6 +21152,8 @@ Proof modification of "sbtT" is discouraged (7 steps). Proof modification of "scmateALT" is discouraged (236 steps). Proof modification of "seqp1iOLD" is discouraged (20 steps). Proof modification of "setsidvaldOLD" is discouraged (93 steps). +Proof modification of "setsmsbasOLD" is discouraged (55 steps). +Proof modification of "setsmsdsOLD" is discouraged (62 steps). Proof modification of "setsnidOLD" is discouraged (140 steps). Proof modification of "sgrpplusgaopALT" is discouraged (82 steps). Proof modification of "sii" is discouraged (145 steps). @@ -20908,7 +21180,9 @@ Proof modification of "srabaseOLD" is discouraged (21 steps). Proof modification of "sradsOLD" is discouraged (34 steps). Proof modification of "sralemOLD" is discouraged (368 steps). Proof modification of "sramulrOLD" is discouraged (21 steps). +Proof modification of "srascaOLD" is discouraged (204 steps). Proof modification of "sratsetOLD" is discouraged (21 steps). +Proof modification of "sravscaOLD" is discouraged (177 steps). Proof modification of "ss2abdvALT" is discouraged (41 steps). Proof modification of "ss2abdvOLD" is discouraged (23 steps). Proof modification of "ss2abiOLD" is discouraged (17 steps). @@ -20971,6 +21245,8 @@ Proof modification of "tfr1ALT" is discouraged (29 steps). Proof modification of "tfr2ALT" is discouraged (63 steps). Proof modification of "tfr3ALT" is discouraged (95 steps). Proof modification of "thincmoALT" is discouraged (93 steps). +Proof modification of "thlbasOLD" is discouraged (141 steps). +Proof modification of "thlleOLD" is discouraged (217 steps). Proof modification of "tmslemOLD" is discouraged (174 steps). Proof modification of "tngbasOLD" is discouraged (23 steps). Proof modification of "tngdsOLD" is discouraged (188 steps). @@ -21003,6 +21279,7 @@ Proof modification of "ttgbasOLD" is discouraged (25 steps). Proof modification of "ttgdsOLD" is discouraged (31 steps). Proof modification of "ttglemOLD" is discouraged (273 steps). Proof modification of "ttgplusgOLD" is discouraged (25 steps). +Proof modification of "ttgvalOLD" is discouraged (845 steps). Proof modification of "ttgvscaOLD" is discouraged (25 steps). Proof modification of "tuslemOLD" is discouraged (304 steps). Proof modification of "tz6.26OLD" is discouraged (96 steps). @@ -21173,9 +21450,11 @@ 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 "zlmdsOLD" is discouraged (122 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 "zlmtsetOLD" is discouraged (102 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). diff --git a/set.mm b/set.mm index b3a3a67590..1da41e0251 100644 --- a/set.mm +++ b/set.mm @@ -201137,14 +201137,28 @@ C_ dom ( S sSet <. I , E >. ) ) $= ${ 1str.g $e |- G = { <. ( Base ` ndx ) , B >. } $. - $( A constructed one-slot structure. (Contributed by AV, 27-Mar-2020.) $) + $( A constructed one-slot structure. Depending on hard-coded index. Use + ~ 1strstr1 instead. (Contributed by AV, 27-Mar-2020.) + (New usage is discouraged.) $) 1strstr $p |- G Struct <. 1 , 1 >. $= ( cnx cbs cfv cop csn c1 cstr 1nn basendx strle1 eqbrtri ) BDEFZAGHIIGJCO IAKLMN $. + $( A constructed one-slot structure. (Contributed by AV, 15-Nov-2024.) $) + 1strstr1 $p |- G Struct <. ( Base ` ndx ) , ( Base ` ndx ) >. $= + ( cnx cbs cfv cop csn cstr basendxnn eqid strle1 eqbrtri ) BDEFZAGHNNGICN + NAJNKLM $. + $( The base set of a constructed one-slot structure. (Contributed by AV, - 27-Mar-2020.) $) + 27-Mar-2020.) (Proof shortened by AV, 15-Nov-2024.) $) 1strbas $p |- ( B e. V -> B = ( Base ` G ) ) $= + ( cbs cnx cfv cop 1strstr1 baseid csn eqimss2i strfv ) ABECFEGZNHABDIJBNA + HKDLM $. + + $( Obsolete proof of ~ 1strbas as of 15-Nov-2024. The base set of a + constructed one-slot structure. (Contributed by AV, 27-Mar-2020.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + 1strbasOLD $p |- ( B e. V -> B = ( Base ` G ) ) $= ( cbs c1 cop 1strstr baseid cnx cfv csn eqimss2i strfv ) ABECFFGABDHIBJEK AGLDMN $. @@ -201649,7 +201663,7 @@ C_ dom ( S sSet <. I , E >. ) ) $= df-cco $a |- comp = Slot ; 1 5 $. $( Index value of the ~ df-plusg slot. (Contributed by Mario Carneiro, - 14-Aug-2015.) $) + 14-Aug-2015.) (New usage is discouraged.) $) plusgndx $p |- ( +g ` ndx ) = 2 $= ( cplusg c2 df-plusg 2nn ndxarg ) ABCDE $. @@ -201761,7 +201775,7 @@ C_ dom ( S sSet <. I , E >. ) ) $= $} $( Index value of the ~ df-mulr slot. (Contributed by Mario Carneiro, - 14-Aug-2015.) $) + 14-Aug-2015.) (New usage is discouraged.) $) mulrndx $p |- ( .r ` ndx ) = 3 $= ( cmulr c3 df-mulr 3nn ndxarg ) ABCDE $. @@ -201824,7 +201838,7 @@ base set is not the slot for the ring (multiplication) operation in an $} $( Index value of the ~ df-starv slot. (Contributed by Mario Carneiro, - 14-Aug-2015.) $) + 14-Aug-2015.) (New usage is discouraged.) $) starvndx $p |- ( *r ` ndx ) = 4 $= ( cstv c4 df-starv 4nn ndxarg ) ABCDE $. @@ -201915,7 +201929,7 @@ base set is not the slot for the ring (multiplication) operation in an $} $( Index value of the ~ df-sca slot. (Contributed by Mario Carneiro, - 14-Aug-2015.) $) + 14-Aug-2015.) (New usage is discouraged.) $) scandx $p |- ( Scalar ` ndx ) = 5 $= ( csca c5 df-sca 5nn ndxarg ) ABCDE $. @@ -201945,7 +201959,7 @@ base set is not the slot for the ring (multiplication) operation in an ) ABCZADCZEFGEGFHIJOFPGKLMN $. $( Index value of the ~ df-vsca slot. (Contributed by Mario Carneiro, - 14-Aug-2015.) $) + 14-Aug-2015.) (New usage is discouraged.) $) vscandx $p |- ( .s ` ndx ) = 6 $= ( cvsca c6 df-vsca 6nn ndxarg ) ABCDE $. @@ -202030,7 +202044,7 @@ base set is not the slot for the ring (multiplication) operation in an $} $( Index value of the ~ df-ip slot. (Contributed by Mario Carneiro, - 14-Aug-2015.) $) + 14-Aug-2015.) (New usage is discouraged.) $) ipndx $p |- ( .i ` ndx ) = 8 $= ( cip c8 df-ip 8nn ndxarg ) ABCDE $. @@ -202058,6 +202072,14 @@ base set is not the slot for the ring (multiplication) operation in an ( cnx cip cfv cmulr wne c8 c3 3re 3lt8 gtneii ipndx mulrndx neeq12i mpbir ) ABCZADCZEFGEGFHIJOFPGKLMN $. + $( The slot for the scalar is not the index of other slots. Formerly part of + proof for ~ srasca and ~ sravsca . (Contributed by AV, 12-Nov-2024.) $) + slotsdifipndx $p |- ( ( .s ` ndx ) =/= ( .i ` ndx ) + /\ ( Scalar ` ndx ) =/= ( .i ` ndx ) ) $= + ( cnx cvsca cfv cip wne csca c6 6re 6lt8 ltneii vscandx ipndx neeq12i mpbir + c8 c5 5re 5lt8 scandx pm3.2i ) ABCZADCZEZAFCZUBEZUCGOEGOHIJUAGUBOKLMNUEPOEP + OQRJUDPUBOSLMNT $. + ${ ipspart.a $e |- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. @@ -202203,7 +202225,7 @@ base set is not the slot for the ring (multiplication) operation in an $} $( Index value of the ~ df-tset slot. (Contributed by Mario Carneiro, - 14-Aug-2015.) $) + 14-Aug-2015.) (New usage is discouraged.) $) tsetndx $p |- ( TopSet ` ndx ) = 9 $= ( cts c9 df-tset 9nn ndxarg ) ABCDE $. @@ -202243,6 +202265,13 @@ base set is not the slot for the ring (multiplication) operation in an ( cnx cts cfv cmulr wne c9 c3 3re 3lt9 gtneii tsetndx mulrndx neeq12i mpbir ) ABCZADCZEFGEGFHIJOFPGKLMN $. + $( The slot for the topology is not the slot for the involution in an + extensible structure. Formerly part of proof for ~ cnfldfun . + (Contributed by AV, 11-Nov-2024.) $) + tsetndxnstarvndx $p |- ( TopSet ` ndx ) =/= ( *r ` ndx ) $= + ( cnx cts cfv cstv wne c9 c4 4re 4lt9 gtneii tsetndx starvndx neeq12i mpbir + ) ABCZADCZEFGEGFHIJOFPGKLMN $. + $( The slots ` Scalar ` , ` .s ` and ` .i ` are different from the slot ` TopSet ` . Formerly part of ~ sralem and proofs using it. (Contributed by AV, 29-Oct-2024.) $) @@ -202293,7 +202322,8 @@ base set is not the slot for the ring (multiplication) operation in an $} $( Index value of the ~ df-ple slot. (Contributed by Mario Carneiro, - 14-Aug-2015.) (Revised by AV, 9-Sep-2021.) $) + 14-Aug-2015.) (Revised by AV, 9-Sep-2021.) + (New usage is discouraged.) $) plendx $p |- ( le ` ndx ) = ; 1 0 $= ( cple c1 cc0 cdc df-ple 10nn ndxarg ) ABCDEFG $. @@ -202349,6 +202379,15 @@ be used in an extensible structure (slots must be positive integers). ( cnx cple cfv cvsca wne c1 cc0 cdc 6re 6lt10 gtneii plendx vscandx neeq12i c6 mpbir ) ABCZADCZEFGHZOEOSIJKQSROLMNP $. + $( The index of the slot for the distance is not the index of other slots. + Formerly part of proof for ~ cnfldfun . (Contributed by AV, + 11-Nov-2024.) $) + slotsdifplendx $p |- ( ( *r ` ndx ) =/= ( le ` ndx ) + /\ ( TopSet ` ndx ) =/= ( le ` ndx ) ) $= + ( cnx cstv cfv cple wne cts c4 c1 cc0 cdc 4re 4lt10 ltneii starvndx neeq12i + plendx mpbir c9 9re 9lt10 tsetndx pm3.2i ) ABCZADCZEZAFCZUDEZUEGHIJZEGUHKLM + UCGUDUHNPOQUGRUHERUHSTMUFRUDUHUAPOQUB $. + ${ otpsstr.w $e |- K = { <. ( Base ` ndx ) , B >. , <. ( TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. } $. @@ -202388,7 +202427,7 @@ be used in an extensible structure (slots must be positive integers). $} $( Index value of the ~ df-ocomp slot. (Contributed by Mario Carneiro, - 25-Oct-2015.) $) + 25-Oct-2015.) (New usage is discouraged.) $) ocndx $p |- ( oc ` ndx ) = ; 1 1 $= ( coc c1 cdc df-ocomp 1nn0 1nn decnncl ndxarg ) ABBCDBBEFGH $. @@ -202397,8 +202436,22 @@ be used in an extensible structure (slots must be positive integers). ocid $p |- oc = Slot ( oc ` ndx ) $= ( coc c1 cdc df-ocomp 1nn0 1nn decnncl ndxid ) ABBCDBBEFGH $. + $( The slot for the orthocomplementation is not the slot for the base set in + an extensible structure. Formerly part of proof for ~ thlbas . + (Contributed by AV, 11-Nov-2024.) $) + basendxnocndx $p |- ( Base ` ndx ) =/= ( oc ` ndx ) $= + ( cnx cbs cfv coc wne c1 cdc 1re 1nn 1nn0 1lt10 declti ltneii basendx ocndx + neeq12i mpbir ) ABCZADCZEFFFGZEFTHFFFIJJKLMRFSTNOPQ $. + + $( The slot for the orthocomplementation is not the slot for the order in an + extensible structure. Formerly part of proof for ~ thlle . (Contributed + by AV, 11-Nov-2024.) $) + plendxnocndx $p |- ( le ` ndx ) =/= ( oc ` ndx ) $= + ( cnx cple cfv coc wne cc0 cdc 10re 1nn0 0nn0 1nn declt ltneii plendx ocndx + c1 0lt1 neeq12i mpbir ) ABCZADCZEPFGZPPGZEUBUCHPFPIJKQLMTUBUAUCNORS $. + $( Index value of the ~ df-ds slot. (Contributed by Mario Carneiro, - 14-Aug-2015.) $) + 14-Aug-2015.) (New usage is discouraged.) $) dsndx $p |- ( dist ` ndx ) = ; 1 2 $= ( cds c1 c2 cdc df-ds 1nn0 2nn decnncl ndxarg ) ABCDEBCFGHI $. @@ -202460,8 +202513,18 @@ be used in an extensible structure (slots must be positive integers). ( cnx cds cfv cts wne c1 c2 cdc 9re 1nn 2nn0 9nn0 9lt10 declti gtneii dsndx c9 tsetndx neeq12i mpbir ) ABCZADCZEFGHZQEQUCIFGQJKLMNOUAUCUBQPRST $. + $( The index of the slot for the distance is not the index of other slots. + Formerly part of proof for ~ cnfldfun . (Contributed by AV, + 11-Nov-2024.) $) + slotsdifdsndx $p |- ( ( *r ` ndx ) =/= ( dist ` ndx ) + /\ ( le ` ndx ) =/= ( dist ` ndx ) ) $= + ( cnx cstv cfv cds wne cple c4 c1 c2 cdc 4re 2nn0 4nn0 4lt10 ltneii neeq12i + 1nn dsndx mpbir cc0 declti starvndx 10re 1nn0 0nn0 2pos declt plendx pm3.2i + 2nn ) ABCZADCZEZAFCZULEZUMGHIJZEGUPKHIGQLMNUAOUKGULUPUBRPSUOHTJZUPEUQUPUCHT + IUDUEUJUFUGOUNUQULUPUHRPSUI $. + $( Index value of the ~ df-unif slot. (Contributed by Thierry Arnoux, - 17-Dec-2017.) $) + 17-Dec-2017.) (New usage is discouraged.) $) unifndx $p |- ( UnifSet ` ndx ) = ; 1 3 $= ( cunif c1 c3 cdc df-unif 1nn0 3nn decnncl ndxarg ) ABCDEBCFGHI $. @@ -202497,6 +202560,22 @@ be used in an extensible structure (slots must be positive integers). ( cnx cunif cfv cts wne c1 c3 cdc c9 9re 1nn 3nn0 9nn0 9lt10 declti unifndx gtneii tsetndx neeq12i mpbir ) ABCZADCZEFGHZIEIUCJFGIKLMNOQUAUCUBIPRST $. + $( The index of the slot for the uniform set is not the index of other slots. + Formerly part of proof for ~ cnfldfun . (Contributed by AV, + 10-Nov-2024.) $) + slotsdifunifndx $p |- ( ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) + /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) + /\ ( *r ` ndx ) =/= ( UnifSet ` ndx ) ) + /\ ( ( le ` ndx ) =/= ( UnifSet ` ndx ) + /\ ( dist ` ndx ) =/= ( UnifSet ` ndx ) ) ) $= + ( cnx cfv wne c2 c1 c3 cdc 3nn0 2nn0 declti ltneii unifndx neeq12i mpbir c4 + 1nn cc0 1nn0 3nn declt cplusg cunif cmulr cstv w3a cple cds wa 2re plusgndx + 2lt10 3re 3lt10 mulrndx 4re 4nn0 starvndx 3pm3.2i 10re 0nn0 3pos plendx 2nn + 4lt10 decnncl nnrei 2lt3 dsndx pm3.2i ) AUABZAUBBZCZAUCBZVKCZAUDBZVKCZUEAUF + BZVKCZAUGBZVKCZUHVLVNVPVLDEFGZCDWAUIEFDPHIUKJKVJDVKWAUJLMNVNFWACFWAULEFFPHH + UMJKVMFVKWAUNLMNVPOWACOWAUOEFOPHUPVDJKVOOVKWAUQLMNURVRVTVREQGZWACWBWAUSEQFR + UTSVATKVQWBVKWAVBLMNVTEDGZWACWCWAWCEDRVCVEVFEDFRISVGTKVSWCVKWAVHLMNVIVI $. + ${ ressunif.1 $e |- H = ( G |`s A ) $. ressunif.2 $e |- U = ( UnifSet ` G ) $. @@ -202573,7 +202652,7 @@ be used in an extensible structure (slots must be positive integers). $} $( Index value of the ~ df-hom slot. (Contributed by Mario Carneiro, - 7-Jan-2017.) $) + 7-Jan-2017.) (New usage is discouraged.) $) homndx $p |- ( Hom ` ndx ) = ; 1 4 $= ( chom c1 c4 cdc df-hom 1nn0 4nn decnncl ndxarg ) ABCDEBCFGHI $. @@ -202583,7 +202662,7 @@ be used in an extensible structure (slots must be positive integers). ( chom c1 c4 cdc df-hom 1nn0 4nn decnncl ndxid ) ABCDEBCFGHI $. $( Index value of the ~ df-cco slot. (Contributed by Mario Carneiro, - 7-Jan-2017.) $) + 7-Jan-2017.) (New usage is discouraged.) $) ccondx $p |- ( comp ` ndx ) = ; 1 5 $= ( cco c1 c5 cdc df-cco 1nn0 5nn decnncl ndxarg ) ABCDEBCFGHI $. @@ -202614,6 +202693,26 @@ be used in an extensible structure (slots must be positive integers). FUMUNFFSIZUMFUPPFSFGUDKLMNTORULUOUMQUOUPUMUOUPUOFHKJUEUFFHSKJUGUIUHNTORUJ $. + $( The index of the slot for the "less than or equal to" ordering is not the + index of other slots. Formerly part of proof for ~ prstcleval . + (Contributed by AV, 12-Nov-2024.) $) + slotsdifplendx2 $p |- ( ( le ` ndx ) =/= ( comp ` ndx ) + /\ ( le ` ndx ) =/= ( Hom ` ndx ) ) $= + ( cnx cple cfv cco wne chom c1 cc0 cdc c5 10re 1nn0 5nn declt ltneii plendx + 0nn0 neeq12i mpbir c4 5pos ccondx 4nn 4pos homndx pm3.2i ) ABCZADCZEZUGAFCZ + EZUIGHIZGJIZEULUMKGHJLQMUANOUGULUHUMPUBRSUKULGTIZEULUNKGHTLQUCUDNOUGULUJUNP + UERSUF $. + + $( The index of the slot for the orthocomplementation is not the index of + other slots. Formerly part of proof for ~ prstcocval . (Contributed by + AV, 12-Nov-2024.) $) + slotsdifocndx $p |- ( ( oc ` ndx ) =/= ( comp ` ndx ) + /\ ( oc ` ndx ) =/= ( Hom ` ndx ) ) $= + ( cnx coc cfv cco wne chom c1 cdc c5 1nn0 1nn decnncl nnrei 5nn declt ocndx + ltneii neeq12i mpbir c4 1lt5 ccondx 4nn 1lt4 homndx pm3.2i ) ABCZADCZEZUGAF + CZEZUIGGHZGIHZEULUMULGGJKLMZGGIJJNUAOQUGULUHUMPUBRSUKULGTHZEULUOUNGGTJJUCUD + OQUGULUJUOPUERSUF $. + ${ resshom.1 $e |- D = ( C |`s A ) $. ${ @@ -209218,8 +209317,32 @@ which when given operations from the base category (using ~ df-resc ) rescabs.s $e |- ( ph -> S e. W ) $. rescabs.t $e |- ( ph -> T C_ S ) $. $( Restriction absorption law. (Contributed by Mario Carneiro, - 6-Jan-2017.) $) + 6-Jan-2017.) (Proof shortened by AV, 9-Nov-2024.) $) rescabs $p |- ( ph -> ( ( C |`cat H ) |`cat J ) = ( C |`cat J ) ) $= + ( cress co csts cvv eqid wceq wcel cnx cfv cop cresc ovexd ssexd rescval2 + cbs wss wa simpr adantr baseid wne cco slotsbhcdif simp1i setsnid ressid2 + chom syl3anc oveq1d ovex cxp xpexd setsabs sylancr cin ressbas syl sseq1d + fnexd biimpar inss2 ssind ssrind eqssd oveq2d ressinbas 3eqtr4d 3eqtrd wn + ressval2 necomi fvex inex2 setscom syl22anc ressabs syl2an2r eqtr3d eqtrd + a1i pm2.61dan ) ABCNOZUAUTUBZEUCZPOZFUDOZBDNOZWPFUCZPOZBEUDOZFUDOBFUDOZAW + SWRDNOZXAPOZXBAWRWSDFQQWSRAWOWQPUEADCHLMUFZKUGAWOUHUBZDUIZXFXBSAXIUJZXFWR + XAPOZWOXAPOZXBXJXEWRXAPXJXIWRQTZDQTZXEWRSAXIUKXJWOWQPUEAXNXIXGULZDXHXEWRQ + QXERZEWPUHWOUMUAUHUBZWPUNXQUAUOUBZUNWPXRUNUPUQZURZUSVAVBXJWOQTZFQTZXKXLSB + CNVCAYBXIADDVDFQKADDQQXGXGVEVLZULWPEFWOQQVFVGXJWOWTXAPXJBCBUHUBZVHZNOZBDY + DVHZNOZWOWTXJYEYGBNXJYEYGXJYEDYDAYEDUIXIAYEXHDACHTZYEXHSLCYDWOHBWORYDRZVI + VJVKVMYEYDUIXJCYDVNWMVOXJDCYDADCUIZXIMULVPVQVRXJYIWOYFSAYIXILULCYDBHYJVSV + JXJXNWTYHSXODYDBQYJVSVJVTVBWAAXIWBZUJZXFWTWQPOZXAPOZXBYMXEYNXAPYMXEWRXQDX + HVHZUCZPOZWOYQPOZWQPOZYNYMYLXMXNXEYRSAYLUKZYMWOWQPUEAXNYLXGULZDXHXEWRQQXP + XTWCVAYMYAWPXQUNZEQTZYPQTZYRYTSYMBCNUEZUUCYMXQWPXSWDWMAUUDYLACCVDEQJACCHH + LLVEVLULUUEYMXHDWOUHWEWFWMWPXQEYPWOQQQUAUTWEUAUHWEWGWHYMYSWTWQPYMWODNOZYS + WTYMYLYAXNUUGYSSUUAUUFUUBDXHUUGWOQQUUGRXHRWCVAAYIYLYKUUGWTSLAYKYLMULCDBHW + IWJWKVBWAVBYMWTQTYBYOXBSBDNVCAYBYLYCULWPEFWTQQVFVGWLWNWLAXCWRFUDABXCCEGHX + CRILJUGVBABXDDFGQXDRIXGKUGVT $. + + $( Obsolete proof of ~ seqp1d as of 10-Nov-2024. Restriction absorption + law. (Contributed by Mario Carneiro, 6-Jan-2017.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + rescabsOLD $p |- ( ph -> ( ( C |`cat H ) |`cat J ) = ( C |`cat J ) ) $= ( cress co csts cvv wceq wcel adantr cnx chom cfv cop cresc eqid rescval2 ovexd ssexd cbs wss wa simpr baseid wne c1 c4 cdc 1re 1nn 4nn0 1nn0 1lt10 declti ltneii basendx homndx neeq12i mpbir setsnid ressid2 syl3anc oveq1d @@ -218542,8 +218665,16 @@ that F(A') is isomorphic to B'.". Therefore, the category of sets and odubas.b $e |- B = ( Base ` O ) $. $( Base set of an order dual structure. (Contributed by Stefan O'Rear, - 29-Jan-2015.) $) + 29-Jan-2015.) (Proof shortened by AV, 12-Nov-2024.) $) odubas $p |- B = ( Base ` D ) $= + ( cbs cfv cnx cple ccnv csts co baseid plendxnbasendx necomi setsnid eqid + cop oduval fveq2i 3eqtr4i ) CFGCHIGZCIGZJZRKLZFGABFGUDUBFCMUBHFGNOPEBUEFB + UCCDUCQSTUA $. + + $( Obsolete proof of ~ odubas as of 12-Nov-2024. Base set of an order dual + structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + odubasOLD $p |- B = ( Base ` D ) $= ( cbs cfv cnx cple ccnv cop csts co baseid wne c1 cc0 cdc 1re 1lt10 mpbir ltneii basendx plendx neeq12i setsnid eqid oduval fveq2i 3eqtr4i ) CFGCHI GZCIGZJZKLMZFGABFGUMUKFCNHFGZUKOPPQRZOPUPSTUBUOPUKUPUCUDUEUAUFEBUNFBULCDU @@ -259884,8 +260015,23 @@ U C_ ( N ` { X } ) ) -> ( U = ( N ` { X } ) \/ U = { .0. } ) ) $= $( The set of scalars of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by - Thierry Arnoux, 16-Jun-2019.) $) + Thierry Arnoux, 16-Jun-2019.) (Proof shortened by AV, 12-Nov-2024.) $) srasca $p |- ( ph -> ( W |`s S ) = ( Scalar ` A ) ) $= + ( cvv wcel cress co csca cfv wceq wa cnx cop csts scaid setsnid c0 necomi + cvsca cmulr vscandxnscandx slotsdifipndx simpri eqtri ovexd setsid sylan2 + cip wne csra adantl cbs wss sraval eqtrd fveq2d 3eqtr4a wn str0 reldmress + ovprc1 adantr fv2prc sylan9eqr pm2.61ian ) DGHZADCIJZBKLZMVIANZDOKLZVJPQJ + ZKLZVNOUBLZDUCLZPQJZOUKLZVQPQJZKLZVJVKVOVRKLWAVQVPKVNRVPVMUDUASVQVSKVRRVP + VSULVMVSULUEUFSUGAVIVJGHVJVOMADCIUHGVJKGDRUIUJVLBVTKVLBCDUMLLZVTABWBMVIEU + NAVICDUOLUPWBVTMFCGDUQUJURUSUTVIVAZANZTTKLVJVKKVMRVBWCVJTMADCIVCVDVEWDBTK + AWCBWBTEDCUMVFVGUSUTVH $. + + $( Obsolete proof of ~ srasca as of 12-Nov-2024. The set of scalars of a + subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised + by Mario Carneiro, 12-Nov-2015.) (Revised by Thierry Arnoux, + 16-Jun-2019.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + srascaOLD $p |- ( ph -> ( W |`s S ) = ( Scalar ` A ) ) $= ( cvv cress co csca cfv wceq cnx cop csts scaid wne c5 c6 c0 wa cvsca cip wcel cmulr 5lt6 ltneii scandx vscandx neeq12i mpbir setsnid c8 5lt8 ipndx 5re eqtri ovexd setsid sylan2 csra adantl cbs sraval eqtrd fveq2d 3eqtr4a @@ -259898,8 +260044,23 @@ U C_ ( N ` { X } ) ) -> ( U = ( N ` { X } ) \/ U = { .0. } ) ) $= $( The scalar product operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) - (Revised by Thierry Arnoux, 16-Jun-2019.) $) + (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof shortened by AV, + 12-Nov-2024.) $) sravsca $p |- ( ph -> ( .r ` W ) = ( .s ` A ) ) $= + ( cvv wcel cmulr cfv cvsca wceq wa cnx co cop csts vscaid wne c0 csca cip + cress ovex fvex setsid mp2an slotsdifipndx simpli setsnid csra adantl cbs + eqtri wss sraval sylan2 eqtrd fveq2d eqtr4id str0 adantr fv2prc sylan9eqr + wn fvprc 3eqtr4a pm2.61ian ) DGHZADIJZBKJZLVIAMZVJDNUAJZDCUCOPZQOZNKJZVJP + QOZNUBJZVJPQOZKJZVKVJVQKJZVTVOGHVJGHVJWALDVNQUDDIUEGVJKGVORUFUGVJVRKVQRVP + VRSVMVRSUHUIUJUNVLBVSKVLBCDUKJJZVSABWBLVIEULAVICDUMJUOWBVSLFCGDUPUQURUSUT + VIVEZAMZTTKJVJVKKVPRVAWCVJTLADIVFVBWDBTKAWCBWBTEDCUKVCVDUSVGVH $. + + $( Obsolete proof of ~ sravsca as of 12-Nov-2024. The scalar product + operation of a subring algebra. (Contributed by Stefan O'Rear, + 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by + Thierry Arnoux, 16-Jun-2019.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + sravscaOLD $p |- ( ph -> ( .r ` W ) = ( .s ` A ) ) $= ( cvv wcel cmulr cfv cvsca wceq cnx co cop csts vscaid c6 c8 c0 cress cip wa csca ovex fvex setsid mp2an wne 6re ltneii vscandx ipndx neeq12i mpbir 6lt8 setsnid eqtri csra adantl cbs wss sraval sylan2 eqtrd fveq2d eqtr4id @@ -261680,8 +261841,46 @@ such that every prime ideal contains a prime element (this is a UINOUJEUMNROUNEUONPSZVESHVEVFTUPUQURUSUT $. $( The field of complex numbers is a function. (Contributed by AV, - 14-Nov-2021.) $) + 14-Nov-2021.) (Proof shortened by AV, 11-Nov-2024.) $) cnfldfun $p |- Fun CCfld $= + ( wfun cnx cfv cc cop ccj wa cdm cin c0 wceq wne fvex cnex cvv mp2an necomi + ineq12i eqtri ax-mp ccnfld cbs cplusg caddc cmulr cmul ctp cstv csn cun cts + cabs cmin ccom cmopn cple cle cunif cmetu basendxnplusgndx plusgndxnmulrndx + cds basendxnmulrndx addex mulex funtp mp3an wf wcel cjf funsn pm3.2i dmtpop + starvndxnbasendx starvndxnplusgndx starvndxnmulrndx disjtpsn slotsdifplendx + fex dmsnop funun simpri dsndxntsetndx slotsdifdsndx ctsr letsr elexi cr cxp + absf subf xpex w3a slotsdifunifndx unifndxntsetndx a1i anim1i 3anass sylibr + coex tsetndxnbasendx tsetndxnmulrndx 3pm3.2i plendxnbasendx plendxnplusgndx + tsetndxnplusgndx plendxnmulrndx dsndxnbasendx dsndxnmulrndx unifndxnbasendx + dmun dsndxnplusgndx disjtp2 3simpa sylanbrc adantr undisj2 tsetndxnstarvndx + mpbi necom biimpi ineqcomi simpl3 disjsn2 undisj1 df-cnfld funeqi mpbir ) U + AABUBCZDEBUCCZUDEBUECZUFEUGZBUHCZFEUIZUJZBUKCZULUMUNZUOCZEBUPCZUQEBVBCZYQEU + GZBURCZYQUSCZEUIZUJZUJZAZYOAZUUEAZGYOHZUUEHZIZJKUUGUUHUUIYLAZYNAZGYLHZYNHZI + ZJKUUHUUMUUNYIYJLYIYKLYJYKLUUMUTVCVAYIYJYKDUDUFBUBMBUCMBUEMNVDVEVFVGYMFBUHM + DDFVHDOVIZFOVIVJNDDOFVSPZVKVLUUQYIYJYKUGZYMUIZIZJUUOUUTUUPUVAYIDYJUDYKUFNVD + VEVMZYMFUUSVTZRYIYMLYJYMLYKYMLUVBJKYMYIVNQYMYJVOQYMYKVPQYIYJYKYMVQVGSYLYNWA + PUUAAZUUDAZGUUAHZUUDHZIZJKUUIUVEUVFYPYSLZYPYTLYSYTLZUVEYMYSLZUVJVRWBYTYPWCQ + YMYTLZUVKWDWBYPYSYTYRUQYQBUKMBUPMBVBMYQUOMZUQWEWFWGZULUMDWHULVHUURULOVIWJND + WHOULVSPDDWIZDUMVHUVPOVIUMOVIWKDDNNWLUVPDOUMVSPWTZVFVGUUBUUCBURMYQUSMZVKVLU + VIYPYSYTUGZUUBUIZIZJUVGUVSUVHUVTYPYRYSUQYTYQUVNUVOUVQVMZUUBUUCUVRVTZRYPUUBL + ZYSUUBLZYTUUBLZWMZUWAJKYJUUBLZYKUUBLZYMUUBLZWMZUWEUWFGZGZUWGWNUWMUWDUWLGUWG + UWKUWDUWLUWDUWKUUBYPWOQWPWQUWDUWEUWFWRWSTYPYSYTUUBVQTSUUAUUDWAPVLUULUUOUUPU + JZUVGUVHUJZIZJUUJUWNUUKUWOYLYNXKUUAUUDXKRUUOUWOIJKZUUPUWOIJKZGUWPJKUWQUWRUU + OUVGIZJKZUUOUVHIZJKZGUWQUWTUXBUWSUUTUVSIZJUUOUUTUVGUVSUVCUWBRYIYPLZYJYPLZYK + YPLZWMYIYSLZYJYSLZYKYSLZWMYIYTLZYJYTLZYKYTLZWMUXCJKUXDUXEUXFYPYIXAQYPYJXFQY + PYKXBQXCUXGUXHUXIYSYIXDQYSYJXEQYSYKXGQXCUXJUXKUXLYTYIXHQYTYJXLQYTYKXIQXCYIY + JYKYPYSYTXMVGSUXAUUTUVTIZJUUOUUTUVHUVTUVCUWCRYIUUBLZUWHUWIWMZUXMJKUWMUXOWNU + WKUXOUWLUWKUXNUWHUWIGUXOUXNUWKUUBYIXJQWPUWHUWIUWJXNUXNUWHUWIWRXOXPTYIYJYKUU + BVQTSVLUUOUVGUVHXQXSUUPUVGIZJKZUUPUVHIZJKZGUWRUXQUXSUXPUVAUVSIJUUPUVAUVGUVS + UVDUWBRUVSUVAJYPYMLYSYMLZYTYMLZUVSUVAIJKXRUVLUVJGUXTVRUVLUXTUVJUVLUXTYMYSXT + YAXPTUVMUVKGUYAWDUVMUYAUVKUVMUYAYMYTXTYAXPTYPYSYTYMVQVGYBSUXRUVAUVTIZJUUPUV + AUVHUVTUVDUWCRUWJUYBJKUWMUWJWNUWHUWIUWJUWLYCTYMUUBYDTSVLUUPUVGUVHXQXSVLUUOU + UPUWOYEXSSYOUUEWAPUAUUFYFYGYH $. + + $( Obsolete proof of ~ cnfldfun as of 10-Nov-2024. The field of complex + numbers is a function. (Contributed by AV, 14-Nov-2021.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + cnfldfunOLD $p |- Fun CCfld $= ( wfun cnx cfv cc cin c0 wceq wne fvex c1 c4 ltneii neeqtrri eqnetri c2 1nn c3 c9 2nn0 decltdi ccnfld cbs cop caddc cmulr cmul ctp cstv ccj csn cun cts cplusg cabs cmin ccom cmopn cple cle cds cunif cmetu wa cdm basendxnmulrndx @@ -265829,8 +266028,20 @@ S C_ ( ._|_ ` ( ._|_ ` S ) ) ) $= ${ thlbas.c $e |- C = ( ClSubSp ` W ) $. $( Base set of the Hilbert lattice of closed subspaces. (Contributed by - Mario Carneiro, 25-Oct-2015.) $) + Mario Carneiro, 25-Oct-2015.) (Proof shortened by AV, + 11-Nov-2024.) $) thlbas $p |- C = ( Base ` K ) $= + ( cvv wcel cbs cfv wceq cipo cnx coc ccss eqid fveq2d fvprc eqtrid cthl + c0 cocv cop csts fvexi ipobas ax-mp baseid basendxnocndx setsnid thlval + co eqtri eqtr4id wn base0 3eqtr4a pm2.61i ) CFGZABHIZJURAAKIZLMIZCUAIZU + BUCUKZHIZUSAUTHIZVDAFGAVEJACNEUDAUTFUTOZUEUFVBVAHUTUGUHUIULURBVCHAUTBVB + FCDEVFVBOUJPUMURUNZTTHIAUSUOVGACNITECNQRVGBTHVGBCSITDCSQRPUPUQ $. + + $( Obsolete proof of ~ thlbas as of 11-Nov-2024. Base set of the Hilbert + lattice of closed subspaces. (Contributed by Mario Carneiro, + 25-Oct-2015.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + thlbasOLD $p |- C = ( Base ` K ) $= ( cvv wcel cbs cfv wceq cnx ccss eqid wne c1 1nn0 fveq2d fvprc eqtrid c0 cipo coc cocv cop csts co fvexi ipobas ax-mp baseid cdc 1lt10 declti 1re 1nn ltneii basendx ocndx neeq12i mpbir setsnid eqtri thlval eqtr4id @@ -265843,8 +266054,24 @@ S C_ ( ._|_ ` ( ._|_ ` S ) ) ) $= thlle.i $e |- I = ( toInc ` C ) $. thlle.l $e |- .<_ = ( le ` I ) $. $( Ordering on the Hilbert lattice of closed subspaces. (Contributed - by Mario Carneiro, 25-Oct-2015.) $) + by Mario Carneiro, 25-Oct-2015.) (Proof shortened by AV, + 11-Nov-2024.) $) thlle $p |- .<_ = ( le ` K ) $= + ( vx vy cvv wcel cple cfv wceq cnx pleid c0 ccss coc cocv cop csts co + plendxnocndx setsnid eqtri eqid thlval fveq2d eqtr4id wn str0 cpr wss + cv wa copab fvexi ipolerval ax-mp eqtr4i wne wex opabn0 elfvex eleq2s + vex prss ad2antrr sylanbr exlimivv sylbi necon1bi eqtrid cthl 3eqtr4a + fvprc pm2.61i ) ELMZDCNOZPWADBQUAOZEUBOZUCUDUEZNOZWBDBNOZWFIWDWCNBRUF + UGUHWACWENABCWDLEFGHWDUIUJUKULWAUMZSSNODWBNQNORUNWHDJUQZKUQZUOAUPZWIW + JUPZURZJKUSZSDWGWNIALMWNWGPAETGUTJKABLHVAVBVCWAWNSWNSVDWMKVEJVEWAWMJK + VFWMWAJKWKWIAMZWJAMZURWLWAWIWJAJVIKVIVJWOWAWPWLWAWIETOAWIETVGGVHVKVLV + MVNVOVPWHCSNWHCEVQOSFEVQVSVPUKVRVT $. + + $( Obsolete proof of ~ thlle as of 11-Nov-2024. Ordering on the + Hilbert lattice of closed subspaces. (Contributed by Mario + Carneiro, 25-Oct-2015.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + thlleOLD $p |- .<_ = ( le ` K ) $= ( vx vy cvv wcel cple cfv wceq wne c1 c0 ccss cnx coc cocv csts pleid cop cc0 cdc 10re 1nn0 0nn0 1nn 0lt1 declt ltneii plendx ocndx neeq12i co mpbir setsnid eqtri eqid thlval fveq2d eqtr4id wn cv cpr wss copab @@ -278983,17 +279210,38 @@ represented as an element of (the base set of) ` ( ( 1 ... n ) Mat R ) ` . ZKLAKLUIUHKCTUBUAUGAUJKABUICDEFGUIUCUDUEUF $. $( The matrix ring has the same scalars as its underlying linear structure. - (Contributed by Stefan O'Rear, 4-Sep-2015.) $) + (Contributed by Stefan O'Rear, 4-Sep-2015.) (Proof shortened by AV, + 12-Nov-2024.) $) matsca $p |- ( ( N e. Fin /\ R e. V ) -> ( Scalar ` G ) = ( Scalar ` A ) ) $= + ( cfn wcel wa csca cfv cnx cmulr cotp cmmul co cop csts scaid eqid matval + scandxnmulrndx setsnid fveq2d eqtr4id ) DHIBEIJZCKLCMNLZBDDDOPQZRSQZKLAKL + UIUHKCTUCUDUGAUJKABUICDEFGUIUAUBUEUF $. + + $( Obsolete proof of ~ matsca as of 12-Nov-2024. The matrix ring has the + same scalars as its underlying linear structure. (Contributed by Stefan + O'Rear, 4-Sep-2015.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + matscaOLD $p |- ( ( N e. Fin /\ R e. V ) -> + ( Scalar ` G ) = ( Scalar ` A ) ) $= ( cfn wcel wa csca cfv cnx cmulr cotp cmmul co wne c5 c3 cop scaid gtneii csts 3lt5 scandx mulrndx neeq12i mpbir setsnid eqid matval fveq2d eqtr4id 3re ) DHIBEIJZCKLCMNLZBDDDOPQZUAUDQZKLAKLURUQKCUBMKLZUQRSTRTSUOUEUCUTSUQT UFUGUHUIUJUPAUSKABURCDEFGURUKULUMUN $. $( The matrix ring has the same scalar multiplication as its underlying - linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.) $) + linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.) (Proof + shortened by AV, 12-Nov-2024.) $) matvsca $p |- ( ( N e. Fin /\ R e. V ) -> ( .s ` G ) = ( .s ` A ) ) $= + ( cfn wcel wa cvsca cfv cnx cmulr cotp cmmul co cop csts vscaid setsnid + vscandxnmulrndx eqid matval fveq2d eqtr4id ) DHIBEIJZCKLCMNLZBDDDOPQZRSQZ + KLAKLUIUHKCTUBUAUGAUJKABUICDEFGUIUCUDUEUF $. + + $( Obsolete proof of ~ matvsca as of 12-Nov-2024. The matrix ring has the + same scalar multiplication as its underlying linear structure. + (Contributed by Stefan O'Rear, 4-Sep-2015.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + matvscaOLD $p |- ( ( N e. Fin /\ R e. V ) -> ( .s ` G ) = ( .s ` A ) ) $= ( cfn wcel wa cvsca cfv cnx cmulr cotp cmmul co cop c6 c3 csts vscaid 3re vscandx 3lt6 gtneii mulrndx neeqtrri eqnetri setsnid eqid matval eqtr4id fveq2d ) DHIBEIJZCKLCMNLZBDDDOPQZRUAQZKLAKLUQUPKCUBMKLSUPUDSTUPTSUCUEUFUG @@ -318434,15 +318682,30 @@ the base set to the (extended) reals and which is nonnegative, symmetric setsms.k $e |- ( ph -> K = ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) ) $. $( The base set of a constructed metric space. (Contributed by Mario - Carneiro, 28-Aug-2015.) $) + Carneiro, 28-Aug-2015.) (Proof shortened by AV, 12-Nov-2024.) $) setsmsbas $p |- ( ph -> X = ( Base ` K ) ) $= + ( cbs cfv cnx cts cmopn cop csts co baseid tsetndxnbasendx necomi setsnid + fveq2d 3eqtr4a ) ADIJDKLJZBMJZNOPZIJECIJUDUCIDQUCKIJRSTFACUEIHUAUB $. + + $( Obsolete proof of ~ setsmsbas as of 12-Nov-2024. The base set of a + constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + setsmsbasOLD $p |- ( ph -> X = ( Base ` K ) ) $= ( cbs cfv cnx cts cmopn cop csts co baseid wne c1 c9 1lt9 basendx tsetndx 1re ltneii neeq12i mpbir setsnid fveq2d 3eqtr4a ) ADIJDKLJZBMJZNOPZIJECIJ ULUKIDQKIJZUKRSTRSTUDUAUEUNSUKTUBUCUFUGUHFACUMIHUIUJ $. $( The distance function of a constructed metric space. (Contributed by - Mario Carneiro, 28-Aug-2015.) $) + Mario Carneiro, 28-Aug-2015.) (Proof shortened by AV, 11-Nov-2024.) $) setsmsds $p |- ( ph -> ( dist ` M ) = ( dist ` K ) ) $= + ( cds cfv cnx cts cmopn cop csts co dsid dsndxntsetndx setsnid fveq2d + eqtr4id ) ADIJDKLJZBMJZNOPZIJCIJUCUBIDQRSACUDIHTUA $. + + $( Obsolete proof of ~ setsmsds as of 11-Nov-2024. The distance function + of a constructed metric space. (Contributed by Mario Carneiro, + 28-Aug-2015.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + setsmsdsOLD $p |- ( ph -> ( dist ` M ) = ( dist ` K ) ) $= ( cds cfv cnx cts cmopn cop csts co wne c1 c2 c9 dsid cdc 2nn0 9nn0 9lt10 9re 1nn declti gtneii dsndx tsetndx neeq12i mpbir setsnid fveq2d eqtr4id ) ADIJDKLJZBMJZNOPZIJCIJURUQIDUAKIJZUQQRSUBZTQTVAUFRSTUGUCUDUEUHUIUTVAUQT @@ -395972,12 +396235,12 @@ The second section ("Tarskian geometry") develops the synthetic treatment of df-lng $a |- LineG = Slot ; 1 7 $. $( Index value of the Interval (segment) slot. Use ~ ndxarg . (Contributed - by Thierry Arnoux, 24-Aug-2017.) $) + by Thierry Arnoux, 24-Aug-2017.) (New usage is discouraged.) $) itvndx $p |- ( Itv ` ndx ) = ; 1 6 $= ( citv c1 c6 cdc df-itv 1nn0 6nn decnncl ndxarg ) ABCDEBCFGHI $. $( Index value of the "line" slot. Use ~ ndxarg . (Contributed by Thierry - Arnoux, 27-Mar-2019.) $) + Arnoux, 27-Mar-2019.) (New usage is discouraged.) $) lngndx $p |- ( LineG ` ndx ) = ; 1 7 $= ( clng c1 c7 cdc df-lng 1nn0 7nn decnncl ndxarg ) ABCDEBCFGHI $. @@ -396019,6 +396282,14 @@ The second section ("Tarskian geometry") develops the synthetic treatment of BVKVEIVKQVEQVKUJFGQJKRUGMNUHOPSVHVJVBVKVGIVKTVGTVKUKFGTJKULUMMNUNOPVBVKVIIV KFQHZVIVLVKVLFQLUOUPUQFQGLRURUSUTNVAOPSS $. + $( The slot for the line is not the slot for the Interval (segment) in an + extensible structure. Formerly part of proof for ~ ttgval . (Contributed + by AV, 9-Nov-2024.) $) + lngndxnitvndx $p |- ( LineG ` ndx ) =/= ( Itv ` ndx ) $= + ( cnx clng cfv citv wne c1 c7 cdc c6 1nn0 6nn decnncl nnrei 6nn0 6lt7 declt + 7nn gtneii lngndx itvndx neeq12i mpbir ) ABCZADCZEFGHZFIHZEUFUEUFFIJKLMFIGJ + NQOPRUCUEUDUFSTUAUB $. + ${ trkgstr.w $e |- W = { <. ( Base ` ndx ) , U >. , <. ( dist ` ndx ) , D >. , <. ( Itv ` ndx ) , I >. } $. @@ -405487,7 +405758,7 @@ and angles (6 parts). This is often the actual textbook definition of ttgval.i $e |- I = ( Itv ` G ) $. $( Define a function to augment a subcomplex Hilbert space with betweenness and a line definition. (Contributed by Thierry Arnoux, - 25-Mar-2019.) $) + 25-Mar-2019.) (Proof shortened by AV, 9-Nov-2024.) $) ttgval $p |- ( H e. V -> ( G = ( ( H sSet <. ( Itv ` ndx ) , ( x e. B , y e. B |-> { z e. B | E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) >. ) @@ -405497,6 +405768,49 @@ and angles (6 parts). This is often the actual textbook definition of E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) ) ) $= ( wcel co wceq csts vi vw va vb vc cnx citv cfv cc0 cicc wrex crab cmpo cv cop clng w3o cttg csb a1i cvv elex cbs csg cvsca fveq2 eqtr4di oveqd + c1 oveq123d eqeq12d rexbidv rabeqbidv mpoeq123dv rabeqdv opeq2d oveq12d + eqidd oveq1 csbeq12dv df-ttg csbex fvmpt syl fvexi mpoex wa simpr oveq2 + ovex oveq2d rabbidv eqeq2d eqeq1d cbvrabv eqtrdi eleq2d mpoeq3dv syldan + cbvmpov 3orbi123d csbied 3eqtrd fveq2d itvid lngndxnitvndx necomi mpan2 + setsnid setsid 3eqtr4d eqtr4d jca ) HKQZGHUFUGUHZABDDCUNZAUNZJRZFUNZBUN + ZXQJRZERZSZFUIVIUJRZUKZCDULZUMZUOZTRZUFUPUHZABDDXPXQXTIRZQZXQXPXTIRZQZX + TXQXPIRZQZUQZCDULZUMZUOZTRZSIYGSXNGYIYJABDDXPXQXTYGRZQZXQXPXTYGRZQZXTXQ + XPYGRZQZUQZCDULZUMZUOZTRZUUAXNGHURUHZUAYGHXOUAUNZUOZTRZYJABDDXPXQXTUUNR + ZQZXQXPXTUUNRZQZXTXQXPUUNRZQZUQZCDULZUMZUOZTRZUSZUULGUUMSXNLUTXNHVAQUUM + UVHSHKVBUBHUAABUBUNZVCUHZUVJXPXQUVIVDUHZRZXSXTXQUVKRZUVIVEUHZRZSZFYDUKZ + CUVJULZUMZUVIUUOTRZYJABUVJUVJUVCCUVJULZUMZUOZTRZUSUVHVAURUVIHSZUAUVSUWD + YGUVGUWEABUVJUVJUVRDDYFUWEUVJHVCUHDUVIHVCVFMVGZUWFUWEUVQYECUVJDUWFUWEUV + PYCFYDUWEUVLXRUVOYBUWEUVKJXPXQUWEUVKHVDUHJUVIHVDVFNVGZVHUWEXSXSUVMYAUVN + EUWEUVNHVEUHEUVIHVEVFOVGUWEXSVRUWEUVKJXTXQUWGVHVJVKVLVMVNUWEUVTUUPUWCUV + FTUVIHUUOTVSUWEUWBUVEYJUWEABUVJUVJUWADDUVDUWFUWFUWEUVCCUVJDUWFVOVNVPVQV + TABCUBUAFWAUAYGUVGUUPUVFTWJWBWCWDXNUAYGUVGUULVAYGVAQZXNABDDYFDHVCMWEZUW + IWFZUTXNUUNYGSZUUNUCUDDDUEUNZUCUNZJRZXSUDUNZUWMJRZERZSZFYDUKZUEDULZUMZS + ZUVGUULSXNUWKWGUUNYGUXAXNUWKWHUCUDABDDUWTYFUWLXQJRZXSUWOXQJRZERZSZFYDUK + ZUEDULZUWMXQSZUWSUXGUEDUXIUWRUXFFYDUXIUWNUXCUWQUXEUWMXQUWLJWIUXIUWPUXDX + SEUWMXQUWOJWIWKVKVLWLUWOXTSZUXHUXCYBSZFYDUKZUEDULYFUXJUXGUXLUEDUXJUXFUX + KFYDUXJUXEYBUXCUXJUXDYAXSEUWOXTXQJVSWKWMVLWLUXLYEUECDUWLXPSZUXKYCFYDUXM + UXCXRYBUWLXPXQJVSWNVLWOWPWTZVGXNUXBWGZUUPYIUVFUUKTUXOUUOYHHTUXOUUNYGXOU + XOUUNUXAYGXNUXBWHUXNWPZVPWKUXOUVEUUJYJUXOABDDUVDUUIUXOUVCUUHCDUXOUURUUC + UUTUUEUVBUUGUXOUUQUUBXPUXOUUNYGXQXTUXPVHWQUXOUUSUUDXQUXOUUNYGXPXTUXPVHW + QUXOUVAUUFXTUXOUUNYGXQXPUXPVHWQXAWLWRVPVQWSXBXCZXNYTUUKYITXNYSUUJYJXNAB + DDYRUUIXNYQUUHCDXNYLUUCYNUUEYPUUGXNYKUUBXPXNIYGXQXTXNGUGUHZYIUGUHZIYGXN + UXRUULUGUHUXSXNGUULUGUXQXDUUJYJUGYIXEYJXOXFXGXIVGIUXRSXNPUTXNUWHYGUXSSU + WJKYGUGVAHXEXJXHXKZVHWQXNYMUUDXQXNIYGXPXTUXTVHWQXNYOUUFXTXNIYGXQXPUXTVH + WQXAWLWRVPWKXLUXTXM $. + + $( Obsolete proof of ~ ttgval as of 9-Nov-2024. Define a function to + augment a subcomplex Hilbert space with betweenness and a line + definition. (Contributed by Thierry Arnoux, 25-Mar-2019.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + ttgvalOLD $p |- ( H e. V -> ( G = ( ( H sSet <. ( Itv ` ndx ) , + ( x e. B , y e. B |-> { z e. B | + E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) >. ) + sSet <. ( LineG ` ndx ) , ( x e. B , y e. B |-> { z e. B | + ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) >. ) + /\ I = ( x e. B , y e. B |-> { z e. B | + E. k e. ( 0 [,] 1 ) ( z .- x ) = ( k .x. ( y .- x ) ) } ) ) ) $= + ( wcel co wceq csts vi vw va vb vc cnx citv cfv cc0 cicc wrex crab cmpo + cv cop clng w3o cttg csb a1i cvv elex cbs csg cvsca fveq2 eqtr4di oveqd c1 oveq123d eqeq12d rexbidv rabeqbidv mpoeq123dv csbeq1d rabeqdv opeq2d eqidd oveq1 oveq12d csbeq2dv eqtrd df-ttg ovex csbex fvmpt syl fvexi wa mpoex simpr oveq2 oveq2d rabbidv eqeq2d eqeq1d cbvrabv eqtrdi 3orbi123d @@ -409986,12 +410300,12 @@ otherwise it could not be used in an extensible structure (slots must be $( The index value of the ` Base ` slot is less than the index value of the ` .ef ` slot. (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 30-Oct-2024.) $) - baseltedgf $p |- ( Base ` ndx ) < ( .ef ` ndx ) $= + basendxltedgfndx $p |- ( Base ` ndx ) < ( .ef ` ndx ) $= ( c1 cdc cnx cbs cfv cedgf clt 1nn 8nn0 1nn0 declti basendx edgfndx 3brtr4i c8 1lt10 ) AAOBCDECFEGAOAHIJPKLMN $. - $( Obsolete proof of ~ baseltedgf as of 30-Oct-2024. The index value of the - ` Base ` slot is less than the index value of the ` .ef ` slot. + $( Obsolete proof of ~ basendxltedgfndx as of 30-Oct-2024. The index value + of the ` Base ` slot is less than the index value of the ` .ef ` slot. (Contributed by AV, 21-Sep-2020.) (Proof modification is discouraged.) (New usage is discouraged.) $) baseltedgfOLD $p |- ( Base ` ndx ) < ( .ef ` ndx ) $= @@ -410001,7 +410315,8 @@ otherwise it could not be used in an extensible structure (slots must be $( The slots ` Base ` and ` .ef ` are different. (Contributed by AV, 21-Sep-2020.) $) basendxnedgfndx $p |- ( Base ` ndx ) =/= ( .ef ` ndx ) $= - ( cnx cbs cfv cedgf basendxnn nnrei baseltedgf ltneii ) ABCZADCIEFGH $. + ( cnx cbs cfv cedgf basendxnn nnrei basendxltedgfndx ltneii ) ABCZADCIEFGH + $. $( @@ -410415,13 +410730,13 @@ class is an extensible structure (containing a slot for "edge functions") and indexed edges is actually an extensible structure. (Contributed by AV, 23-Nov-2020.) $) struct2grstr $p |- G Struct <. ( Base ` ndx ) , ( .ef ` ndx ) >. $= - ( cnx cedgf cfv baseltedgf edgfndxnn 2strstr1 ) CABEFGDHIJ $. + ( cnx cedgf cfv basendxltedgfndx edgfndxnn 2strstr1 ) CABEFGDHIJ $. $( The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 23-Sep-2020.) $) struct2grvtx $p |- ( ( V e. X /\ E e. Y ) -> ( Vtx ` G ) = V ) $= - ( cnx cedgf cfv edgfndxnn baseltedgf structvtxval ) GHIABCDEJKFL $. + ( cnx cedgf cfv edgfndxnn basendxltedgfndx structvtxval ) GHIABCDEJKFL $. $( The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by @@ -491981,8 +492296,17 @@ closed sets (see for example ~ zarcls0 for the definition of ` V ` ). ${ zlmds.1 $e |- D = ( dist ` G ) $. $( Distance in a ` ZZ ` -module (if present). (Contributed by Thierry - Arnoux, 8-Nov-2017.) $) + Arnoux, 8-Nov-2017.) (Proof shortened by AV, 11-Nov-2024.) $) zlmds $p |- ( G e. V -> D = ( dist ` W ) ) $= + ( wcel cds cfv cnx csca czring cop csts co dsid wne slotsdnscsi setsnid + cvsca cmg eqid zlmval fveq2d cip simp1i simp2i eqtri eqtr4di eqtr4id ) + BCGZABHIZDHIZFUKUMBJKIZLMNOZJTIZBUAIZMNOZHIZULUKDURHUQBCDEUQUBUCUDULUOH + IUSLUNHBPJHIZUNQZUTUPQZUTJUEIQZRUFSUQUPHUOPVAVBVCRUGSUHUIUJ $. + + $( Obsolete proof of ~ zlmds as of 11-Nov-2024. Distance in a ` ZZ ` + -module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + zlmdsOLD $p |- ( G e. V -> D = ( dist ` W ) ) $= ( cds cfv cnx czring cop csts co dsid wne c1 c2 c5 1nn c6 wcel csca cmg cvsca eqid zlmval fveq2d cdc 2nn0 5nn0 5lt10 declti gtneii dsndx scandx 5re neeq12i mpbir setsnid 6re 6nn0 6lt10 vscandx eqtri eqtr4di eqtr4id @@ -491994,8 +492318,17 @@ closed sets (see for example ~ zarcls0 for the definition of ` V ` ). ${ zlmtset.1 $e |- J = ( TopSet ` G ) $. $( Topology in a ` ZZ ` -module (if present). (Contributed by Thierry - Arnoux, 8-Nov-2017.) $) + Arnoux, 8-Nov-2017.) (Proof shortened by AV, 12-Nov-2024.) $) zlmtset $p |- ( G e. V -> J = ( TopSet ` W ) ) $= + ( wcel cnx csca cfv czring cop csts co cvsca cts tsetid wne slotstnscsi + setsnid cmg cip simp1i simp2i 3eqtri eqid zlmval fveq2d eqtr4id ) ACGZB + AHIJZKLMNZHOJZAUAJZLMNZPJZDPJBAPJULPJUPFKUKPAQHPJZUKRZUQUMRZUQHUBJRZSUC + TUNUMPULQURUSUTSUDTUEUJDUOPUNACDEUNUFUGUHUI $. + + $( Obsolete proof of ~ zlmtset as of 11-Nov-2024. Topology in a ` ZZ ` + -module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + zlmtsetOLD $p |- ( G e. V -> J = ( TopSet ` W ) ) $= ( cnx cfv czring cop csts co cts tsetid wne c9 c5 gtneii tsetndx c6 cmg wcel csca cvsca 5re 5lt9 scandx neeq12i setsnid 6re 6lt9 vscandx 3eqtri mpbir eqid zlmval fveq2d eqtr4id ) ACUBZBAGUCHZIJKLZGUDHZAUAHZJKLZMHZDM @@ -785864,8 +786197,17 @@ mean the category of preordered sets (classes). However, "ProsetToCat" ${ prstcle.l $e |- ( ph -> .<_ = ( le ` K ) ) $. $( Value of the less-than-or-equal-to relation is unchanged. - (Contributed by Zhi Wang, 20-Sep-2024.) $) + (Contributed by Zhi Wang, 20-Sep-2024.) (Proof shortened by AV, + 12-Nov-2024.) $) prstcleval $p |- ( ph -> .<_ = ( le ` C ) ) $= + ( cple cfv pleid cnx cco wne chom slotsdifplendx2 simpli prstcnid eqtrd + simpri ) ADCHIBHIGABHCEFJKHIZKLIMZTKNIMZOPUAUBOSQR $. + + $( Obsolete proof of ~ prstcleval as of 12-Nov-2024. Value of the + less-than-or-equal-to relation is unchanged. (Contributed by Zhi + Wang, 20-Sep-2024.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + prstclevalOLD $p |- ( ph -> .<_ = ( le ` C ) ) $= ( cple cfv cnx wne c1 cc0 cdc c5 10re 1nn0 0nn0 5nn c4 pleid cco nngt0i declt ltneii plendx ccondx neeq12i mpbir chom 4nn homndx prstcnid eqtrd ) ADCHIBHIGABHCEFUAJHIZJUBIZKLMNZLONZKUQURPLMOQRSOSUCUDUEUOUQUPURUFUGUH @@ -785880,8 +786222,16 @@ mean the category of preordered sets (classes). However, "ProsetToCat" ${ prstcoc.oc $e |- ( ph -> ._|_ = ( oc ` K ) ) $. $( Orthocomplementation is unchanged. (Contributed by Zhi Wang, - 20-Sep-2024.) $) + 20-Sep-2024.) (Proof shortened by AV, 12-Nov-2024.) $) prstcocval $p |- ( ph -> ._|_ = ( oc ` C ) ) $= + ( coc cfv ocid cnx cco chom slotsdifocndx simpli simpri prstcnid eqtrd + wne ) ADCHIBHIGABHCEFJKHIZKLISZTKMISZNOUAUBNPQR $. + + $( Obsolete proof of ~ prstcocval as of 12-Nov-2024. + Orthocomplementation is unchanged. (Contributed by Zhi Wang, + 20-Sep-2024.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + prstcocvalOLD $p |- ( ph -> ._|_ = ( oc ` C ) ) $= ( coc cfv cnx wne c1 cdc c5 1nn0 declt ltneii ocndx neeq12i mpbir deccl ocid cco nn0rei 5nn 1lt5 ccondx chom c4 4nn 1lt4 homndx prstcnid eqtrd ) ADCHIBHIGABHCEFUBJHIZJUCIZKLLMZLNMZKUQURUQLLOOUAUDZLLNOOUEUFPQUOUQUPU