Skip to content

Commit

Permalink
Comments on extensible structures
Browse files Browse the repository at this point in the history 
* header comment for section "7.1.1  Basic definitions" revised (header comment for section "7.1.1.4  Structure component indices" referenced instead of comment for ~ basendx)
* header comment for section "7.1.1.3  Slots" revised
* header comment for section "7.1.1.4  Structure component indices" added
* comment for ~ basendx revised.
* proofs of theorems cnfldfun and cnfldfunALT switched
  • Loading branch information
@avekens
avekens committed Nov 24, 2024
1 parent 36f24be commit 593e66d
Show file tree
Hide file tree
Showing 2 changed files with 116 additions and 64 deletions.
24 changes: 12 additions & 12 deletions discouraged
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1683,7 +1683,7 @@
"basendx" is used by "basendxnn".
"basendx" is used by "basendxnocndx".
"basendx" is used by "catstr".
"basendx" is used by "cnfldfunOLD".
"basendx" is used by "cnfldfunALTOLD".
"basendx" is used by "eengstr".
"basendx" is used by "grpbasex".
"basendx" is used by "grpplusgx".
Expand Down Expand Up @@ -4737,7 +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 "cnfldfunALTOLD".
"df-cnfld" is used by "cnfldle".
"df-cnfld" is used by "cnfldmul".
"df-cnfld" is used by "cnfldstr".
Expand Down Expand Up @@ -5568,7 +5568,7 @@
"drsb1" is used by "sb2ae".
"drsb1" is used by "sbco3".
"dsndx" is used by "basendxltdsndx".
"dsndx" is used by "cnfldfunOLD".
"dsndx" is used by "cnfldfunALTOLD".
"dsndx" is used by "cnfldstr".
"dsndx" is used by "dsndxnmulrndx".
"dsndx" is used by "dsndxnn".
Expand Down Expand Up @@ -10130,7 +10130,7 @@
"mulresr" is used by "axrrecex".
"mulrndx" is used by "basendxnmulrndx".
"mulrndx" is used by "basendxnmulrndxOLD".
"mulrndx" is used by "cnfldfunOLD".
"mulrndx" is used by "cnfldfunALTOLD".
"mulrndx" is used by "dsndxnmulrndx".
"mulrndx" is used by "ipndxnmulrndx".
"mulrndx" is used by "matscaOLD".
Expand Down Expand Up @@ -12155,7 +12155,7 @@
"pl42lem3N" is used by "pl42lem4N".
"pl42lem4N" is used by "pl42N".
"plendx" is used by "basendxltplendx".
"plendx" is used by "cnfldfunOLD".
"plendx" is used by "cnfldfunALTOLD".
"plendx" is used by "cnfldstr".
"plendx" is used by "idlsrgstr".
"plendx" is used by "imasvalstr".
Expand All @@ -12180,7 +12180,7 @@
"plpv" is used by "addcompr".
"plusgndx" is used by "basendxltplusgndx".
"plusgndx" is used by "basendxnplusgndxOLD".
"plusgndx" is used by "cnfldfunOLD".
"plusgndx" is used by "cnfldfunALTOLD".
"plusgndx" is used by "dsndxnplusgndx".
"plusgndx" is used by "grpbasex".
"plusgndx" is used by "grpplusgx".
Expand Down Expand Up @@ -13530,7 +13530,7 @@
"ssralv2" is used by "ordelordALTVD".
"st0" is used by "largei".
"stadd3i" is used by "golem2".
"starvndx" is used by "cnfldfunOLD".
"starvndx" is used by "cnfldfunALTOLD".
"starvndx" is used by "hlhilslemOLD".
"starvndx" is used by "slotsdifdsndx".
"starvndx" is used by "slotsdifplendx".
Expand Down Expand Up @@ -13689,7 +13689,7 @@
"trsbc" is used by "truniALT".
"trsbc" is used by "truniALTVD".
"tsetndx" is used by "basendxlttsetndx".
"tsetndx" is used by "cnfldfunOLD".
"tsetndx" is used by "cnfldfunALTOLD".
"tsetndx" is used by "cnfldstr".
"tsetndx" is used by "dsndxntsetndx".
"tsetndx" is used by "idlsrgstr".
Expand Down Expand Up @@ -13725,7 +13725,7 @@
"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 "cnfldfunALTOLD".
"unifndx" is used by "cnfldstr".
"unifndx" is used by "slotsdifunifndx".
"unifndx" is used by "tuslemOLD".
Expand Down Expand Up @@ -15725,7 +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 "cnfldfunALTOLD" 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).
Expand Down Expand Up @@ -20017,8 +20017,8 @@ Proof modification of "cnaddabloOLD" is discouraged (65 steps).
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 "cnfldfunALT" is discouraged (768 steps).
Proof modification of "cnfldfunALTOLD" 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).
Expand Down
156 changes: 104 additions & 52 deletions set.mm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -200055,8 +200055,9 @@ on a finite (and not necessarily sequential) subset of ` NN ` . The
~ ndxid , we can refer to a specific poset with base set ` B ` and order
relation ` L ` using the extensible structure
` { <. ( Base `` ndx ) , B >. , <. ( le `` ndx ) , L >. } ` rather than
` { <. 1 , B >. , <. ; 1 0 , L >. } ` . See the comment of ~ basendx for
more details on numeric indices versus the structure component extractors.
` { <. 1 , B >. , <. ; 1 0 , L >. } ` . See section header comment
~ mmtheorems.html#cnx for more details on numeric indices versus the
structure component extractors.

There are many other possible ways to handle structures. We chose this
extensible structure approach because this approach (1) results in simpler
Expand Down Expand Up @@ -200611,17 +200612,39 @@ as a partially ordered set ( ~ df-poset ) or a group ( ~ df-grp )).

Note that ` Slot A ` is implemented as "evaluation at ` A ` ". That is,
` ( Slot A `` S ) ` is defined to be ` ( S `` A ) ` , where ` A ` will
typically be a small nonzero natural number. Each extensible structure
` S ` is a function defined on specific natural number "slots", and this
function extracts the value at a particular slot.
typically be an index (which is implemented as a small natural number)
of a component of an extensible structure ` S ` . Each extensible
structure is a function defined on specific (natural number) "slots",
and the function ` Slot A ` extracts the structure's component as a
function value at a particular slot (with index ` A ` ).

The special "structure" ` ndx ` , defined as the identity function
restricted to ` NN ` , can be used to extract the number ` A ` from a
slot, since ` ( Slot A `` ndx ) = A ` (see ~ ndxarg ). This is
typically used to refer to the number of a slot when defining structures
without having to expose the detail of what that number is (for
instance, we use the expression ` ( Base `` ndx ) ` in theorems and
proofs instead of its value 1).
proofs instead of its value 1). Therefore, the usage of the specific
definition slot extractors like ` Base = Slot 1 ` (see ~ df-base ) is
discouraged. Actually, these definitions are used in two basic theorems
named *id (theorems of the form ` C = Slot ( C `` ndx ) ` ) and *ndx
(theorems of the form ` ( C `` ndx ) = N ` ) only (see, for example,
~ baseid and ~ basendx ), except additionally in the discouraged theorem
~ baseval to demonstrate the representations of the value of the base
set extractor. The *id theorems are implementation independent
equivalents of the definitions by the means of ~ ndxid , but the *ndx
theorems still depend on the hard-coded values of the indices.
Therefore, the usage of these *ndx theorems is also discouraged (for
more details see comment on ~ basendx ).

Example: The group operation is the second component, i.e., the
component in the second slot, of a group-like structure
` G = { <. ( Base `` ndx ) , B >. , <. ( +g `` ndx ) , .+ >. } ` (see
~ grpstr ). The slot extractor ` +g = Slot 2 ` (see ~ df-plusg )
applied on the structure ` G ` provides the group operation
` .+ = ( +g `` G ) ` . Expanding the defintions, we get
` .+ = ( Slot 2 `` G ) = ( G `` 2 ) = ( G `` ( +g `` ndx ) ) ` (for the
last equation, see ~ plusgndx ).

The class ` Slot ` cannot be defined as
` ( x e. _V |-> ( f e. _V |-> ( f `` x ) ) ) ` because each ` Slot A `
Expand Down Expand Up @@ -200744,6 +200767,42 @@ class of all (base sets of) groups is proper. (Contributed by Mario
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
Structure component indices
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-

The structure component index extractor ` ndx `, defined in this subsection,
is used to get the numeric argument from a defined structure component
extractor such as ~ df-base (see ~ ndxarg ). For each defined structure
component extractor, there should be a corresponding specific theorem
providing its index, like ~ basendx . The usage of these theorems, however,
is discouraged since the particular value for the index is an implementation
detail. It is generally sufficient to work with ` ( Base `` ndx ) ` instead
of the hard-coded index value, and use theorems such as ~ baseid and
~ basendxnplusgndx .

The main circumstance in which it is necessary to look at indices directly is
when showing that a set of indices are disjoint (for example in proofs such
as ~ cznabel , based on ~ setsnid ) or even ordered (in proofs such as
~ lmodstr ). The requirement that the indices are distinct is necessary for
sets of ordered pairs to be extensible structures, whereas the ordering
allows for proofs avoiding the usage of quadradically many inequalities
(compare ~ cnfldfun with ~ cnfldfunALT ).

As for the inequalities, it is recommended to provide them explicitly as
theorems like ~ basendxnplusgndx , whenever they are required. Since these
theorems are proved by discouraged theorems, they should be placed near the
definition of a slot (within the same subsection), so that the range of
usages of discouraged theorems is tightly limited. Although there could be
quadradically many of them in the total number of indices, there actually
much less already available (and not much more are expected).

As for the ordering, there are some theorems like ~ basendxltplusgndx
providing the less-than relationship between two indices. These theorems are
also proved by discouraged theorems, so they should be placed near the
definition of a slot (within the same subsection), too. Since such theorems
are rarely used (in structure building theorems *str like ~ rngstr ), it is
not recommended to provide explicit theorems for all of them, but to use the
(discouraged) *ndx theorems as in ~ lmodstr . Therefore, such *str are
depending in general on the hard-coded values of the indices.

$)

$c ndx $.
Expand Down Expand Up @@ -201064,21 +201123,11 @@ class of all (base sets of) groups is proper. (Contributed by Mario
( wcel cvv elbasov simpld ) FAJEKJBKJFACDEBIGHLM $.
$}

$( Index value of the base set extractor.

Use of this theorem is discouraged since the particular value ` 1 ` for
the index is an implementation detail. It is generally sufficient to work
with ` ( Base `` ndx ) ` and use theorems such as ~ baseid and
~ basendxnn .

The main circumstance in which it is necessary to look at indices directly
is when showing that a set of indices are disjoint, in proofs such as
~ lmodstr . Although we have a few theorems such as ~ basendxnplusgndx ,
we do not intend to add such theorems for every pair of indices (which
would be quadradically many in the number of indices).

(New usage is discouraged.) (Contributed by Mario Carneiro,
2-Aug-2013.) $)
$( Index value of the base set extractor. (Contributed by Mario Carneiro,
2-Aug-2013.) Use of this theorem is discouraged since the particular
value ` 1 ` for the index is an implementation detail, see section header
comment ~ mmtheorems.html#cnx for more information.
(New usage is discouraged.) $)
basendx $p |- ( Base ` ndx ) = 1 $=
( cbs c1 df-base 1nn ndxarg ) ABCDE $.

Expand Down Expand Up @@ -202266,7 +202315,7 @@ base set is not the slot for the ring (multiplication) operation in an
) ABCZADCZEFGEGFHIJOFPGKLMN $.

$( The slot for the topology is not the slot for the involution in an
extensible structure. Formerly part of proof for ~ cnfldfun .
extensible structure. Formerly part of proof for ~ cnfldfunALT .
(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
Expand Down Expand Up @@ -202380,7 +202429,7 @@ be used in an extensible structure (slots must be positive integers).
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,
Formerly part of proof for ~ cnfldfunALT . (Contributed by AV,
11-Nov-2024.) $)
slotsdifplendx $p |- ( ( *r ` ndx ) =/= ( le ` ndx )
/\ ( TopSet ` ndx ) =/= ( le ` ndx ) ) $=
Expand Down Expand Up @@ -202514,7 +202563,7 @@ be used in an extensible structure (slots must be positive integers).
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,
Formerly part of proof for ~ cnfldfunALT . (Contributed by AV,
11-Nov-2024.) $)
slotsdifdsndx $p |- ( ( *r ` ndx ) =/= ( dist ` ndx )
/\ ( le ` ndx ) =/= ( dist ` ndx ) ) $=
Expand Down Expand Up @@ -202561,7 +202610,7 @@ be used in an extensible structure (slots must be positive integers).
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,
Formerly part of proof for ~ cnfldfunALT . (Contributed by AV,
10-Nov-2024.) $)
slotsdifunifndx $p |- ( ( ( +g ` ndx ) =/= ( UnifSet ` ndx )
/\ ( .r ` ndx ) =/= ( UnifSet ` ndx )
Expand Down Expand Up @@ -261840,9 +261889,35 @@ such that every prime ideal contains a prime element (this is a
VADQVBHIFKKLMNUAUBOIEVBNPZOUCEVAUDENOUKEUENOUFEVANRZVCSZHVCVDTVEOUGEULNOUHE
UINOUJEUMNROUNEUONPSZVESHVEVFTUPUQURUSUT $.

$( The field of complex numbers is a function. (Contributed by AV,
14-Nov-2021.) (Proof shortened by AV, 11-Nov-2024.) $)
$( The field of complex numbers is a function. The proof is much shorter
than the proof of ~ cnfldfunALT by using ~ cnfldstr and ~ structn0fun : in
addition, it must be shown that ` (/) e/ CCfld ` . (Contributed by AV,
18-Nov-2021.) $)
cnfldfun $p |- Fun CCfld $=
( ccnfld cop c0 wceq wcel wn cnx cfv cc ccj wo cabs cmin wa fvex cnex opnzi
nesymi cvv ax-mp c1 cdc cstr wbr wfun cnfldstr csn cdif structn0fun cin cbs
c3 cplusg caddc cmulr cmul ctp cstv cts ccom cmopn cple cle cds cunif cmetu
addex mulex w3o w3a 3ioran 0ex eltp xchnxbir mpbir3an wne wf cjf fex necomi
mp2an nelsn pm3.2i ctsr letsr elexi absf subf xpex coex mtbir ioran anbi12i
cr cxp bitri cun df-cnfld eleq2i elun orbi12i 3bitri disjsn disjdif2 funeqi
mpbir sylib ) AUAUAULUBBZUCUDZAUEZUFXIACUGZUHZUEXJAXHUIXLAAXKUJCDZXLADXMCAE
ZFXNCGUKHZIBZGUMHZUNBZGUOHZUPBZUQZEZCGURHZJBZUGZEZKZCGUSHZLMUTZVAHZBZGVBHZV
CBZGVDHZYIBZUQZEZCGVEHZYIVFHZBZUGZEZKZKZUUDFZYBFZYFFZNZYQFZUUBFZNZNZUUHUUKU
UFUUGUUFCXPDZFZCXRDZFZCXTDZFZXPCXOIGUKOPQRXRCXQUNGUMOVGQRXTCXSUPGUOOVHQRUUM
UUOUUQVIUUNUUPUURVJYBUUMUUOUUQVKCXPXRXTVLVMVNVOCYDVPUUGYDCYCJGUROIIJVQISEZJ
SEVRPIISJVSWAQVTCYDWBTWCUUIUUJYQCYKDZCYMDZCYODZVIZUVCFUUTFUVAFUVBFYKCYHYJGU
SOYIVAOQRYMCYLVCGVBOVCWDWEWFQRYOCYNYIGVDOLMIWNLVQUUSLSEWGPIWNSLVSWAIIWOZIMV
QUVDSEMSEWHIIPPWIUVDISMVSWAWJQRUUTUVAUVBVKVOCYKYMYOVLVMWKCYTVPUUJYTCYRYSGVE
OYIVFOQVTCYTWBTWCWCUUEYGFZUUCFZNUULYGUUCWLUVEUUHUVFUUKYBYFWLYQUUBWLWMWPXFXN
CYAYEWQZYPUUAWQZWQZECUVGEZCUVHEZKUUDAUVICWRWSCUVGUVHWTUVJYGUVKUUCCYAYEWTCYP
UUAWTXAXBWKACXCXFAXKXDTXEXGT $.

$( The field of complex numbers is a function. Alternate proof of ~ cnfldfun
not requireing that the index set of the components is ordered, but using
quadratically many inequalities for the indices. (Contributed by AV,
14-Nov-2021.) (Proof shortened by AV, 11-Nov-2024.)
(Proof modification is discouraged.) (New usage is discouraged.) $)
cnfldfunALT $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
Expand Down Expand Up @@ -261877,10 +261952,10 @@ such that every prime ideal contains a prime element (this is a
AUVHUVTUVDUWCRUWJUYBJKUWMUWJWNUWHUWIUWJUWLYCTYMUUBYDTSVLUUPUVGUVHXQXSVLUUOU
UPUWOYEXSSYOUUEWAPUAUUFYFYGYH $.

$( Obsolete proof of ~ cnfldfun as of 10-Nov-2024. The field of complex
$( Obsolete proof of ~ cnfldfunALT 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 $=
cnfldfunALTOLD $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
Expand Down Expand Up @@ -261923,29 +261998,6 @@ such that every prime ideal contains a prime element (this is a
UWHUXFWBUUQUVFHUYRFGUUQKUVFWEKUXGUVFKUXGYQJQKPYAYTUYQTLYBMNUUQUVFUUHUUIWOVS
UVTUWKUWLYOYPVSUVSUVTUXIUUJYPWOUUSUVIWPVQUAUVJUUKUUBUUL $.

$( Alternate proof of ~ cnfldfun (much shorter proof, using ~ cnfldstr and
~ structn0fun : in addition, it must be shown that ` (/) e/ CCfld ` ).
(Contributed by AV, 18-Nov-2021.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
cnfldfunALT $p |- Fun CCfld $=
( ccnfld cop c0 wceq wcel wn cnx cfv cc ccj wo cabs cmin wa fvex cnex opnzi
nesymi cvv ax-mp c1 cdc cstr wbr wfun cnfldstr csn cdif structn0fun cin cbs
c3 cplusg caddc cmulr cmul ctp cstv cts ccom cmopn cple cle cds cunif cmetu
addex mulex w3o w3a 3ioran 0ex eltp xchnxbir mpbir3an wne wf cjf fex necomi
mp2an nelsn pm3.2i ctsr letsr elexi absf subf xpex coex mtbir ioran anbi12i
cr cxp bitri cun df-cnfld eleq2i elun orbi12i 3bitri disjsn disjdif2 funeqi
mpbir sylib ) AUAUAULUBBZUCUDZAUEZUFXIACUGZUHZUEXJAXHUIXLAAXKUJCDZXLADXMCAE
ZFXNCGUKHZIBZGUMHZUNBZGUOHZUPBZUQZEZCGURHZJBZUGZEZKZCGUSHZLMUTZVAHZBZGVBHZV
CBZGVDHZYIBZUQZEZCGVEHZYIVFHZBZUGZEZKZKZUUDFZYBFZYFFZNZYQFZUUBFZNZNZUUHUUKU
UFUUGUUFCXPDZFZCXRDZFZCXTDZFZXPCXOIGUKOPQRXRCXQUNGUMOVGQRXTCXSUPGUOOVHQRUUM
UUOUUQVIUUNUUPUURVJYBUUMUUOUUQVKCXPXRXTVLVMVNVOCYDVPUUGYDCYCJGUROIIJVQISEZJ
SEVRPIISJVSWAQVTCYDWBTWCUUIUUJYQCYKDZCYMDZCYODZVIZUVCFUUTFUVAFUVBFYKCYHYJGU
SOYIVAOQRYMCYLVCGVBOVCWDWEWFQRYOCYNYIGVDOLMIWNLVQUUSLSEWGPIWNSLVSWAIIWOZIMV
QUVDSEMSEWHIIPPWIUVDISMVSWAWJQRUUTUVAUVBVKVOCYKYMYOVLVMWKCYTVPUUJYTCYRYSGVE
OYIVFOQVTCYTWBTWCWCUUEYGFZUUCFZNUULYGUUCWLUVEUUHUVFUUKYBYFWLYQUUBWLWMWPXFXN
CYAYEWQZYPUUAWQZWQZECUVGEZCUVHEZKUUDAUVICWRWSCUVGUVHWTUVJYGUVKUUCCYAYEWTCYP
UUAWTXAXBWKACXCXFAXKXDTXEXGT $.

${
$d x y z A $. $d x y B $.
$( The extended real structure is a structure. (Contributed by Mario
Expand Down

0 comments on commit 593e66d

Please sign in to comment.