Home | Metamath
Proof Explorer Theorem List (p. 459 of 470) | < 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: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | uspgrex 45801* | The class ๐บ of all "simple pseudographs" with a fixed set of vertices ๐ is a set. (Contributed by AV, 26-Nov-2021.) |
โข ๐ = ๐ซ (Pairsโ๐) & โข ๐บ = {โจ๐ฃ, ๐โฉ โฃ (๐ฃ = ๐ โง โ๐ โ USPGraph ((Vtxโ๐) = ๐ฃ โง (Edgโ๐) = ๐))} โ โข (๐ โ ๐ โ ๐บ โ V) | ||
Theorem | uspgrbispr 45802* | There is a bijection between the "simple pseudographs" with a fixed set of vertices ๐ and the subsets of the set of pairs over the set ๐. (Contributed by AV, 26-Nov-2021.) |
โข ๐ = ๐ซ (Pairsโ๐) & โข ๐บ = {โจ๐ฃ, ๐โฉ โฃ (๐ฃ = ๐ โง โ๐ โ USPGraph ((Vtxโ๐) = ๐ฃ โง (Edgโ๐) = ๐))} โ โข (๐ โ ๐ โ โ๐ ๐:๐บโ1-1-ontoโ๐) | ||
Theorem | uspgrspren 45803* | The set ๐บ of the "simple pseudographs" with a fixed set of vertices ๐ and the class ๐ of subsets of the set of pairs over the fixed set ๐ are equinumerous. (Contributed by AV, 27-Nov-2021.) |
โข ๐ = ๐ซ (Pairsโ๐) & โข ๐บ = {โจ๐ฃ, ๐โฉ โฃ (๐ฃ = ๐ โง โ๐ โ USPGraph ((Vtxโ๐) = ๐ฃ โง (Edgโ๐) = ๐))} โ โข (๐ โ ๐ โ ๐บ โ ๐) | ||
Theorem | uspgrymrelen 45804* | The set ๐บ of the "simple pseudographs" with a fixed set of vertices ๐ and the class ๐ of the symmetric relations on the fixed set ๐ are equinumerous. For more details about the class ๐บ of all "simple pseudographs" see comments on uspgrbisymrel 45805. (Contributed by AV, 27-Nov-2021.) |
โข ๐บ = {โจ๐ฃ, ๐โฉ โฃ (๐ฃ = ๐ โง โ๐ โ USPGraph ((Vtxโ๐) = ๐ฃ โง (Edgโ๐) = ๐))} & โข ๐ = {๐ โ ๐ซ (๐ ร ๐) โฃ โ๐ฅ โ ๐ โ๐ฆ โ ๐ (๐ฅ๐๐ฆ โ ๐ฆ๐๐ฅ)} โ โข (๐ โ ๐ โ ๐บ โ ๐ ) | ||
Theorem | uspgrbisymrel 45805* |
There is a bijection between the "simple pseudographs" for a fixed
set
๐ of vertices and the class ๐
of the
symmetric relations on the
fixed set ๐. The simple pseudographs, which are
graphs without
hyper- or multiedges, but which may contain loops, are expressed as
ordered pairs of the vertices and the edges (as proper or improper
unordered pairs of vertices, not as indexed edges!) in this theorem.
That class ๐บ of such simple pseudographs is a set
(if ๐ is a
set, see uspgrex 45801) of equivalence classes of graphs
abstracting from
the index sets of their edge functions.
Solely for this abstraction, there is a bijection between the "simple pseudographs" as members of ๐บ and the symmetric relations ๐ on the fixed set ๐ of vertices. This theorem would not hold for ๐บ = {๐ โ USPGraph โฃ (Vtxโ๐) = ๐} and even not for ๐บ = {โจ๐ฃ, ๐โฉ โฃ (๐ฃ = ๐ โง โจ๐ฃ, ๐โฉ โ USPGraph)}, because these are much bigger classes. (Proposed by Gerard Lang, 16-Nov-2021.) (Contributed by AV, 27-Nov-2021.) |
โข ๐บ = {โจ๐ฃ, ๐โฉ โฃ (๐ฃ = ๐ โง โ๐ โ USPGraph ((Vtxโ๐) = ๐ฃ โง (Edgโ๐) = ๐))} & โข ๐ = {๐ โ ๐ซ (๐ ร ๐) โฃ โ๐ฅ โ ๐ โ๐ฆ โ ๐ (๐ฅ๐๐ฆ โ ๐ฆ๐๐ฅ)} โ โข (๐ โ ๐ โ โ๐ ๐:๐บโ1-1-ontoโ๐ ) | ||
Theorem | uspgrbisymrelALT 45806* | Alternate proof of uspgrbisymrel 45805 not using the definition of equinumerosity. (Contributed by AV, 26-Nov-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
โข ๐บ = {โจ๐ฃ, ๐โฉ โฃ (๐ฃ = ๐ โง โ๐ โ USPGraph ((Vtxโ๐) = ๐ฃ โง (Edgโ๐) = ๐))} & โข ๐ = {๐ โ ๐ซ (๐ ร ๐) โฃ โ๐ฅ โ ๐ โ๐ฆ โ ๐ (๐ฅ๐๐ฆ โ ๐ฆ๐๐ฅ)} โ โข (๐ โ ๐ โ โ๐ ๐:๐บโ1-1-ontoโ๐ ) | ||
Theorem | ovn0dmfun 45807 | If a class operation value for two operands is not the empty set, then the operands are contained in the domain of the class, and the class restricted to the operands is a function, analogous to fvfundmfvn0 6880. (Contributed by AV, 27-Jan-2020.) |
โข ((๐ด๐น๐ต) โ โ โ (โจ๐ด, ๐ตโฉ โ dom ๐น โง Fun (๐น โพ {โจ๐ด, ๐ตโฉ}))) | ||
Theorem | xpsnopab 45808* | A Cartesian product with a singleton expressed as ordered-pair class abstraction. (Contributed by AV, 27-Jan-2020.) |
โข ({๐} ร ๐ถ) = {โจ๐, ๐โฉ โฃ (๐ = ๐ โง ๐ โ ๐ถ)} | ||
Theorem | xpiun 45809* | A Cartesian product expressed as indexed union of ordered-pair class abstractions. (Contributed by AV, 27-Jan-2020.) |
โข (๐ต ร ๐ถ) = โช ๐ฅ โ ๐ต {โจ๐, ๐โฉ โฃ (๐ = ๐ฅ โง ๐ โ ๐ถ)} | ||
Theorem | ovn0ssdmfun 45810* | If a class' operation value for two operands is not the empty set, the operands are contained in the domain of the class, and the class restricted to the operands is a function, analogous to fvfundmfvn0 6880. (Contributed by AV, 27-Jan-2020.) |
โข (โ๐ โ ๐ท โ๐ โ ๐ธ (๐๐น๐) โ โ โ ((๐ท ร ๐ธ) โ dom ๐น โง Fun (๐น โพ (๐ท ร ๐ธ)))) | ||
Theorem | fnxpdmdm 45811 | The domain of the domain of a function over a Cartesian square. (Contributed by AV, 13-Jan-2020.) |
โข (๐น Fn (๐ด ร ๐ด) โ dom dom ๐น = ๐ด) | ||
Theorem | cnfldsrngbas 45812 | The base set of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.) |
โข ๐ = (โfld โพs ๐) โ โข (๐ โ โ โ ๐ = (Baseโ๐ )) | ||
Theorem | cnfldsrngadd 45813 | The group addition operation of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.) |
โข ๐ = (โfld โพs ๐) โ โข (๐ โ ๐ โ + = (+gโ๐ )) | ||
Theorem | cnfldsrngmul 45814 | The ring multiplication operation of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.) |
โข ๐ = (โfld โพs ๐) โ โข (๐ โ ๐ โ ยท = (.rโ๐ )) | ||
Theorem | plusfreseq 45815 | If the empty set is not contained in the range of the group addition function of an extensible structure (not necessarily a magma), the restriction of the addition operation to (the Cartesian square of) the base set is the functionalization of it. (Contributed by AV, 28-Jan-2020.) |
โข ๐ต = (Baseโ๐) & โข + = (+gโ๐) & โข โจฃ = (+๐โ๐) โ โข (โ โ ran โจฃ โ ( + โพ (๐ต ร ๐ต)) = โจฃ ) | ||
Theorem | mgmplusfreseq 45816 | If the empty set is not contained in the base set of a magma, the restriction of the addition operation to (the Cartesian square of) the base set is the functionalization of it. (Contributed by AV, 28-Jan-2020.) |
โข ๐ต = (Baseโ๐) & โข + = (+gโ๐) & โข โจฃ = (+๐โ๐) โ โข ((๐ โ Mgm โง โ โ ๐ต) โ ( + โพ (๐ต ร ๐ต)) = โจฃ ) | ||
Theorem | 0mgm 45817 | A set with an empty base set is always a magma. (Contributed by AV, 25-Feb-2020.) |
โข (Baseโ๐) = โ โ โข (๐ โ ๐ โ ๐ โ Mgm) | ||
Theorem | mgmpropd 45818* | 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 45819* | Deduce a magma from its properties. (Contributed by AV, 25-Feb-2020.) |
โข (๐ โ ๐ต = (Baseโ๐บ)) & โข (๐ โ ๐บ โ ๐) & โข (๐ โ + = (+gโ๐บ)) & โข ((๐ โง ๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ฅ + ๐ฆ) โ ๐ต) โ โข (๐ โ ๐บ โ Mgm) | ||
Syntax | cmgmhm 45820 | Hom-set generator class for magmas. |
class MgmHom | ||
Syntax | csubmgm 45821 | Class function taking a magma to its lattice of submagmas. |
class SubMgm | ||
Definition | df-mgmhm 45822* | A magma homomorphism is a function on the base sets which preserves the binary operation. (Contributed by AV, 24-Feb-2020.) |
โข MgmHom = (๐ โ Mgm, ๐ก โ Mgm โฆ {๐ โ ((Baseโ๐ก) โm (Baseโ๐ )) โฃ โ๐ฅ โ (Baseโ๐ )โ๐ฆ โ (Baseโ๐ )(๐โ(๐ฅ(+gโ๐ )๐ฆ)) = ((๐โ๐ฅ)(+gโ๐ก)(๐โ๐ฆ))}) | ||
Definition | df-submgm 45823* | A submagma is a subset of a magma which is closed under the operation. Such subsets are themselves magmas. (Contributed by AV, 24-Feb-2020.) |
โข SubMgm = (๐ โ Mgm โฆ {๐ก โ ๐ซ (Baseโ๐ ) โฃ โ๐ฅ โ ๐ก โ๐ฆ โ ๐ก (๐ฅ(+gโ๐ )๐ฆ) โ ๐ก}) | ||
Theorem | mgmhmrcl 45824 | Reverse closure of a magma homomorphism. (Contributed by AV, 24-Feb-2020.) |
โข (๐น โ (๐ MgmHom ๐) โ (๐ โ Mgm โง ๐ โ Mgm)) | ||
Theorem | submgmrcl 45825 | Reverse closure for submagmas. (Contributed by AV, 24-Feb-2020.) |
โข (๐ โ (SubMgmโ๐) โ ๐ โ Mgm) | ||
Theorem | ismgmhm 45826* | Property of a magma homomorphism. (Contributed by AV, 25-Feb-2020.) |
โข ๐ต = (Baseโ๐) & โข ๐ถ = (Baseโ๐) & โข + = (+gโ๐) & โข โจฃ = (+gโ๐) โ โข (๐น โ (๐ MgmHom ๐) โ ((๐ โ Mgm โง ๐ โ Mgm) โง (๐น:๐ตโถ๐ถ โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐นโ(๐ฅ + ๐ฆ)) = ((๐นโ๐ฅ) โจฃ (๐นโ๐ฆ))))) | ||
Theorem | mgmhmf 45827 | A magma homomorphism is a function. (Contributed by AV, 25-Feb-2020.) |
โข ๐ต = (Baseโ๐) & โข ๐ถ = (Baseโ๐) โ โข (๐น โ (๐ MgmHom ๐) โ ๐น:๐ตโถ๐ถ) | ||
Theorem | mgmhmpropd 45828* | Magma homomorphism depends only on the operation of structures. (Contributed by AV, 25-Feb-2020.) |
โข (๐ โ ๐ต = (Baseโ๐ฝ)) & โข (๐ โ ๐ถ = (Baseโ๐พ)) & โข (๐ โ ๐ต = (Baseโ๐ฟ)) & โข (๐ โ ๐ถ = (Baseโ๐)) & โข (๐ โ ๐ต โ โ ) & โข (๐ โ ๐ถ โ โ ) & โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ฅ(+gโ๐ฝ)๐ฆ) = (๐ฅ(+gโ๐ฟ)๐ฆ)) & โข ((๐ โง (๐ฅ โ ๐ถ โง ๐ฆ โ ๐ถ)) โ (๐ฅ(+gโ๐พ)๐ฆ) = (๐ฅ(+gโ๐)๐ฆ)) โ โข (๐ โ (๐ฝ MgmHom ๐พ) = (๐ฟ MgmHom ๐)) | ||
Theorem | mgmhmlin 45829 | A magma homomorphism preserves the binary operation. (Contributed by AV, 25-Feb-2020.) |
โข ๐ต = (Baseโ๐) & โข + = (+gโ๐) & โข โจฃ = (+gโ๐) โ โข ((๐น โ (๐ MgmHom ๐) โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐นโ(๐ + ๐)) = ((๐นโ๐) โจฃ (๐นโ๐))) | ||
Theorem | mgmhmf1o 45830 | A magma homomorphism is bijective iff its converse is also a magma homomorphism. (Contributed by AV, 25-Feb-2020.) |
โข ๐ต = (Baseโ๐ ) & โข ๐ถ = (Baseโ๐) โ โข (๐น โ (๐ MgmHom ๐) โ (๐น:๐ตโ1-1-ontoโ๐ถ โ โก๐น โ (๐ MgmHom ๐ ))) | ||
Theorem | idmgmhm 45831 | The identity homomorphism on a magma. (Contributed by AV, 27-Feb-2020.) |
โข ๐ต = (Baseโ๐) โ โข (๐ โ Mgm โ ( I โพ ๐ต) โ (๐ MgmHom ๐)) | ||
Theorem | issubmgm 45832* | Expand definition of a submagma. (Contributed by AV, 25-Feb-2020.) |
โข ๐ต = (Baseโ๐) & โข + = (+gโ๐) โ โข (๐ โ Mgm โ (๐ โ (SubMgmโ๐) โ (๐ โ ๐ต โง โ๐ฅ โ ๐ โ๐ฆ โ ๐ (๐ฅ + ๐ฆ) โ ๐))) | ||
Theorem | issubmgm2 45833 | Submagmas are subsets that are also magmas. (Contributed by AV, 25-Feb-2020.) |
โข ๐ต = (Baseโ๐) & โข ๐ป = (๐ โพs ๐) โ โข (๐ โ Mgm โ (๐ โ (SubMgmโ๐) โ (๐ โ ๐ต โง ๐ป โ Mgm))) | ||
Theorem | rabsubmgmd 45834* | Deduction for proving that a restricted class abstraction is a submagma. (Contributed by AV, 26-Feb-2020.) |
โข ๐ต = (Baseโ๐) & โข + = (+gโ๐) & โข (๐ โ ๐ โ Mgm) & โข ((๐ โง ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โง (๐ โง ๐))) โ ๐) & โข (๐ง = ๐ฅ โ (๐ โ ๐)) & โข (๐ง = ๐ฆ โ (๐ โ ๐)) & โข (๐ง = (๐ฅ + ๐ฆ) โ (๐ โ ๐)) โ โข (๐ โ {๐ง โ ๐ต โฃ ๐} โ (SubMgmโ๐)) | ||
Theorem | submgmss 45835 | Submagmas are subsets of the base set. (Contributed by AV, 26-Feb-2020.) |
โข ๐ต = (Baseโ๐) โ โข (๐ โ (SubMgmโ๐) โ ๐ โ ๐ต) | ||
Theorem | submgmid 45836 | Every magma is trivially a submagma of itself. (Contributed by AV, 26-Feb-2020.) |
โข ๐ต = (Baseโ๐) โ โข (๐ โ Mgm โ ๐ต โ (SubMgmโ๐)) | ||
Theorem | submgmcl 45837 | Submagmas are closed under the monoid operation. (Contributed by AV, 26-Feb-2020.) |
โข + = (+gโ๐) โ โข ((๐ โ (SubMgmโ๐) โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ + ๐) โ ๐) | ||
Theorem | submgmmgm 45838 | Submagmas are themselves magmas under the given operation. (Contributed by AV, 26-Feb-2020.) |
โข ๐ป = (๐ โพs ๐) โ โข (๐ โ (SubMgmโ๐) โ ๐ป โ Mgm) | ||
Theorem | submgmbas 45839 | The base set of a submagma. (Contributed by AV, 26-Feb-2020.) |
โข ๐ป = (๐ โพs ๐) โ โข (๐ โ (SubMgmโ๐) โ ๐ = (Baseโ๐ป)) | ||
Theorem | subsubmgm 45840 | A submagma of a submagma is a submagma. (Contributed by AV, 26-Feb-2020.) |
โข ๐ป = (๐บ โพs ๐) โ โข (๐ โ (SubMgmโ๐บ) โ (๐ด โ (SubMgmโ๐ป) โ (๐ด โ (SubMgmโ๐บ) โง ๐ด โ ๐))) | ||
Theorem | resmgmhm 45841 | Restriction of a magma homomorphism to a submagma is a homomorphism. (Contributed by AV, 26-Feb-2020.) |
โข ๐ = (๐ โพs ๐) โ โข ((๐น โ (๐ MgmHom ๐) โง ๐ โ (SubMgmโ๐)) โ (๐น โพ ๐) โ (๐ MgmHom ๐)) | ||
Theorem | resmgmhm2 45842 | One direction of resmgmhm2b 45843. (Contributed by AV, 26-Feb-2020.) |
โข ๐ = (๐ โพs ๐) โ โข ((๐น โ (๐ MgmHom ๐) โง ๐ โ (SubMgmโ๐)) โ ๐น โ (๐ MgmHom ๐)) | ||
Theorem | resmgmhm2b 45843 | Restriction of the codomain of a homomorphism. (Contributed by AV, 26-Feb-2020.) |
โข ๐ = (๐ โพs ๐) โ โข ((๐ โ (SubMgmโ๐) โง ran ๐น โ ๐) โ (๐น โ (๐ MgmHom ๐) โ ๐น โ (๐ MgmHom ๐))) | ||
Theorem | mgmhmco 45844 | The composition of magma homomorphisms is a homomorphism. (Contributed by AV, 27-Feb-2020.) |
โข ((๐น โ (๐ MgmHom ๐) โง ๐บ โ (๐ MgmHom ๐)) โ (๐น โ ๐บ) โ (๐ MgmHom ๐)) | ||
Theorem | mgmhmima 45845 | The homomorphic image of a submagma is a submagma. (Contributed by AV, 27-Feb-2020.) |
โข ((๐น โ (๐ MgmHom ๐) โง ๐ โ (SubMgmโ๐)) โ (๐น โ ๐) โ (SubMgmโ๐)) | ||
Theorem | mgmhmeql 45846 | The equalizer of two magma homomorphisms is a submagma. (Contributed by AV, 27-Feb-2020.) |
โข ((๐น โ (๐ MgmHom ๐) โง ๐บ โ (๐ MgmHom ๐)) โ dom (๐น โฉ ๐บ) โ (SubMgmโ๐)) | ||
Theorem | submgmacs 45847 | Submagmas are an algebraic closure system. (Contributed by AV, 27-Feb-2020.) |
โข ๐ต = (Baseโ๐บ) โ โข (๐บ โ Mgm โ (SubMgmโ๐บ) โ (ACSโ๐ต)) | ||
Theorem | ismhm0 45848 | Property of a monoid homomorphism, expressed by a magma homomorphism. (Contributed by AV, 17-Apr-2020.) |
โข ๐ต = (Baseโ๐) & โข ๐ถ = (Baseโ๐) & โข + = (+gโ๐) & โข โจฃ = (+gโ๐) & โข 0 = (0gโ๐) & โข ๐ = (0gโ๐) โ โข (๐น โ (๐ MndHom ๐) โ ((๐ โ Mnd โง ๐ โ Mnd) โง (๐น โ (๐ MgmHom ๐) โง (๐นโ 0 ) = ๐))) | ||
Theorem | mhmismgmhm 45849 | Each monoid homomorphism is a magma homomorphism. (Contributed by AV, 29-Feb-2020.) |
โข (๐น โ (๐ MndHom ๐) โ ๐น โ (๐ MgmHom ๐)) | ||
Theorem | opmpoismgm 45850* | A structure with a group addition operation in maps-to notation is a magma if the operation value is contained in the base set. (Contributed by AV, 16-Feb-2020.) |
โข ๐ต = (Baseโ๐) & โข (+gโ๐) = (๐ฅ โ ๐ต, ๐ฆ โ ๐ต โฆ ๐ถ) & โข (๐ โ ๐ต โ โ ) & โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ถ โ ๐ต) โ โข (๐ โ ๐ โ Mgm) | ||
Theorem | copissgrp 45851* | A structure with a constant group addition operation is a semigroup if the constant is contained in the base set. (Contributed by AV, 16-Feb-2020.) |
โข ๐ต = (Baseโ๐) & โข (+gโ๐) = (๐ฅ โ ๐ต, ๐ฆ โ ๐ต โฆ ๐ถ) & โข (๐ โ ๐ต โ โ ) & โข (๐ โ ๐ถ โ ๐ต) โ โข (๐ โ ๐ โ Smgrp) | ||
Theorem | copisnmnd 45852* | A structure with a constant group addition operation and at least two elements is not a monoid. (Contributed by AV, 16-Feb-2020.) |
โข ๐ต = (Baseโ๐) & โข (+gโ๐) = (๐ฅ โ ๐ต, ๐ฆ โ ๐ต โฆ ๐ถ) & โข (๐ โ ๐ถ โ ๐ต) & โข (๐ โ 1 < (โฏโ๐ต)) โ โข (๐ โ ๐ โ Mnd) | ||
Theorem | 0nodd 45853* | 0 is not an odd integer. (Contributed by AV, 3-Feb-2020.) |
โข ๐ = {๐ง โ โค โฃ โ๐ฅ โ โค ๐ง = ((2 ยท ๐ฅ) + 1)} โ โข 0 โ ๐ | ||
Theorem | 1odd 45854* | 1 is an odd integer. (Contributed by AV, 3-Feb-2020.) |
โข ๐ = {๐ง โ โค โฃ โ๐ฅ โ โค ๐ง = ((2 ยท ๐ฅ) + 1)} โ โข 1 โ ๐ | ||
Theorem | 2nodd 45855* | 2 is not an odd integer. (Contributed by AV, 3-Feb-2020.) |
โข ๐ = {๐ง โ โค โฃ โ๐ฅ โ โค ๐ง = ((2 ยท ๐ฅ) + 1)} โ โข 2 โ ๐ | ||
Theorem | oddibas 45856* | Lemma 1 for oddinmgm 45858: The base set of M is the set of all odd integers. (Contributed by AV, 3-Feb-2020.) |
โข ๐ = {๐ง โ โค โฃ โ๐ฅ โ โค ๐ง = ((2 ยท ๐ฅ) + 1)} & โข ๐ = (โfld โพs ๐) โ โข ๐ = (Baseโ๐) | ||
Theorem | oddiadd 45857* | Lemma 2 for oddinmgm 45858: The group addition operation of M is the addition of complex numbers. (Contributed by AV, 3-Feb-2020.) |
โข ๐ = {๐ง โ โค โฃ โ๐ฅ โ โค ๐ง = ((2 ยท ๐ฅ) + 1)} & โข ๐ = (โfld โพs ๐) โ โข + = (+gโ๐) | ||
Theorem | oddinmgm 45858* | The structure of all odd integers together with the addition of complex numbers is not a magma. Remark: the structure of the complementary subset of the set of integers, the even integers, is a magma, actually an abelian group, see 2zrngaabl 45991, and even a non-unital ring, see 2zrng 45982. (Contributed by AV, 3-Feb-2020.) |
โข ๐ = {๐ง โ โค โฃ โ๐ฅ โ โค ๐ง = ((2 ยท ๐ฅ) + 1)} & โข ๐ = (โfld โพs ๐) โ โข ๐ โ Mgm | ||
Theorem | nnsgrpmgm 45859 | The structure of positive integers together with the addition of complex numbers is a magma. (Contributed by AV, 4-Feb-2020.) |
โข ๐ = (โfld โพs โ) โ โข ๐ โ Mgm | ||
Theorem | nnsgrp 45860 | The structure of positive integers together with the addition of complex numbers is a semigroup. (Contributed by AV, 4-Feb-2020.) |
โข ๐ = (โfld โพs โ) โ โข ๐ โ Smgrp | ||
Theorem | nnsgrpnmnd 45861 | The structure of positive integers together with the addition of complex numbers is not a monoid. (Contributed by AV, 4-Feb-2020.) |
โข ๐ = (โfld โพs โ) โ โข ๐ โ Mnd | ||
Theorem | nn0mnd 45862 | The set of nonnegative integers under (complex) addition is a monoid. Example in [Lang] p. 6. Remark: ๐ could have also been written as (โfld โพs โ0). (Contributed by AV, 27-Dec-2023.) |
โข ๐ = {โจ(Baseโndx), โ0โฉ, โจ(+gโndx), + โฉ} โ โข ๐ โ Mnd | ||
Theorem | gsumsplit2f 45863* | Split a group sum into two parts. (Contributed by AV, 4-Sep-2019.) |
โข โฒ๐๐ & โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข + = (+gโ๐บ) & โข (๐ โ ๐บ โ CMnd) & โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ โ ๐ต) & โข (๐ โ (๐ โ ๐ด โฆ ๐) finSupp 0 ) & โข (๐ โ (๐ถ โฉ ๐ท) = โ ) & โข (๐ โ ๐ด = (๐ถ โช ๐ท)) โ โข (๐ โ (๐บ ฮฃg (๐ โ ๐ด โฆ ๐)) = ((๐บ ฮฃg (๐ โ ๐ถ โฆ ๐)) + (๐บ ฮฃg (๐ โ ๐ท โฆ ๐)))) | ||
Theorem | gsumdifsndf 45864* | Extract a summand from a finitely supported group sum. (Contributed by AV, 4-Sep-2019.) |
โข โฒ๐๐ & โข โฒ๐๐ & โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข (๐ โ ๐บ โ CMnd) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ (๐ โ ๐ด โฆ ๐) finSupp (0gโ๐บ)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ด) & โข (๐ โ ๐ โ ๐ต) & โข ((๐ โง ๐ = ๐) โ ๐ = ๐) โ โข (๐ โ (๐บ ฮฃg (๐ โ ๐ด โฆ ๐)) = ((๐บ ฮฃg (๐ โ (๐ด โ {๐}) โฆ ๐)) + ๐)) | ||
Theorem | gsumfsupp 45865 | A group sum of a family can be restricted to the support of that family without changing its value, provided that that support is finite. This corresponds to the definition of an (infinite) product in [Lang] p. 5, last two formulas. (Contributed by AV, 27-Dec-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข ๐ผ = (๐น supp 0 ) & โข (๐ โ ๐บ โ CMnd) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐น:๐ดโถ๐ต) & โข (๐ โ ๐น finSupp 0 ) โ โข (๐ โ (๐บ ฮฃg (๐น โพ ๐ผ)) = (๐บ ฮฃg ๐น)) | ||
With df-mpo 7354, binary operations are defined by a rule, and with df-ov 7352, 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 (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, we call binary operations mapping the elements of the Cartesian product ๐ ร ๐ internal binary operations, see df-intop 45882. If, in addition, the result is also contained in the set ๐, the operation is called closed internal binary operation, see df-clintop 45883. Therefore, a "binary operation on a set ๐ " according to Wikipedia is a "closed internal binary operation" in our 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 45883 ). Taking a step back, we define "laws" applicable for "binary operations" (which even need not to be functions), according to the definition in [Hall] p. 1 and [BourbakiAlg1] p. 1, p. 4 and p. 7. These laws are used, on the one hand, to specialize internal binary operations (see df-clintop 45883 and df-assintop 45884), and on the other hand to define the common algebraic structures like magmas, groups, rings, etc. Internal binary operations, which obey these laws, are defined afterwards. Notice that in [BourbakiAlg1] p. 1, p. 4 and p. 7, these operations are called "laws" by themselves. In the following, an alternate definition df-cllaw 45869 for an internal binary operation is provided, which does not require function-ness, but only closure. Therefore, this definition could be used as binary operation (Slot 2) defined for a magma as extensible structure, see mgmplusgiopALT 45877, or for an alternate definition df-mgm2 45902 for a magma as extensible structure. Similar results are obtained for an associative operation (defining semigroups). | ||
In this subsection, the "laws" applicable for "binary operations" according to the definition in [Hall] p. 1 and [BourbakiAlg1] p. 1, p. 4 and p. 7 are defined. These laws are called "internal laws" in [BourbakiAlg1] p. xxi. | ||
Syntax | ccllaw 45866 | Extend class notation for the closure law. |
class clLaw | ||
Syntax | casslaw 45867 | Extend class notation for the associative law. |
class assLaw | ||
Syntax | ccomlaw 45868 | Extend class notation for the commutative law. |
class comLaw | ||
Definition | df-cllaw 45869* | The closure law for binary operations, see definitions of laws A0. and M0. in section 1.1 of [Hall] p. 1, or definition 1 in [BourbakiAlg1] p. 1: the value of a binary operation applied to two operands of a given sets is an element of this set. By this definition, the closure law is expressed as binary relation: a binary operation is related to a set by clLaw if the closure law holds for this binary operation regarding this set. Note that the binary operation needs not to be a function. (Contributed by AV, 7-Jan-2020.) |
โข clLaw = {โจ๐, ๐โฉ โฃ โ๐ฅ โ ๐ โ๐ฆ โ ๐ (๐ฅ๐๐ฆ) โ ๐} | ||
Definition | df-comlaw 45870* | The commutative law for binary operations, see definitions of laws A2. and M2. in section 1.1 of [Hall] p. 1, or definition 8 in [BourbakiAlg1] p. 7: the value of a binary operation applied to two operands equals the value of a binary operation applied to the two operands in reversed order. By this definition, the commutative law is expressed as binary relation: a binary operation is related to a set by comLaw if the commutative law holds for this binary operation regarding this set. Note that the binary operation needs neither to be closed nor to be a function. (Contributed by AV, 7-Jan-2020.) |
โข comLaw = {โจ๐, ๐โฉ โฃ โ๐ฅ โ ๐ โ๐ฆ โ ๐ (๐ฅ๐๐ฆ) = (๐ฆ๐๐ฅ)} | ||
Definition | df-asslaw 45871* | The associative law for binary operations, see definitions of laws A1. and M1. in section 1.1 of [Hall] p. 1, or definition 5 in [BourbakiAlg1] p. 4: the value of a binary operation applied the value of the binary operation applied to two operands and a third operand equals the value of the binary operation applied to the first operand and the value of the binary operation applied to the second and third operand. By this definition, the associative law is expressed as binary relation: a binary operation is related to a set by assLaw if the associative law holds for this binary operation regarding this set. Note that the binary operation needs neither to be closed nor to be a function. (Contributed by FL, 1-Nov-2009.) (Revised by AV, 13-Jan-2020.) |
โข assLaw = {โจ๐, ๐โฉ โฃ โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐๐ฆ)๐๐ง) = (๐ฅ๐(๐ฆ๐๐ง))} | ||
Theorem | iscllaw 45872* | The predicate "is a closed operation". (Contributed by AV, 13-Jan-2020.) |
โข (( โฌ โ ๐ โง ๐ โ ๐) โ ( โฌ clLaw ๐ โ โ๐ฅ โ ๐ โ๐ฆ โ ๐ (๐ฅ โฌ ๐ฆ) โ ๐)) | ||
Theorem | iscomlaw 45873* | The predicate "is a commutative operation". (Contributed by AV, 20-Jan-2020.) |
โข (( โฌ โ ๐ โง ๐ โ ๐) โ ( โฌ comLaw ๐ โ โ๐ฅ โ ๐ โ๐ฆ โ ๐ (๐ฅ โฌ ๐ฆ) = (๐ฆ โฌ ๐ฅ))) | ||
Theorem | clcllaw 45874 | Closure of a closed operation. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 21-Jan-2020.) |
โข (( โฌ clLaw ๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ โฌ ๐) โ ๐) | ||
Theorem | isasslaw 45875* | The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.) (Revised by AV, 13-Jan-2020.) |
โข (( โฌ โ ๐ โง ๐ โ ๐) โ ( โฌ assLaw ๐ โ โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ โฌ ๐ฆ) โฌ ๐ง) = (๐ฅ โฌ (๐ฆ โฌ ๐ง)))) | ||
Theorem | asslawass 45876* | Associativity of an associative operation. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 21-Jan-2020.) |
โข ( โฌ assLaw ๐ โ โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ โฌ ๐ฆ) โฌ ๐ง) = (๐ฅ โฌ (๐ฆ โฌ ๐ง))) | ||
Theorem | mgmplusgiopALT 45877 | Slot 2 (group operation) of a magma as extensible structure is a closed operation on the base set. (Contributed by AV, 13-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
โข (๐ โ Mgm โ (+gโ๐) clLaw (Baseโ๐)) | ||
Theorem | sgrpplusgaopALT 45878 | Slot 2 (group operation) of a semigroup as extensible structure is an associative operation on the base set. (Contributed by AV, 13-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
โข (๐บ โ Smgrp โ (+gโ๐บ) assLaw (Baseโ๐บ)) | ||
In this subsection, "internal binary operations" obeying different laws are defined. | ||
Syntax | cintop 45879 | Extend class notation with class of internal (binary) operations for a set. |
class intOp | ||
Syntax | cclintop 45880 | Extend class notation with class of closed operations for a set. |
class clIntOp | ||
Syntax | cassintop 45881 | Extend class notation with class of associative operations for a set. |
class assIntOp | ||
Definition | df-intop 45882* | Function mapping a set to the class of all internal (binary) operations for this set. (Contributed by AV, 20-Jan-2020.) |
โข intOp = (๐ โ V, ๐ โ V โฆ (๐ โm (๐ ร ๐))) | ||
Definition | df-clintop 45883 | Function mapping a set to the class of all closed (internal binary) operations for this set, see definition in section 1.2 of [Hall] p. 2, definition in section I.1 of [Bruck] p. 1, or definition 1 in [BourbakiAlg1] p. 1, where it is called "a law of composition". (Contributed by AV, 20-Jan-2020.) |
โข clIntOp = (๐ โ V โฆ (๐ intOp ๐)) | ||
Definition | df-assintop 45884* | Function mapping a set to the class of all associative (closed internal binary) operations for this set, see definition 5 in [BourbakiAlg1] p. 4, where it is called "an associative law of composition". (Contributed by AV, 20-Jan-2020.) |
โข assIntOp = (๐ โ V โฆ {๐ โ ( clIntOp โ๐) โฃ ๐ assLaw ๐}) | ||
Theorem | intopval 45885 | The internal (binary) operations for a set. (Contributed by AV, 20-Jan-2020.) |
โข ((๐ โ ๐ โง ๐ โ ๐) โ (๐ intOp ๐) = (๐ โm (๐ ร ๐))) | ||
Theorem | intop 45886 | An internal (binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
โข ( โฌ โ (๐ intOp ๐) โ โฌ :(๐ ร ๐)โถ๐) | ||
Theorem | clintopval 45887 | The closed (internal binary) operations for a set. (Contributed by AV, 20-Jan-2020.) |
โข (๐ โ ๐ โ ( clIntOp โ๐) = (๐ โm (๐ ร ๐))) | ||
Theorem | assintopval 45888* | The associative (closed internal binary) operations for a set. (Contributed by AV, 20-Jan-2020.) |
โข (๐ โ ๐ โ ( assIntOp โ๐) = {๐ โ ( clIntOp โ๐) โฃ ๐ assLaw ๐}) | ||
Theorem | assintopmap 45889* | The associative (closed internal binary) operations for a set, expressed with set exponentiation. (Contributed by AV, 20-Jan-2020.) |
โข (๐ โ ๐ โ ( assIntOp โ๐) = {๐ โ (๐ โm (๐ ร ๐)) โฃ ๐ assLaw ๐}) | ||
Theorem | isclintop 45890 | The predicate "is a closed (internal binary) operations for a set". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.) |
โข (๐ โ ๐ โ ( โฌ โ ( clIntOp โ๐) โ โฌ :(๐ ร ๐)โถ๐)) | ||
Theorem | clintop 45891 | A closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
โข ( โฌ โ ( clIntOp โ๐) โ โฌ :(๐ ร ๐)โถ๐) | ||
Theorem | assintop 45892 | An associative (closed internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
โข ( โฌ โ ( assIntOp โ๐) โ ( โฌ :(๐ ร ๐)โถ๐ โง โฌ assLaw ๐)) | ||
Theorem | isassintop 45893* | The predicate "is an associative (closed internal binary) operations for a set". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.) |
โข (๐ โ ๐ โ ( โฌ โ ( assIntOp โ๐) โ ( โฌ :(๐ ร ๐)โถ๐ โง โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ โฌ ๐ฆ) โฌ ๐ง) = (๐ฅ โฌ (๐ฆ โฌ ๐ง))))) | ||
Theorem | clintopcllaw 45894 | The closure law holds for a closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
โข ( โฌ โ ( clIntOp โ๐) โ โฌ clLaw ๐) | ||
Theorem | assintopcllaw 45895 | The closure low holds for an associative (closed internal binary) operation for a set. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.) |
โข ( โฌ โ ( assIntOp โ๐) โ โฌ clLaw ๐) | ||
Theorem | assintopasslaw 45896 | The associative low holds for a associative (closed internal binary) operation for a set. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.) |
โข ( โฌ โ ( assIntOp โ๐) โ โฌ assLaw ๐) | ||
Theorem | assintopass 45897* | An associative (closed internal binary) operation for a set is associative. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.) |
โข ( โฌ โ ( assIntOp โ๐) โ โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ โฌ ๐ฆ) โฌ ๐ง) = (๐ฅ โฌ (๐ฆ โฌ ๐ง))) | ||
Syntax | cmgm2 45898 | Extend class notation with class of all magmas. |
class MgmALT | ||
Syntax | ccmgm2 45899 | Extend class notation with class of all commutative magmas. |
class CMgmALT | ||
Syntax | csgrp2 45900 | Extend class notation with class of all semigroups. |
class SGrpALT |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |