![]() |
Metamath
Proof Explorer Theorem List (p. 186 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30680) |
![]() (30681-32203) |
![]() (32204-48126) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ipopos 18501 | The inclusion poset on a family of sets is actually a poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
β’ πΌ = (toIncβπΉ) β β’ πΌ β Poset | ||
Theorem | isipodrs 18502* | Condition for a family of sets to be directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ ((toIncβπ΄) β Dirset β (π΄ β V β§ π΄ β β β§ βπ₯ β π΄ βπ¦ β π΄ βπ§ β π΄ (π₯ βͺ π¦) β π§)) | ||
Theorem | ipodrscl 18503 | Direction by inclusion as used here implies sethood. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ ((toIncβπ΄) β Dirset β π΄ β V) | ||
Theorem | ipodrsfi 18504* | Finite upper bound property for directed collections of sets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ (((toIncβπ΄) β Dirset β§ π β π΄ β§ π β Fin) β βπ§ β π΄ βͺ π β π§) | ||
Theorem | fpwipodrs 18505 | The finite subsets of any set are directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ (π΄ β π β (toIncβ(π« π΄ β© Fin)) β Dirset) | ||
Theorem | ipodrsima 18506* | The monotone image of a directed set. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ (π β πΉ Fn π« π΄) & β’ ((π β§ (π’ β π£ β§ π£ β π΄)) β (πΉβπ’) β (πΉβπ£)) & β’ (π β (toIncβπ΅) β Dirset) & β’ (π β π΅ β π« π΄) & β’ (π β (πΉ β π΅) β π) β β’ (π β (toIncβ(πΉ β π΅)) β Dirset) | ||
Theorem | isacs3lem 18507* | An algebraic closure system satisfies isacs3 18515. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ (πΆ β (ACSβπ) β (πΆ β (Mooreβπ) β§ βπ β π« πΆ((toIncβπ ) β Dirset β βͺ π β πΆ))) | ||
Theorem | acsdrsel 18508 | An algebraic closure system contains all directed unions of closed sets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ ((πΆ β (ACSβπ) β§ π β πΆ β§ (toIncβπ) β Dirset) β βͺ π β πΆ) | ||
Theorem | isacs4lem 18509* | In a closure system in which directed unions of closed sets are closed, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ ((πΆ β (Mooreβπ) β§ βπ β π« πΆ((toIncβπ ) β Dirset β βͺ π β πΆ)) β (πΆ β (Mooreβπ) β§ βπ‘ β π« π« π((toIncβπ‘) β Dirset β (πΉββͺ π‘) = βͺ (πΉ β π‘)))) | ||
Theorem | isacs5lem 18510* | If closure commutes with directed unions, then the closure of a set is the closure of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ ((πΆ β (Mooreβπ) β§ βπ‘ β π« π« π((toIncβπ‘) β Dirset β (πΉββͺ π‘) = βͺ (πΉ β π‘))) β (πΆ β (Mooreβπ) β§ βπ β π« π(πΉβπ ) = βͺ (πΉ β (π« π β© Fin)))) | ||
Theorem | acsdrscl 18511 | In an algebraic closure system, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ ((πΆ β (ACSβπ) β§ π β π« π β§ (toIncβπ) β Dirset) β (πΉββͺ π) = βͺ (πΉ β π)) | ||
Theorem | acsficl 18512 | A closure in an algebraic closure system is the union of the closures of finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ ((πΆ β (ACSβπ) β§ π β π) β (πΉβπ) = βͺ (πΉ β (π« π β© Fin))) | ||
Theorem | isacs5 18513* | A closure system is algebraic iff the closure of a generating set is the union of the closures of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ (πΆ β (ACSβπ) β (πΆ β (Mooreβπ) β§ βπ β π« π(πΉβπ ) = βͺ (πΉ β (π« π β© Fin)))) | ||
Theorem | isacs4 18514* | A closure system is algebraic iff closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ (πΆ β (ACSβπ) β (πΆ β (Mooreβπ) β§ βπ β π« π« π((toIncβπ ) β Dirset β (πΉββͺ π ) = βͺ (πΉ β π )))) | ||
Theorem | isacs3 18515* | A closure system is algebraic iff directed unions of closed sets are closed. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
β’ (πΆ β (ACSβπ) β (πΆ β (Mooreβπ) β§ βπ β π« πΆ((toIncβπ ) β Dirset β βͺ π β πΆ))) | ||
Theorem | acsficld 18516 | In an algebraic closure system, the closure of a set is the union of the closures of its finite subsets. Deduction form of acsficl 18512. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (ACSβπ)) & β’ π = (mrClsβπ΄) & β’ (π β π β π) β β’ (π β (πβπ) = βͺ (π β (π« π β© Fin))) | ||
Theorem | acsficl2d 18517* | In an algebraic closure system, an element is in the closure of a set if and only if it is in the closure of a finite subset. Alternate form of acsficl 18512. Deduction form. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (ACSβπ)) & β’ π = (mrClsβπ΄) & β’ (π β π β π) β β’ (π β (π β (πβπ) β βπ₯ β (π« π β© Fin)π β (πβπ₯))) | ||
Theorem | acsfiindd 18518 | In an algebraic closure system, a set is independent if and only if all its finite subsets are independent. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (ACSβπ)) & β’ π = (mrClsβπ΄) & β’ πΌ = (mrIndβπ΄) & β’ (π β π β π) β β’ (π β (π β πΌ β (π« π β© Fin) β πΌ)) | ||
Theorem | acsmapd 18519* | In an algebraic closure system, if π is contained in the closure of π, there is a map π from π into the set of finite subsets of π such that the closure of βͺ ran π contains π. This is proven by applying acsficl2d 18517 to each element of π. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (ACSβπ)) & β’ π = (mrClsβπ΄) & β’ (π β π β π) & β’ (π β π β (πβπ)) β β’ (π β βπ(π:πβΆ(π« π β© Fin) β§ π β (πββͺ ran π))) | ||
Theorem | acsmap2d 18520* | In an algebraic closure system, if π and π have the same closure and π is independent, then there is a map π from π into the set of finite subsets of π such that π equals the union of ran π. This is proven by taking the map π from acsmapd 18519 and observing that, since π and π have the same closure, the closure of βͺ ran π must contain π. Since π is independent, by mrissmrcd 17593, βͺ ran π must equal π. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (ACSβπ)) & β’ π = (mrClsβπ΄) & β’ πΌ = (mrIndβπ΄) & β’ (π β π β πΌ) & β’ (π β π β π) & β’ (π β (πβπ) = (πβπ)) β β’ (π β βπ(π:πβΆ(π« π β© Fin) β§ π = βͺ ran π)) | ||
Theorem | acsinfd 18521 | In an algebraic closure system, if π and π have the same closure and π is infinite independent, then π is infinite. This follows from applying unirnffid 9346 to the map given in acsmap2d 18520. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (ACSβπ)) & β’ π = (mrClsβπ΄) & β’ πΌ = (mrIndβπ΄) & β’ (π β π β πΌ) & β’ (π β π β π) & β’ (π β (πβπ) = (πβπ)) & β’ (π β Β¬ π β Fin) β β’ (π β Β¬ π β Fin) | ||
Theorem | acsdomd 18522 | In an algebraic closure system, if π and π have the same closure and π is infinite independent, then π dominates π. This follows from applying acsinfd 18521 and then applying unirnfdomd 10564 to the map given in acsmap2d 18520. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (ACSβπ)) & β’ π = (mrClsβπ΄) & β’ πΌ = (mrIndβπ΄) & β’ (π β π β πΌ) & β’ (π β π β π) & β’ (π β (πβπ) = (πβπ)) & β’ (π β Β¬ π β Fin) β β’ (π β π βΌ π) | ||
Theorem | acsinfdimd 18523 | In an algebraic closure system, if two independent sets have equal closure and one is infinite, then they are equinumerous. This is proven by using acsdomd 18522 twice with acsinfd 18521. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (ACSβπ)) & β’ π = (mrClsβπ΄) & β’ πΌ = (mrIndβπ΄) & β’ (π β π β πΌ) & β’ (π β π β πΌ) & β’ (π β (πβπ) = (πβπ)) & β’ (π β Β¬ π β Fin) β β’ (π β π β π) | ||
Theorem | acsexdimd 18524* | In an algebraic closure system whose closure operator has the exchange property, if two independent sets have equal closure, they are equinumerous. See mreexfidimd 17603 for the finite case and acsinfdimd 18523 for the infinite case. This is a special case of Theorem 4.2.2 in [FaureFrolicher] p. 87. (Contributed by David Moews, 1-May-2017.) |
β’ (π β π΄ β (ACSβπ)) & β’ π = (mrClsβπ΄) & β’ πΌ = (mrIndβπ΄) & β’ (π β βπ β π« πβπ¦ β π βπ§ β ((πβ(π βͺ {π¦})) β (πβπ ))π¦ β (πβ(π βͺ {π§}))) & β’ (π β π β πΌ) & β’ (π β π β πΌ) & β’ (π β (πβπ) = (πβπ)) β β’ (π β π β π) | ||
Theorem | mrelatglb 18525 | Greatest lower bounds in a Moore space are realized by intersections. (Contributed by Stefan O'Rear, 31-Jan-2015.) See mrelatglbALT 47895 for an alternate proof. |
β’ πΌ = (toIncβπΆ) & β’ πΊ = (glbβπΌ) β β’ ((πΆ β (Mooreβπ) β§ π β πΆ β§ π β β ) β (πΊβπ) = β© π) | ||
Theorem | mrelatglb0 18526 | The empty intersection in a Moore space is realized by the base set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
β’ πΌ = (toIncβπΆ) & β’ πΊ = (glbβπΌ) β β’ (πΆ β (Mooreβπ) β (πΊββ ) = π) | ||
Theorem | mrelatlub 18527 | Least upper bounds in a Moore space are realized by the closure of the union. (Contributed by Stefan O'Rear, 31-Jan-2015.) See mrelatlubALT 47894 for an alternate proof. |
β’ πΌ = (toIncβπΆ) & β’ πΉ = (mrClsβπΆ) & β’ πΏ = (lubβπΌ) β β’ ((πΆ β (Mooreβπ) β§ π β πΆ) β (πΏβπ) = (πΉββͺ π)) | ||
Theorem | mreclatBAD 18528* | A Moore space is a complete lattice under inclusion. (Contributed by Stefan O'Rear, 31-Jan-2015.) TODO (df-riota 7361 update): Reprove using isclat 18465 instead of the isclatBAD. hypothesis. See commented-out mreclat above. See mreclat 47896 for a good version. |
β’ πΌ = (toIncβπΆ) & β’ (πΌ β CLat β (πΌ β Poset β§ βπ₯(π₯ β (BaseβπΌ) β (((lubβπΌ)βπ₯) β (BaseβπΌ) β§ ((glbβπΌ)βπ₯) β (BaseβπΌ))))) β β’ (πΆ β (Mooreβπ) β πΌ β CLat) | ||
See commented-out notes for lattices as relations. | ||
Syntax | cps 18529 | Extend class notation with the class of all posets. |
class PosetRel | ||
Syntax | ctsr 18530 | Extend class notation with the class of all totally ordered sets. |
class TosetRel | ||
Definition | df-ps 18531 | Define the class of all posets (partially ordered sets) with weak ordering (e.g., "less than or equal to" instead of "less than"). A poset is a relation which is transitive, reflexive, and antisymmetric. (Contributed by NM, 11-May-2008.) |
β’ PosetRel = {π β£ (Rel π β§ (π β π) β π β§ (π β© β‘π) = ( I βΎ βͺ βͺ π))} | ||
Definition | df-tsr 18532 | Define the class of all totally ordered sets. (Contributed by FL, 1-Nov-2009.) |
β’ TosetRel = {π β PosetRel β£ (dom π Γ dom π) β (π βͺ β‘π)} | ||
Theorem | isps 18533 | The predicate "is a poset" i.e. a transitive, reflexive, antisymmetric relation. (Contributed by NM, 11-May-2008.) |
β’ (π β π΄ β (π β PosetRel β (Rel π β§ (π β π ) β π β§ (π β© β‘π ) = ( I βΎ βͺ βͺ π )))) | ||
Theorem | psrel 18534 | A poset is a relation. (Contributed by NM, 12-May-2008.) |
β’ (π΄ β PosetRel β Rel π΄) | ||
Theorem | psref2 18535 | A poset is antisymmetric and reflexive. (Contributed by FL, 3-Aug-2009.) |
β’ (π β PosetRel β (π β© β‘π ) = ( I βΎ βͺ βͺ π )) | ||
Theorem | pstr2 18536 | A poset is transitive. (Contributed by FL, 3-Aug-2009.) |
β’ (π β PosetRel β (π β π ) β π ) | ||
Theorem | pslem 18537 | Lemma for psref 18539 and others. (Contributed by NM, 12-May-2008.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ (π β PosetRel β (((π΄π π΅ β§ π΅π πΆ) β π΄π πΆ) β§ (π΄ β βͺ βͺ π β π΄π π΄) β§ ((π΄π π΅ β§ π΅π π΄) β π΄ = π΅))) | ||
Theorem | psdmrn 18538 | The domain and range of a poset equal its field. (Contributed by NM, 13-May-2008.) |
β’ (π β PosetRel β (dom π = βͺ βͺ π β§ ran π = βͺ βͺ π )) | ||
Theorem | psref 18539 | A poset is reflexive. (Contributed by NM, 13-May-2008.) |
β’ π = dom π β β’ ((π β PosetRel β§ π΄ β π) β π΄π π΄) | ||
Theorem | psrn 18540 | The range of a poset equals it domain. (Contributed by NM, 7-Jul-2008.) |
β’ π = dom π β β’ (π β PosetRel β π = ran π ) | ||
Theorem | psasym 18541 | A poset is antisymmetric. (Contributed by NM, 12-May-2008.) |
β’ ((π β PosetRel β§ π΄π π΅ β§ π΅π π΄) β π΄ = π΅) | ||
Theorem | pstr 18542 | A poset is transitive. (Contributed by NM, 12-May-2008.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ ((π β PosetRel β§ π΄π π΅ β§ π΅π πΆ) β π΄π πΆ) | ||
Theorem | cnvps 18543 | The converse of a poset is a poset. In the general case (β‘π β PosetRel β π β PosetRel) is not true. See cnvpsb 18544 for a special case where the property holds. (Contributed by FL, 5-Jan-2009.) (Proof shortened by Mario Carneiro, 3-Sep-2015.) |
β’ (π β PosetRel β β‘π β PosetRel) | ||
Theorem | cnvpsb 18544 | The converse of a poset is a poset. (Contributed by FL, 5-Jan-2009.) |
β’ (Rel π β (π β PosetRel β β‘π β PosetRel)) | ||
Theorem | psss 18545 | Any subset of a partially ordered set is partially ordered. (Contributed by FL, 24-Jan-2010.) |
β’ (π β PosetRel β (π β© (π΄ Γ π΄)) β PosetRel) | ||
Theorem | psssdm2 18546 | Field of a subposet. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ π = dom π β β’ (π β PosetRel β dom (π β© (π΄ Γ π΄)) = (π β© π΄)) | ||
Theorem | psssdm 18547 | Field of a subposet. (Contributed by FL, 19-Sep-2011.) (Revised by Mario Carneiro, 9-Sep-2015.) |
β’ π = dom π β β’ ((π β PosetRel β§ π΄ β π) β dom (π β© (π΄ Γ π΄)) = π΄) | ||
Theorem | istsr 18548 | The predicate is a toset. (Contributed by FL, 1-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
β’ π = dom π β β’ (π β TosetRel β (π β PosetRel β§ (π Γ π) β (π βͺ β‘π ))) | ||
Theorem | istsr2 18549* | The predicate is a toset. (Contributed by FL, 1-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
β’ π = dom π β β’ (π β TosetRel β (π β PosetRel β§ βπ₯ β π βπ¦ β π (π₯π π¦ β¨ π¦π π₯))) | ||
Theorem | tsrlin 18550 | A toset is a linear order. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ π = dom π β β’ ((π β TosetRel β§ π΄ β π β§ π΅ β π) β (π΄π π΅ β¨ π΅π π΄)) | ||
Theorem | tsrlemax 18551 | Two ways of saying a number is less than or equal to the maximum of two others. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ π = dom π β β’ ((π β TosetRel β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π if(π΅π πΆ, πΆ, π΅) β (π΄π π΅ β¨ π΄π πΆ))) | ||
Theorem | tsrps 18552 | A toset is a poset. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ (π β TosetRel β π β PosetRel) | ||
Theorem | cnvtsr 18553 | The converse of a toset is a toset. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (π β TosetRel β β‘π β TosetRel ) | ||
Theorem | tsrss 18554 | Any subset of a totally ordered set is totally ordered. (Contributed by FL, 24-Jan-2010.) (Proof shortened by Mario Carneiro, 21-Nov-2013.) |
β’ (π β TosetRel β (π β© (π΄ Γ π΄)) β TosetRel ) | ||
Theorem | ledm 18555 | The domain of β€ is β*. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 4-May-2015.) |
β’ β* = dom β€ | ||
Theorem | lern 18556 | The range of β€ is β*. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 3-Sep-2015.) |
β’ β* = ran β€ | ||
Theorem | lefld 18557 | The field of the 'less or equal to' relationship on the extended real. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 4-May-2015.) |
β’ β* = βͺ βͺ β€ | ||
Theorem | letsr 18558 | The "less than or equal to" relationship on the extended reals is a toset. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 3-Sep-2015.) |
β’ β€ β TosetRel | ||
Syntax | cdir 18559 | Extend class notation with the class of directed sets. |
class DirRel | ||
Syntax | ctail 18560 | Extend class notation with the tail function for directed sets. |
class tail | ||
Definition | df-dir 18561 | Define the class of directed sets (the order relation itself is sometimes called a direction, and a directed set is a set equipped with a direction). (Contributed by Jeff Hankins, 25-Nov-2009.) |
β’ DirRel = {π β£ ((Rel π β§ ( I βΎ βͺ βͺ π) β π) β§ ((π β π) β π β§ (βͺ βͺ π Γ βͺ βͺ π) β (β‘π β π)))} | ||
Definition | df-tail 18562* | Define the tail function for directed sets. (Contributed by Jeff Hankins, 25-Nov-2009.) |
β’ tail = (π β DirRel β¦ (π₯ β βͺ βͺ π β¦ (π β {π₯}))) | ||
Theorem | isdir 18563 | A condition for a relation to be a direction. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
β’ π΄ = βͺ βͺ π β β’ (π β π β (π β DirRel β ((Rel π β§ ( I βΎ π΄) β π ) β§ ((π β π ) β π β§ (π΄ Γ π΄) β (β‘π β π ))))) | ||
Theorem | reldir 18564 | A direction is a relation. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
β’ (π β DirRel β Rel π ) | ||
Theorem | dirdm 18565 | A direction's domain is equal to its field. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
β’ (π β DirRel β dom π = βͺ βͺ π ) | ||
Theorem | dirref 18566 | A direction is reflexive. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
β’ π = dom π β β’ ((π β DirRel β§ π΄ β π) β π΄π π΄) | ||
Theorem | dirtr 18567 | A direction is transitive. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
β’ (((π β DirRel β§ πΆ β π) β§ (π΄π π΅ β§ π΅π πΆ)) β π΄π πΆ) | ||
Theorem | dirge 18568* | For any two elements of a directed set, there exists a third element greater than or equal to both. Note that this does not say that the two elements have a least upper bound. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
β’ π = dom π β β’ ((π β DirRel β§ π΄ β π β§ π΅ β π) β βπ₯ β π (π΄π π₯ β§ π΅π π₯)) | ||
Theorem | tsrdir 18569 | A totally ordered set is a directed set. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
β’ (π΄ β TosetRel β π΄ β DirRel) | ||
According to Wikipedia ("Magma (algebra)", 08-Jan-2020, https://en.wikipedia.org/wiki/magma_(algebra)) "In abstract algebra, a magma [...] is a basic kind of algebraic structure. Specifically, a magma consists of a set equipped with a single binary operation. The binary operation must be closed by definition but no other properties are imposed.". Since the concept of a "binary operation" is used in different variants, these differences are explained in more detail in the following: With df-mpo 7410, binary operations are defined by a rule, and with df-ov 7408, the value of a binary operation applied to two operands can be expressed. In both cases, the two operands can belong to different sets, and the result can be an element of a third set. However, according to Wikipedia "Binary operation", see https://en.wikipedia.org/wiki/Binary_operation 7408 (19-Jan-2020), "... a binary operation on a set π is a mapping of the elements of the Cartesian product π Γ π to S: π:π Γ πβΆπ. Because the result of performing the operation on a pair of elements of S is again an element of S, the operation is called a closed binary operation on S (or sometimes expressed as having the property of closure).". To distinguish this more restrictive definition (in Wikipedia and most of the literature) from the general case, binary operations mapping the elements of the Cartesian product π Γ π are more precisely called internal binary operations. If, in addition, the result is also contained in the set π, the operation should be called closed internal binary operation. Therefore, a "binary operation on a set π" according to Wikipedia is a "closed internal binary operation" in a more precise terminology. If the sets are different, the operation is explicitly called external binary operation (see Wikipedia https://en.wikipedia.org/wiki/Binary_operation#External_binary_operations 7408). The definition of magmas (Mgm, see df-mgm 18573) concentrates on the closure property of the associated operation, and poses no additional restrictions on it. In this way, it is most general and flexible. | ||
Syntax | cplusf 18570 | Extend class notation with group addition as a function. |
class +π | ||
Syntax | cmgm 18571 | Extend class notation with class of all magmas. |
class Mgm | ||
Definition | df-plusf 18572* | Define group addition function. Usually we will use +g directly instead of +π, and they have the same behavior in most cases. The main advantage of +π for any magma is that it is a guaranteed function (mgmplusf 18583), while +g only has closure (mgmcl 18576). (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ +π = (π β V β¦ (π₯ β (Baseβπ), π¦ β (Baseβπ) β¦ (π₯(+gβπ)π¦))) | ||
Definition | df-mgm 18573* | A magma is a set equipped with an everywhere defined internal operation. Definition 1 in [BourbakiAlg1] p. 1, or definition of a groupoid in section I.1 of [Bruck] p. 1. Note: The term "groupoid" is now widely used to refer to other objects: (small) categories all of whose morphisms are invertible, or groups with a partial function replacing the binary operation. Therefore, we will only use the term "magma" for the present notion in set.mm. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) |
β’ Mgm = {π β£ [(Baseβπ) / π][(+gβπ) / π]βπ₯ β π βπ¦ β π (π₯ππ¦) β π} | ||
Theorem | ismgm 18574* | The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) |
β’ π΅ = (Baseβπ) & β’ β¬ = (+gβπ) β β’ (π β π β (π β Mgm β βπ₯ β π΅ βπ¦ β π΅ (π₯ β¬ π¦) β π΅)) | ||
Theorem | ismgmn0 18575* | The predicate "is a magma" for a structure with a nonempty base set. (Contributed by AV, 29-Jan-2020.) |
β’ π΅ = (Baseβπ) & β’ β¬ = (+gβπ) β β’ (π΄ β π΅ β (π β Mgm β βπ₯ β π΅ βπ¦ β π΅ (π₯ β¬ π¦) β π΅)) | ||
Theorem | mgmcl 18576 | Closure of the operation of a magma. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 13-Jan-2020.) |
β’ π΅ = (Baseβπ) & β’ β¬ = (+gβπ) β β’ ((π β Mgm β§ π β π΅ β§ π β π΅) β (π β¬ π) β π΅) | ||
Theorem | isnmgm 18577 | A condition for a structure not to be a magma. (Contributed by AV, 30-Jan-2020.) (Proof shortened by NM, 5-Feb-2020.) |
β’ π΅ = (Baseβπ) & β’ β¬ = (+gβπ) β β’ ((π β π΅ β§ π β π΅ β§ (π β¬ π) β π΅) β π β Mgm) | ||
Theorem | mgmsscl 18578 | If the base set of a magma is contained in the base set of another magma, and the group operation of the magma is the restriction of the group operation of the other magma to its base set, then the base set of the magma is closed under the group operation of the other magma. Formerly part of proof of grpissubg 19073. (Contributed by AV, 17-Feb-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = (Baseβπ») β β’ (((πΊ β Mgm β§ π» β Mgm) β§ (π β π΅ β§ (+gβπ») = ((+gβπΊ) βΎ (π Γ π))) β§ (π β π β§ π β π)) β (π(+gβπΊ)π) β π) | ||
Theorem | plusffval 18579* | The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Proof shortened by AV, 2-Mar-2024.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & ⒠⨣ = (+πβπΊ) β ⒠⨣ = (π₯ β π΅, π¦ β π΅ β¦ (π₯ + π¦)) | ||
Theorem | plusfval 18580 | The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & ⒠⨣ = (+πβπΊ) β β’ ((π β π΅ β§ π β π΅) β (π ⨣ π) = (π + π)) | ||
Theorem | plusfeq 18581 | If the addition operation is already a function, the functionalization of it is equal to the original operation. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & ⒠⨣ = (+πβπΊ) β β’ ( + Fn (π΅ Γ π΅) β ⨣ = + ) | ||
Theorem | plusffn 18582 | The group addition operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & ⒠⨣ = (+πβπΊ) β ⒠⨣ Fn (π΅ Γ π΅) | ||
Theorem | mgmplusf 18583 | The group addition function of a magma is a function into its base set. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revisd by AV, 28-Jan-2020.) |
β’ π΅ = (Baseβπ) & ⒠⨣ = (+πβπ) β β’ (π β Mgm β ⨣ :(π΅ Γ π΅)βΆπ΅) | ||
Theorem | mgmpropd 18584* | If two structures have the same (nonempty) base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, one is a magma iff the other one is. (Contributed by AV, 25-Feb-2020.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β π΅ β β ) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) β β’ (π β (πΎ β Mgm β πΏ β Mgm)) | ||
Theorem | ismgmd 18585* | Deduce a magma from its properties. (Contributed by AV, 25-Feb-2020.) |
β’ (π β π΅ = (BaseβπΊ)) & β’ (π β πΊ β π) & β’ (π β + = (+gβπΊ)) & β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) β π΅) β β’ (π β πΊ β Mgm) | ||
Theorem | issstrmgm 18586* | Characterize a substructure as submagma by closure properties. (Contributed by AV, 30-Aug-2021.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π» = (πΊ βΎs π) β β’ ((π» β π β§ π β π΅) β (π» β Mgm β βπ₯ β π βπ¦ β π (π₯ + π¦) β π)) | ||
Theorem | intopsn 18587 | The internal operation for a set is the trivial operation iff the set is a singleton. Formerly part of proof of ring1zr 20627. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 23-Jan-2020.) |
β’ (( β¬ :(π΅ Γ π΅)βΆπ΅ β§ π β π΅) β (π΅ = {π} β β¬ = {β¨β¨π, πβ©, πβ©})) | ||
Theorem | mgmb1mgm1 18588 | The only magma with a base set consisting of one element is the trivial magma (at least if its operation is an internal binary operation). (Contributed by AV, 23-Jan-2020.) (Revised by AV, 7-Feb-2020.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) β β’ ((π β Mgm β§ π β π΅ β§ + Fn (π΅ Γ π΅)) β (π΅ = {π} β + = {β¨β¨π, πβ©, πβ©})) | ||
Theorem | mgm0 18589 | Any set with an empty base set and any group operation is a magma. (Contributed by AV, 28-Aug-2021.) |
β’ ((π β π β§ (Baseβπ) = β ) β π β Mgm) | ||
Theorem | mgm0b 18590 | The structure with an empty base set and any group operation is a magma. (Contributed by AV, 28-Aug-2021.) |
β’ {β¨(Baseβndx), β β©, β¨(+gβndx), πβ©} β Mgm | ||
Theorem | mgm1 18591 | The structure with one element and the only closed internal operation for a singleton is a magma. (Contributed by AV, 10-Feb-2020.) |
β’ π = {β¨(Baseβndx), {πΌ}β©, β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©} β β’ (πΌ β π β π β Mgm) | ||
Theorem | opifismgm 18592* | A structure with a group addition operation expressed by a conditional operator is a magma if both values of the conditional operator are contained in the base set. (Contributed by AV, 9-Feb-2020.) |
β’ π΅ = (Baseβπ) & β’ (+gβπ) = (π₯ β π΅, π¦ β π΅ β¦ if(π, πΆ, π·)) & β’ (π β π΅ β β ) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β πΆ β π΅) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π· β π΅) β β’ (π β π β Mgm) | ||
According to Wikipedia ("Identity element", 7-Feb-2020, https://en.wikipedia.org/wiki/Identity_element): "In mathematics, an identity element, or neutral element, is a special type of element of a set with respect to a binary operation on that set, which leaves any element of the set unchanged when combined with it.". Or in more detail "... an element e of S is called a left identity if e * a = a for all a in S, and a right identity if a * e = a for all a in S. If e is both a left identity and a right identity, then it is called a two-sided identity, or simply an identity." We concentrate on two-sided identities in the following. The existence of an identity (an identity is unique if it exists, see mgmidmo 18593) is an important property of monoids (see mndid 18677), and therefore also for groups (see grpid 18905), but also for magmas not required to be associative. Magmas with an identity element are called "unital magmas" (see Definition 2 in [BourbakiAlg1] p. 12) or, if the magmas are cancellative, "loops" (see definition in [Bruck] p. 15). In the context of extensible structures, the identity element (of any magma π) is defined as "group identity element" (0gβπ), see df-0g 17396. Related theorems which are already valid for magmas are provided in the following. | ||
Theorem | mgmidmo 18593* | A two-sided identity element is unique (if it exists) in any magma. (Contributed by Mario Carneiro, 7-Dec-2014.) (Revised by NM, 17-Jun-2017.) |
β’ β*π’ β π΅ βπ₯ β π΅ ((π’ + π₯) = π₯ β§ (π₯ + π’) = π₯) | ||
Theorem | grpidval 18594* | The value of the identity element of a group. (Contributed by NM, 20-Aug-2011.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) β β’ 0 = (β©π(π β π΅ β§ βπ₯ β π΅ ((π + π₯) = π₯ β§ (π₯ + π) = π₯))) | ||
Theorem | grpidpropd 18595* | If two structures have the same base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, they have the same identity element. (Contributed by Mario Carneiro, 27-Nov-2014.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) β β’ (π β (0gβπΎ) = (0gβπΏ)) | ||
Theorem | fn0g 18596 | The group zero extractor is a function. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ 0g Fn V | ||
Theorem | 0g0 18597 | The identity element function evaluates to the empty set on an empty structure. (Contributed by Stefan O'Rear, 2-Oct-2015.) |
β’ β = (0gββ ) | ||
Theorem | ismgmid 18598* | The identity element of a magma, if it exists, belongs to the base set. (Contributed by Mario Carneiro, 27-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ (π β βπ β π΅ βπ₯ β π΅ ((π + π₯) = π₯ β§ (π₯ + π) = π₯)) β β’ (π β ((π β π΅ β§ βπ₯ β π΅ ((π + π₯) = π₯ β§ (π₯ + π) = π₯)) β 0 = π)) | ||
Theorem | mgmidcl 18599* | The identity element of a magma, if it exists, belongs to the base set. (Contributed by Mario Carneiro, 27-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ (π β βπ β π΅ βπ₯ β π΅ ((π + π₯) = π₯ β§ (π₯ + π) = π₯)) β β’ (π β 0 β π΅) | ||
Theorem | mgmlrid 18600* | The identity element of a magma, if it exists, is a left and right identity. (Contributed by Mario Carneiro, 27-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ (π β βπ β π΅ βπ₯ β π΅ ((π + π₯) = π₯ β§ (π₯ + π) = π₯)) β β’ ((π β§ π β π΅) β (( 0 + π) = π β§ (π + 0 ) = π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |