![]() |
Intuitionistic Logic Explorer Theorem List (p. 128 of 150) | < 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 | elrestr 12701 | Sufficient condition for being an open set in a subspace. (Contributed by Jeff Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
β’ ((π½ β π β§ π β π β§ π΄ β π½) β (π΄ β© π) β (π½ βΎt π)) | ||
Theorem | restid2 12702 | The subspace topology over a subset of the base set is the original topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ ((π΄ β π β§ π½ β π« π΄) β (π½ βΎt π΄) = π½) | ||
Theorem | restsspw 12703 | The subspace topology is a collection of subsets of the restriction set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ (π½ βΎt π΄) β π« π΄ | ||
Theorem | restid 12704 | The subspace topology of the base set is the original topology. (Contributed by Jeff Hankins, 9-Jul-2009.) (Revised by Mario Carneiro, 13-Aug-2015.) |
β’ π = βͺ π½ β β’ (π½ β π β (π½ βΎt π) = π½) | ||
Theorem | topnvalg 12705 | Value of the topology extractor function. (Contributed by Mario Carneiro, 13-Aug-2015.) (Revised by Jim Kingdon, 11-Feb-2023.) |
β’ π΅ = (Baseβπ) & β’ π½ = (TopSetβπ) β β’ (π β π β (π½ βΎt π΅) = (TopOpenβπ)) | ||
Theorem | topnidg 12706 | 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 12707 | 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 12708 | Extend class notation with a function that converts a basis to its corresponding topology. |
class topGen | ||
Syntax | cpt 12709 | Extend class notation with a function whose value is a product topology. |
class βt | ||
Syntax | c0g 12710 | Extend class notation with group identity element. |
class 0g | ||
Syntax | cgsu 12711 | Extend class notation to include finitely supported group sums. |
class Ξ£g | ||
Definition | df-0g 12712* | Define group identity element. Remark: this definition is required here because the symbol 0g is already used in df-gsum 12713. The related theorems will be provided later. (Contributed by NM, 20-Aug-2011.) |
β’ 0g = (π β V β¦ (β©π(π β (Baseβπ) β§ βπ₯ β (Baseβπ)((π(+gβπ)π₯) = π₯ β§ (π₯(+gβπ)π) = π₯)))) | ||
Definition | df-gsum 12713* |
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 12714* | 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 12715* | 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 12716* | The topology generated by a basis. See also tgval2 13636 and tgval3 13643. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
β’ (π΅ β π β (topGenβπ΅) = {π₯ β£ π₯ β βͺ (π΅ β© π« π₯)}) | ||
Theorem | tgvalex 12717 | The topology generated by a basis is a set. (Contributed by Jim Kingdon, 4-Mar-2023.) |
β’ (π΅ β π β (topGenβπ΅) β V) | ||
Theorem | ptex 12718 | Existence of the product topology. (Contributed by Jim Kingdon, 19-Mar-2025.) |
β’ (πΉ β π β (βtβπΉ) β V) | ||
Syntax | cprds 12719 | The function constructing structure products. |
class Xs | ||
Syntax | cpws 12720 | The function constructing structure powers. |
class βs | ||
Definition | df-prds 12721* | 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 12722 | 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 12723 | Existence of the structure product. (Contributed by Jim Kingdon, 18-Mar-2025.) |
β’ ((π β π β§ π β π) β (πXsπ ) β V) | ||
Definition | df-pws 12724* | 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 12725 | Image structure function. |
class βs | ||
Syntax | cqus 12726 | Quotient structure function. |
class /s | ||
Syntax | cxps 12727 | Binary product structure function. |
class Γs | ||
Definition | df-iimas 12728* |
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 4641, 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 4640) and/or π ( with df-iress 12472) 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 12729* | Define a quotient ring (or quotient group), which is a special case of an image structure df-iimas 12728 where the image function is π₯ β¦ [π₯]π. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ /s = (π β V, π β V β¦ ((π₯ β (Baseβπ) β¦ [π₯]π) βs π)) | ||
Definition | df-xps 12730* | 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 12731 | Existence of the image structure. (Contributed by Jim Kingdon, 13-Mar-2025.) |
β’ ((πΉ β π β§ π β π) β (πΉ βs π ) β V) | ||
Theorem | imasival 12732* | Value of an image structure. The is a lemma for the theorems imasbas 12733, imasplusg 12734, and imasmulr 12735 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 12733 | 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 12734* | 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 12735* | 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 12736 | Lemma for f1ocpbl 12737. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (π΄ = πΆ β§ π΅ = π·))) | ||
Theorem | f1ocpbl 12737 | An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (πΉβ(π΄ + π΅)) = (πΉβ(πΆ + π·)))) | ||
Theorem | f1ovscpbl 12738 | An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β πΎ β§ π΅ β π β§ πΆ β π)) β ((πΉβπ΅) = (πΉβπΆ) β (πΉβ(π΄ + π΅)) = (πΉβ(π΄ + πΆ)))) | ||
Theorem | f1olecpbl 12739 | An injection is compatible with any relations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β πΉ:πβ1-1-ontoβπ) β β’ ((π β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (((πΉβπ΄) = (πΉβπΆ) β§ (πΉβπ΅) = (πΉβπ·)) β (π΄ππ΅ β πΆππ·))) | ||
Theorem | imasaddfnlemg 12740* | 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 12741* | The operation of an image structure is defined to distribute over the mapping function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) & β’ (π β π β π) & β’ (π β Β· β πΆ) β β’ ((π β§ π β π β§ π β π) β ((πΉβπ) β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasaddflemg 12742* | The image set operations are closed if the original operation is. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) & β’ (π β π β π) & β’ (π β Β· β πΆ) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) β β’ (π β β :(π΅ Γ π΅)βΆπ΅) | ||
Theorem | imasaddfn 12743* | 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 12744* | The value of an image structure's group operation. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (+gβπ ) & β’ β = (+gβπ) β β’ ((π β§ π β π β§ π β π) β ((πΉβπ) β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasaddf 12745* | 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 12746* | The image structure's ring multiplication is a function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ (π β β Fn (π΅ Γ π΅)) | ||
Theorem | imasmulval 12747* | The value of an image structure's ring multiplication. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β π β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ ((π β§ π β π β§ π β π) β ((πΉβπ) β (πΉβπ)) = (πΉβ(π Β· π))) | ||
Theorem | imasmulf 12748* | 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 12749* | Value of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β βΌ β π) & β’ (π β π β π) β β’ (π β π = (πΉ βs π )) | ||
Theorem | quslem 12750* | The function in qusval 12749 is a surjection onto a quotient set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β βΌ β π) & β’ (π β π β π) β β’ (π β πΉ:πβontoβ(π / βΌ )) | ||
Theorem | qusin 12751 | Restrict the equivalence relation in a quotient structure to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ β π) & β’ (π β π β π) & β’ (π β ( βΌ β π) β π) β β’ (π β π = (π /s ( βΌ β© (π Γ π)))) | ||
Theorem | qusbas 12752 | Base set of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ β π) & β’ (π β π β π) β β’ (π β (π / βΌ ) = (Baseβπ)) | ||
Theorem | divsfvalg 12753* | Value of the function in qusval 12749. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) |
β’ (π β βΌ Er π) & β’ (π β π β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β π΄ β π) β β’ (π β (πΉβπ΄) = [π΄] βΌ ) | ||
Theorem | ercpbllemg 12754* | Lemma for ercpbl 12755. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by AV, 12-Jul-2024.) |
β’ (π β βΌ Er π) & β’ (π β π β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β ((πΉβπ΄) = (πΉβπ΅) β π΄ βΌ π΅)) | ||
Theorem | ercpbl 12755* | 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 12756* | 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 12757* | Value of an operation defined on a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) & β’ (π β Β· β π) β β’ ((π β§ π β π β§ π β π) β ([π] βΌ β [π] βΌ ) = [(π Β· π)] βΌ ) | ||
Theorem | qusaddflemg 12758* | The operation of a quotient structure is a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ πΉ = (π₯ β π β¦ [π₯] βΌ ) & β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π Β· π))β©}) & β’ (π β Β· β π) β β’ (π β β :((π / βΌ ) Γ (π / βΌ ))βΆ(π / βΌ )) | ||
Theorem | qusaddval 12759* | The addition in a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ Β· = (+gβπ ) & β’ β = (+gβπ) β β’ ((π β§ π β π β§ π β π) β ([π] βΌ β [π] βΌ ) = [(π Β· π)] βΌ ) | ||
Theorem | qusaddf 12760* | The addition in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ Β· = (+gβπ ) & β’ β = (+gβπ) β β’ (π β β :((π / βΌ ) Γ (π / βΌ ))βΆ(π / βΌ )) | ||
Theorem | qusmulval 12761* | The multiplication in a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ ((π β§ π β π β§ π β π) β ([π] βΌ β [π] βΌ ) = [(π Β· π)] βΌ ) | ||
Theorem | qusmulf 12762* | The multiplication in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) & β’ Β· = (.rβπ ) & β’ β = (.rβπ) β β’ (π β β :((π / βΌ ) Γ (π / βΌ ))βΆ(π / βΌ )) | ||
Theorem | fnpr2o 12763 | Function with a domain of 2o. (Contributed by Jim Kingdon, 25-Sep-2023.) |
β’ ((π΄ β π β§ π΅ β π) β {β¨β , π΄β©, β¨1o, π΅β©} Fn 2o) | ||
Theorem | fnpr2ob 12764 | Biconditional version of fnpr2o 12763. (Contributed by Jim Kingdon, 27-Sep-2023.) |
β’ ((π΄ β V β§ π΅ β V) β {β¨β , π΄β©, β¨1o, π΅β©} Fn 2o) | ||
Theorem | fvpr0o 12765 | The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.) |
β’ (π΄ β π β ({β¨β , π΄β©, β¨1o, π΅β©}ββ ) = π΄) | ||
Theorem | fvpr1o 12766 | The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.) |
β’ (π΅ β π β ({β¨β , π΄β©, β¨1o, π΅β©}β1o) = π΅) | ||
Theorem | fvprif 12767 | The value of the pair function at an element of 2o. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ ((π΄ β π β§ π΅ β π β§ πΆ β 2o) β ({β¨β , π΄β©, β¨1o, π΅β©}βπΆ) = if(πΆ = β , π΄, π΅)) | ||
Theorem | xpsfrnel 12768* | Elementhood in the target space of the function πΉ appearing in xpsval 12776. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ (πΊ β Xπ β 2o if(π = β , π΄, π΅) β (πΊ Fn 2o β§ (πΊββ ) β π΄ β§ (πΊβ1o) β π΅)) | ||
Theorem | xpsfeq 12769 | 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 12770* | Elementhood in the target space of the function πΉ appearing in xpsval 12776. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ ({β¨β , πβ©, β¨1o, πβ©} β Xπ β 2o if(π = β , π΄, π΅) β (π β π΄ β§ π β π΅)) | ||
Theorem | xpscf 12771 | Equivalent condition for the pair function to be a proper function on π΄. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ ({β¨β , πβ©, β¨1o, πβ©}:2oβΆπ΄ β (π β π΄ β§ π β π΄)) | ||
Theorem | xpsfval 12772* | The value of the function appearing in xpsval 12776. (Contributed by Mario Carneiro, 15-Aug-2015.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ {β¨β , π₯β©, β¨1o, π¦β©}) β β’ ((π β π΄ β§ π β π΅) β (ππΉπ) = {β¨β , πβ©, β¨1o, πβ©}) | ||
Theorem | xpsff1o 12773* | The function appearing in xpsval 12776 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 12774* | 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 12775* | The function appearing in xpsval 12776 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 12776* | 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 5882, binary operations are defined by a rule, and with df-ov 5880, 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 5880 (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 5880). The definition of magmas (Mgm, see df-mgm 12780) 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 12777 | Extend class notation with group addition as a function. |
class +π | ||
Syntax | cmgm 12778 | Extend class notation with class of all magmas. |
class Mgm | ||
Definition | df-plusf 12779* | 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 12790), while +g only has closure (mgmcl 12783). (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ +π = (π β V β¦ (π₯ β (Baseβπ), π¦ β (Baseβπ) β¦ (π₯(+gβπ)π¦))) | ||
Definition | df-mgm 12780* | 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 12781* | The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) |
β’ π΅ = (Baseβπ) & β’ β¬ = (+gβπ) β β’ (π β π β (π β Mgm β βπ₯ β π΅ βπ¦ β π΅ (π₯ β¬ π¦) β π΅)) | ||
Theorem | ismgmn0 12782* | The predicate "is a magma" for a structure with a nonempty base set. (Contributed by AV, 29-Jan-2020.) |
β’ π΅ = (Baseβπ) & β’ β¬ = (+gβπ) β β’ (π΄ β π΅ β (π β Mgm β βπ₯ β π΅ βπ¦ β π΅ (π₯ β¬ π¦) β π΅)) | ||
Theorem | mgmcl 12783 | Closure of the operation of a magma. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 13-Jan-2020.) |
β’ π΅ = (Baseβπ) & β’ β¬ = (+gβπ) β β’ ((π β Mgm β§ π β π΅ β§ π β π΅) β (π β¬ π) β π΅) | ||
Theorem | isnmgm 12784 | 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 12785 | 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 12786* | 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 12787 | The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & ⒠⨣ = (+πβπΊ) β β’ ((πΊ β π β§ π β π΅ β§ π β π΅) β (π ⨣ π) = (π + π)) | ||
Theorem | plusfeqg 12788 | 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 12789 | The group addition operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & ⒠⨣ = (+πβπΊ) β β’ (πΊ β π β ⨣ Fn (π΅ Γ π΅)) | ||
Theorem | mgmplusf 12790 | 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 12791 | 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 12792 | 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 12793 | Any set with an empty base set and any group operation is a magma. (Contributed by AV, 28-Aug-2021.) |
β’ ((π β π β§ (Baseβπ) = β ) β π β Mgm) | ||
Theorem | mgm1 12794 | 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 12795* | 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 12796) 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 12712. Related theorems which are already valid for magmas are provided in the following. | ||
Theorem | mgmidmo 12796* | 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 12797* | 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 12798* | 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 12799 | The group zero extractor is a function. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ 0g Fn V | ||
Theorem | 0g0 12800 | The identity element function evaluates to the empty set on an empty structure. (Contributed by Stefan O'Rear, 2-Oct-2015.) |
β’ β = (0gββ ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |