![]() |
Intuitionistic Logic Explorer Theorem List (p. 128 of 149) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | topnidg 12701 | Value of the topology extractor function when the topology is defined over the same set as the base. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ π΅ = (Baseβπ) & β’ π½ = (TopSetβπ) β β’ ((π β π β§ π½ β π« π΅) β π½ = (TopOpenβπ)) | ||
Theorem | topnpropgd 12702 | The topology extractor function depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.) (Revised by Jim Kingdon, 13-Feb-2023.) |
β’ (π β (BaseβπΎ) = (BaseβπΏ)) & β’ (π β (TopSetβπΎ) = (TopSetβπΏ)) & β’ (π β πΎ β π) & β’ (π β πΏ β π) β β’ (π β (TopOpenβπΎ) = (TopOpenβπΏ)) | ||
Syntax | ctg 12703 | Extend class notation with a function that converts a basis to its corresponding topology. |
class topGen | ||
Syntax | cpt 12704 | Extend class notation with a function whose value is a product topology. |
class βt | ||
Syntax | c0g 12705 | Extend class notation with group identity element. |
class 0g | ||
Syntax | cgsu 12706 | Extend class notation to include finitely supported group sums. |
class Ξ£g | ||
Definition | df-0g 12707* | Define group identity element. Remark: this definition is required here because the symbol 0g is already used in df-gsum 12708. The related theorems will be provided later. (Contributed by NM, 20-Aug-2011.) |
β’ 0g = (π β V β¦ (β©π(π β (Baseβπ) β§ βπ₯ β (Baseβπ)((π(+gβπ)π₯) = π₯ β§ (π₯(+gβπ)π) = π₯)))) | ||
Definition | df-gsum 12708* |
Define the group sum for the structure πΊ of a finite sequence of
elements whose values are defined by the expression π΅ and
whose set
of indices is π΄. It may be viewed as a product (if
πΊ
is a
multiplication), a sum (if πΊ is an addition) or any other
operation.
The variable π is normally a free variable in π΅ (i.e.,
π΅
can
be thought of as π΅(π)). The definition is meaningful in
different contexts, depending on the size of the index set π΄ and
each demanding different properties of πΊ.
1. If π΄ = β and πΊ has an identity element, then the sum equals this identity. 2. If π΄ = (π...π) and πΊ is any magma, then the sum is the sum of the elements, evaluated left-to-right, i.e., (π΅(1) + π΅(2)) + π΅(3), etc. 3. If π΄ is a finite set (or is nonzero for finitely many indices) and πΊ is a commutative monoid, then the sum adds up these elements in some order, which is then uniquely defined. 4. If π΄ is an infinite set and πΊ is a Hausdorff topological group, then there is a meaningful sum, but Ξ£g cannot handle this case. (Contributed by FL, 5-Sep-2010.) (Revised by FL, 17-Oct-2011.) (Revised by Mario Carneiro, 7-Dec-2014.) |
β’ Ξ£g = (π€ β V, π β V β¦ β¦{π₯ β (Baseβπ€) β£ βπ¦ β (Baseβπ€)((π₯(+gβπ€)π¦) = π¦ β§ (π¦(+gβπ€)π₯) = π¦)} / πβ¦if(ran π β π, (0gβπ€), if(dom π β ran ..., (β©π₯βπβπ β (β€β₯βπ)(dom π = (π...π) β§ π₯ = (seqπ((+gβπ€), π)βπ))), (β©π₯βπ[(β‘π β (V β π)) / π¦](π:(1...(β―βπ¦))β1-1-ontoβπ¦ β§ π₯ = (seq1((+gβπ€), (π β π))β(β―βπ¦))))))) | ||
Definition | df-topgen 12709* | Define a function that converts a basis to its corresponding topology. Equivalent to the definition of a topology generated by a basis in [Munkres] p. 78. (Contributed by NM, 16-Jul-2006.) |
β’ topGen = (π₯ β V β¦ {π¦ β£ π¦ β βͺ (π₯ β© π« π¦)}) | ||
Definition | df-pt 12710* | Define the product topology on a collection of topologies. For convenience, it is defined on arbitrary collections of sets, expressed as a function from some index set to the subbases of each factor space. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ βt = (π β V β¦ (topGenβ{π₯ β£ βπ((π Fn dom π β§ βπ¦ β dom π(πβπ¦) β (πβπ¦) β§ βπ§ β Fin βπ¦ β (dom π β π§)(πβπ¦) = βͺ (πβπ¦)) β§ π₯ = Xπ¦ β dom π(πβπ¦))})) | ||
Theorem | tgval 12711* | The topology generated by a basis. See also tgval2 13554 and tgval3 13561. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
β’ (π΅ β π β (topGenβπ΅) = {π₯ β£ π₯ β βͺ (π΅ β© π« π₯)}) | ||
Theorem | tgvalex 12712 | The topology generated by a basis is a set. (Contributed by Jim Kingdon, 4-Mar-2023.) |
β’ (π΅ β π β (topGenβπ΅) β V) | ||
Theorem | ptex 12713 | Existence of the product topology. (Contributed by Jim Kingdon, 19-Mar-2025.) |
β’ (πΉ β π β (βtβπΉ) β V) | ||
Syntax | cprds 12714 | The function constructing structure products. |
class Xs | ||
Syntax | cpws 12715 | The function constructing structure powers. |
class βs | ||
Definition | df-prds 12716* | Define a structure product. This can be a product of groups, rings, modules, or ordered topological fields; any unused components will have garbage in them but this is usually not relevant for the purpose of inheriting the structures present in the factors. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.) |
β’ Xs = (π β V, π β V β¦ β¦Xπ₯ β dom π(Baseβ(πβπ₯)) / π£β¦β¦(π β π£, π β π£ β¦ Xπ₯ β dom π((πβπ₯)(Hom β(πβπ₯))(πβπ₯))) / ββ¦(({β¨(Baseβndx), π£β©, β¨(+gβndx), (π β π£, π β π£ β¦ (π₯ β dom π β¦ ((πβπ₯)(+gβ(πβπ₯))(πβπ₯))))β©, β¨(.rβndx), (π β π£, π β π£ β¦ (π₯ β dom π β¦ ((πβπ₯)(.rβ(πβπ₯))(πβπ₯))))β©} βͺ {β¨(Scalarβndx), π β©, β¨( Β·π βndx), (π β (Baseβπ ), π β π£ β¦ (π₯ β dom π β¦ (π( Β·π β(πβπ₯))(πβπ₯))))β©, β¨(Β·πβndx), (π β π£, π β π£ β¦ (π Ξ£g (π₯ β dom π β¦ ((πβπ₯)(Β·πβ(πβπ₯))(πβπ₯)))))β©}) βͺ ({β¨(TopSetβndx), (βtβ(TopOpen β π))β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β π£ β§ βπ₯ β dom π(πβπ₯)(leβ(πβπ₯))(πβπ₯))}β©, β¨(distβndx), (π β π£, π β π£ β¦ sup((ran (π₯ β dom π β¦ ((πβπ₯)(distβ(πβπ₯))(πβπ₯))) βͺ {0}), β*, < ))β©} βͺ {β¨(Hom βndx), ββ©, β¨(compβndx), (π β (π£ Γ π£), π β π£ β¦ (π β (πβ(2nd βπ)), π β (ββπ) β¦ (π₯ β dom π β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(πβπ₯))(πβπ₯))(πβπ₯)))))β©}))) | ||
Theorem | reldmprds 12717 | The structure product is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.) |
β’ Rel dom Xs | ||
Theorem | prdsex 12718 | Existence of the structure product. (Contributed by Jim Kingdon, 18-Mar-2025.) |
β’ ((π β π β§ π β π) β (πXsπ ) β V) | ||
Definition | df-pws 12719* | Define a structure power, which is just a structure product where all the factors are the same. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ βs = (π β V, π β V β¦ ((Scalarβπ)Xs(π Γ {π}))) | ||
Syntax | cimas 12720 | Image structure function. |
class βs | ||
Syntax | cqus 12721 | Quotient structure function. |
class /s | ||
Syntax | cxps 12722 | Binary product structure function. |
class Γs | ||
Definition | df-iimas 12723* |
Define an image structure, which takes a structure and a function on the
base set, and maps all the operations via the function. For this to
work properly π must either be injective or satisfy
the
well-definedness condition π(π) = π(π) β§ π(π) = π(π) β
π(π + π) = π(π + π) for each relevant operation.
Note that although we call this an "image" by association to df-ima 4640, in order to keep the definition simple we consider only the case when the domain of πΉ is equal to the base set of π . Other cases can be achieved by restricting πΉ (with df-res 4639) and/or π ( with df-iress 12470) to their common domain. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by AV, 6-Oct-2020.) |
β’ βs = (π β V, π β V β¦ β¦(Baseβπ) / π£β¦{β¨(Baseβndx), ran πβ©, β¨(+gβndx), βͺ π β π£ βͺ π β π£ {β¨β¨(πβπ), (πβπ)β©, (πβ(π(+gβπ)π))β©}β©, β¨(.rβndx), βͺ π β π£ βͺ π β π£ {β¨β¨(πβπ), (πβπ)β©, (πβ(π(.rβπ)π))β©}β©}) | ||
Definition | df-qus 12724* | Define a quotient ring (or quotient group), which is a special case of an image structure df-iimas 12723 where the image function is π₯ β¦ [π₯]π. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ /s = (π β V, π β V β¦ ((π₯ β (Baseβπ) β¦ [π₯]π) βs π)) | ||
Definition | df-xps 12725* | Define a binary product on structures. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.) |
β’ Γs = (π β V, π β V β¦ (β‘(π₯ β (Baseβπ), π¦ β (Baseβπ ) β¦ {β¨β , π₯β©, β¨1o, π¦β©}) βs ((Scalarβπ)Xs{β¨β , πβ©, β¨1o, π β©}))) | ||
Theorem | imasex 12726 | Existence of the image structure. (Contributed by Jim Kingdon, 13-Mar-2025.) |
β’ ((πΉ β π β§ π β π) β (πΉ βs π ) β V) | ||
Theorem | imasival 12727* | Value of an image structure. The is a lemma for the theorems imasbas 12728, imasplusg 12729, and imasmulr 12730 and should not be needed once they are proved. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Jim Kingdon, 11-Mar-2025.) (New usage is discouraged.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ + = (+gβπ ) & β’ Γ = (.rβπ ) & β’ Β· = ( Β·π βπ ) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©}) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Γ π))β©}) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) β β’ (π β π = {β¨(Baseβndx), π΅β©, β¨(+gβndx), β β©, β¨(.rβndx), β β©}) | ||
Theorem | imasbas 12728 | The base set of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 6-Oct-2020.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) β β’ (π β π΅ = (Baseβπ)) | ||
Theorem | imasplusg 12729* | The group operation in an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ + = (+gβπ ) & β’ β = (+gβπ) β β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©}) | ||
Theorem | imasmulr 12730* | The ring multiplication in an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) | ||
Theorem | f1ocpbllem 12731 | Lemma for f1ocpbl 12732. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (π΄ = πΆ β§ π΅ = π·))) | ||
Theorem | f1ocpbl 12732 | An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (πΉβ(π΄ + π΅)) = (πΉβ(πΆ + π·)))) | ||
Theorem | f1ovscpbl 12733 | An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β πΎ β§ π΅ β π β§ πΆ β π)) β ((πΉβπ΅) = (πΉβπΆ) β (πΉβ(π΄ + π΅)) = (πΉβ(π΄ + πΆ)))) | ||
Theorem | f1olecpbl 12734 | An injection is compatible with any relations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (π΄ππ΅ β πΆππ·))) | ||
Theorem | imasaddfnlemg 12735* | The image structure operation is a function if the original operation is compatible with the function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) & β’ (π β π β π) & β’ (π β Β· β πΆ) β β’ (π β β Fn (π΅ Γ π΅)) | ||
Theorem | imasaddvallemg 12736* | The operation of an image structure is defined to distribute over the mapping function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) & β’ (π β π β π) & β’ (π β Β· β πΆ) β β’ ((π β§ π β π β§ π β π) β ((πΉβπ) β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasaddflemg 12737* | The image set operations are closed if the original operation is. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) & β’ (π β π β π) & β’ (π β Β· β πΆ) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) β β’ (π β β :(π΅ Γ π΅)βΆπ΅) | ||
Theorem | imasaddfn 12738* | The image structure's group operation is a function. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 10-Jul-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (+gβπ ) & β’ β = (+gβπ) β β’ (π β β Fn (π΅ Γ π΅)) | ||
Theorem | imasaddval 12739* | The value of an image structure's group operation. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (+gβπ ) & β’ β = (+gβπ) β β’ ((π β§ π β π β§ π β π) β ((πΉβπ) β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasaddf 12740* | The image structure's group operation is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (+gβπ ) & β’ β = (+gβπ) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) β β’ (π β β :(π΅ Γ π΅)βΆπ΅) | ||
Theorem | imasmulfn 12741* | The image structure's ring multiplication is a function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ (π β β Fn (π΅ Γ π΅)) | ||
Theorem | imasmulval 12742* | The value of an image structure's ring multiplication. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ ((π β§ π β π β§ π β π) β ((πΉβπ) β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasmulf 12743* | The image structure's ring multiplication is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) β β’ (π β β :(π΅ Γ π΅)βΆπ΅) | ||
Theorem | qusval 12744* | Value of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β βΌ β π) & β’ (π β π β π) β β’ (π β π = (πΉ βs π )) | ||
Theorem | quslem 12745* | The function in qusval 12744 is a surjection onto a quotient set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β βΌ β π) & β’ (π β π β π) β β’ (π β πΉ:πβontoβ(π / βΌ )) | ||
Theorem | qusin 12746 | Restrict the equivalence relation in a quotient structure to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ β π) & β’ (π β π β π) & β’ (π β ( βΌ β π) β π) β β’ (π β π = (π /s ( βΌ β© (π Γ π)))) | ||
Theorem | qusbas 12747 | Base set of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ β π) & β’ (π β π β π) β β’ (π β (π / βΌ ) = (Baseβπ)) | ||
Theorem | divsfvalg 12748* | Value of the function in qusval 12744. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) |
β’ (π β βΌ Er π) & β’ (π β π β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β π΄ β π) β β’ (π β (πΉβπ΄) = [π΄] βΌ ) | ||
Theorem | ercpbllemg 12749* | Lemma for ercpbl 12750. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by AV, 12-Jul-2024.) |
β’ (π β βΌ Er π) & β’ (π β π β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β ((πΉβπ΄) = (πΉβπ΅) β π΄ βΌ π΅)) | ||
Theorem | ercpbl 12750* | Translate the function compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) |
β’ (π β βΌ Er π) & β’ (π β π β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ ((π β§ (π β π β§ π β π)) β (π + π) β π) & β’ (π β ((π΄ βΌ πΆ β§ π΅ βΌ π·) β (π΄ + π΅) βΌ (πΆ + π·))) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (πΉβ(π΄ + π΅)) = (πΉβ(πΆ + π·)))) | ||
Theorem | erlecpbl 12751* | Translate the relation compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) |
β’ (π β βΌ Er π) & β’ (π β π β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β ((π΄ βΌ πΆ β§ π΅ βΌ π·) β (π΄ππ΅ β πΆππ·))) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (π΄ππ΅ β πΆππ·))) | ||
Theorem | qusaddvallemg 12752* | Value of an operation defined on a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) & β’ (π β Β· β π) β β’ ((π β§ π β π β§ π β π) β ([π] βΌ β [π] βΌ ) = [(π Β· π)] βΌ ) | ||
Theorem | qusaddflemg 12753* | The operation of a quotient structure is a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) & β’ (π β Β· β π) β β’ (π β β :((π / βΌ ) Γ (π / βΌ ))βΆ(π / βΌ )) | ||
Theorem | qusaddval 12754* | The addition in a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ Β· = (+gβπ ) & β’ β = (+gβπ) β β’ ((π β§ π β π β§ π β π) β ([π] βΌ β [π] βΌ ) = [(π Β· π)] βΌ ) | ||
Theorem | qusaddf 12755* | The addition in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ Β· = (+gβπ ) & β’ β = (+gβπ) β β’ (π β β :((π / βΌ ) Γ (π / βΌ ))βΆ(π / βΌ )) | ||
Theorem | qusmulval 12756* | The multiplication in a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ ((π β§ π β π β§ π β π) β ([π] βΌ β [π] βΌ ) = [(π Β· π)] βΌ ) | ||
Theorem | qusmulf 12757* | The multiplication in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ (π β β :((π / βΌ ) Γ (π / βΌ ))βΆ(π / βΌ )) | ||
Theorem | fnpr2o 12758 | Function with a domain of 2o. (Contributed by Jim Kingdon, 25-Sep-2023.) |
β’ ((π΄ β π β§ π΅ β π) β {β¨β , π΄β©, β¨1o, π΅β©} Fn 2o) | ||
Theorem | fnpr2ob 12759 | Biconditional version of fnpr2o 12758. (Contributed by Jim Kingdon, 27-Sep-2023.) |
β’ ((π΄ β V β§ π΅ β V) β {β¨β , π΄β©, β¨1o, π΅β©} Fn 2o) | ||
Theorem | fvpr0o 12760 | The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.) |
β’ (π΄ β π β ({β¨β , π΄β©, β¨1o, π΅β©}ββ ) = π΄) | ||
Theorem | fvpr1o 12761 | The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.) |
β’ (π΅ β π β ({β¨β , π΄β©, β¨1o, π΅β©}β1o) = π΅) | ||
Theorem | fvprif 12762 | The value of the pair function at an element of 2o. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ ((π΄ β π β§ π΅ β π β§ πΆ β 2o) β ({β¨β , π΄β©, β¨1o, π΅β©}βπΆ) = if(πΆ = β , π΄, π΅)) | ||
Theorem | xpsfrnel 12763* | Elementhood in the target space of the function πΉ appearing in xpsval 12771. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ (πΊ β Xπ β 2o if(π = β , π΄, π΅) β (πΊ Fn 2o β§ (πΊββ ) β π΄ β§ (πΊβ1o) β π΅)) | ||
Theorem | xpsfeq 12764 | A function on 2o is determined by its values at zero and one. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ (πΊ Fn 2o β {β¨β , (πΊββ )β©, β¨1o, (πΊβ1o)β©} = πΊ) | ||
Theorem | xpsfrnel2 12765* | Elementhood in the target space of the function πΉ appearing in xpsval 12771. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ ({β¨β , πβ©, β¨1o, πβ©} β Xπ β 2o if(π = β , π΄, π΅) β (π β π΄ β§ π β π΅)) | ||
Theorem | xpscf 12766 | Equivalent condition for the pair function to be a proper function on π΄. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ({β¨β , πβ©, β¨1o, πβ©}:2oβΆπ΄ β (π β π΄ β§ π β π΄)) | ||
Theorem | xpsfval 12767* | The value of the function appearing in xpsval 12771. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ {β¨β , π₯β©, β¨1o, π¦β©}) β β’ ((π β π΄ β§ π β π΅) β (ππΉπ) = {β¨β , πβ©, β¨1o, πβ©}) | ||
Theorem | xpsff1o 12768* | The function appearing in xpsval 12771 is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = {β , 1o}. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ {β¨β , π₯β©, β¨1o, π¦β©}) β β’ πΉ:(π΄ Γ π΅)β1-1-ontoβXπ β 2o if(π = β , π΄, π΅) | ||
Theorem | xpsfrn 12769* | A short expression for the indexed cartesian product on two indices. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ {β¨β , π₯β©, β¨1o, π¦β©}) β β’ ran πΉ = Xπ β 2o if(π = β , π΄, π΅) | ||
Theorem | xpsff1o2 12770* | The function appearing in xpsval 12771 is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = {β , 1o}. (Contributed by Mario Carneiro, 24-Jan-2015.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ {β¨β , π₯β©, β¨1o, π¦β©}) β β’ πΉ:(π΄ Γ π΅)β1-1-ontoβran πΉ | ||
Theorem | xpsval 12771* | Value of the binary structure product function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.) |
β’ π = (π Γs π) & β’ π = (Baseβπ ) & β’ π = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π) & β’ πΉ = (π₯ β π, π¦ β π β¦ {β¨β , π₯β©, β¨1o, π¦β©}) & β’ πΊ = (Scalarβπ ) & β’ π = (πΊXs{β¨β , π β©, β¨1o, πβ©}) β β’ (π β π = (β‘πΉ βs π)) | ||
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 5880, binary operations are defined by a rule, and with df-ov 5878, 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 5878 (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 5878). The definition of magmas (Mgm, see df-mgm 12775) 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 12772 | Extend class notation with group addition as a function. |
class +π | ||
Syntax | cmgm 12773 | Extend class notation with class of all magmas. |
class Mgm | ||
Definition | df-plusf 12774* | 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 12785), while +g only has closure (mgmcl 12778). (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ +π = (π β V β¦ (π₯ β (Baseβπ), π¦ β (Baseβπ) β¦ (π₯(+gβπ)π¦))) | ||
Definition | df-mgm 12775* | 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 12776* | The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) |
β’ π΅ = (Baseβπ) & β’ β¬ = (+gβπ) β β’ (π β π β (π β Mgm β βπ₯ β π΅ βπ¦ β π΅ (π₯ β¬ π¦) β π΅)) | ||
Theorem | ismgmn0 12777* | The predicate "is a magma" for a structure with a nonempty base set. (Contributed by AV, 29-Jan-2020.) |
β’ π΅ = (Baseβπ) & β’ β¬ = (+gβπ) β β’ (π΄ β π΅ β (π β Mgm β βπ₯ β π΅ βπ¦ β π΅ (π₯ β¬ π¦) β π΅)) | ||
Theorem | mgmcl 12778 | Closure of the operation of a magma. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 13-Jan-2020.) |
β’ π΅ = (Baseβπ) & β’ β¬ = (+gβπ) β β’ ((π β Mgm β§ π β π΅ β§ π β π΅) β (π β¬ π) β π΅) | ||
Theorem | isnmgm 12779 | 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 12780 | 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. (Contributed by AV, 17-Feb-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = (Baseβπ») β β’ (((πΊ β Mgm β§ π» β Mgm) β§ (π β π΅ β§ (+gβπ») = ((+gβπΊ) βΎ (π Γ π))) β§ (π β π β§ π β π)) β (π(+gβπΊ)π) β π) | ||
Theorem | plusffvalg 12781* | The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Proof shortened by AV, 2-Mar-2024.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & ⒠⨣ = (+πβπΊ) β β’ (πΊ β π β ⨣ = (π₯ β π΅, π¦ β π΅ β¦ (π₯ + π¦))) | ||
Theorem | plusfvalg 12782 | The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & ⒠⨣ = (+πβπΊ) β β’ ((πΊ β π β§ π β π΅ β§ π β π΅) β (π ⨣ π) = (π + π)) | ||
Theorem | plusfeqg 12783 | 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 | plusffng 12784 | The group addition operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & ⒠⨣ = (+πβπΊ) β β’ (πΊ β π β ⨣ Fn (π΅ Γ π΅)) | ||
Theorem | mgmplusf 12785 | 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 | intopsn 12786 | The internal operation for a set is the trivial operation iff the set is a singleton. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 23-Jan-2020.) |
β’ (( β¬ :(π΅ Γ π΅)βΆπ΅ β§ π β π΅) β (π΅ = {π} β β¬ = {β¨β¨π, πβ©, πβ©})) | ||
Theorem | mgmb1mgm1 12787 | 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 12788 | Any set with an empty base set and any group operation is a magma. (Contributed by AV, 28-Aug-2021.) |
β’ ((π β π β§ (Baseβπ) = β ) β π β Mgm) | ||
Theorem | mgm1 12789 | 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 | opifismgmdc 12790* | 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(π, πΆ, π·)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β DECID π) & β’ (π β βπ₯ π₯ β π΅) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β πΆ β π΅) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β π· β π΅) β β’ (π β π β 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 12791) is an important property of monoids, and therefore also for groups, 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 12707. Related theorems which are already valid for magmas are provided in the following. | ||
Theorem | mgmidmo 12791* | 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 | grpidvalg 12792* | 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 | grpidpropdg 12793* | 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 12794 | The group zero extractor is a function. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ 0g Fn V | ||
Theorem | 0g0 12795 | The identity element function evaluates to the empty set on an empty structure. (Contributed by Stefan O'Rear, 2-Oct-2015.) |
β’ β = (0gββ ) | ||
Theorem | ismgmid 12796* | 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 12797* | 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 12798* | 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 ) = π)) | ||
Theorem | ismgmid2 12799* | Show that a given element is the identity element of a magma. (Contributed by Mario Carneiro, 27-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ (π β π β π΅) & β’ ((π β§ π₯ β π΅) β (π + π₯) = π₯) & β’ ((π β§ π₯ β π΅) β (π₯ + π) = π₯) β β’ (π β π = 0 ) | ||
Theorem | lidrideqd 12800* | If there is a left and right identity element for any binary operation (group operation) +, both identity elements are equal. Generalization of statement in [Lang] p. 3: it is sufficient that "e" is a left identity element and "e`" is a right identity element instead of both being (two-sided) identity elements. (Contributed by AV, 26-Dec-2023.) |
β’ (π β πΏ β π΅) & β’ (π β π β π΅) & β’ (π β βπ₯ β π΅ (πΏ + π₯) = π₯) & β’ (π β βπ₯ β π΅ (π₯ + π ) = π₯) β β’ (π β πΏ = π ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |