![]() |
Metamath
Proof Explorer Theorem List (p. 466 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | isomuspgrlem2 46501* | Lemma 2 for isomuspgr 46502. (Contributed by AV, 1-Dec-2022.) |
β’ π = (Vtxβπ΄) & β’ π = (Vtxβπ΅) & β’ πΈ = (Edgβπ΄) & β’ πΎ = (Edgβπ΅) β β’ (((π΄ β USPGraph β§ π΅ β USPGraph) β§ π:πβ1-1-ontoβπ) β (βπ β π βπ β π ({π, π} β πΈ β {(πβπ), (πβπ)} β πΎ) β βπ(π:πΈβ1-1-ontoβπΎ β§ βπ β πΈ (π β π) = (πβπ)))) | ||
Theorem | isomuspgr 46502* | The isomorphy relation for two simple pseudographs. This corresponds to the definition in [Bollobas] p. 3. (Contributed by AV, 1-Dec-2022.) |
β’ π = (Vtxβπ΄) & β’ π = (Vtxβπ΅) & β’ πΈ = (Edgβπ΄) & β’ πΎ = (Edgβπ΅) β β’ ((π΄ β USPGraph β§ π΅ β USPGraph) β (π΄ IsomGr π΅ β βπ(π:πβ1-1-ontoβπ β§ βπ β π βπ β π ({π, π} β πΈ β {(πβπ), (πβπ)} β πΎ)))) | ||
Theorem | isomgrref 46503 | The isomorphy relation is reflexive for hypergraphs. (Contributed by AV, 11-Nov-2022.) |
β’ (πΊ β UHGraph β πΊ IsomGr πΊ) | ||
Theorem | isomgrsym 46504 | The isomorphy relation is symmetric for hypergraphs. (Contributed by AV, 11-Nov-2022.) |
β’ ((π΄ β UHGraph β§ π΅ β π) β (π΄ IsomGr π΅ β π΅ IsomGr π΄)) | ||
Theorem | isomgrsymb 46505 | The isomorphy relation is symmetric for hypergraphs. (Contributed by AV, 11-Nov-2022.) |
β’ ((π΄ β UHGraph β§ π΅ β UHGraph) β (π΄ IsomGr π΅ β π΅ IsomGr π΄)) | ||
Theorem | isomgrtrlem 46506* | Lemma for isomgrtr 46507. (Contributed by AV, 5-Dec-2022.) |
β’ (((((π΄ β UHGraph β§ π΅ β UHGraph β§ πΆ β π) β§ π:(Vtxβπ΄)β1-1-ontoβ(Vtxβπ΅) β§ π£:(Vtxβπ΅)β1-1-ontoβ(VtxβπΆ)) β§ (π:dom (iEdgβπ΄)β1-1-ontoβdom (iEdgβπ΅) β§ βπ β dom (iEdgβπ΄)(π β ((iEdgβπ΄)βπ)) = ((iEdgβπ΅)β(πβπ)))) β§ (π€:dom (iEdgβπ΅)β1-1-ontoβdom (iEdgβπΆ) β§ βπ β dom (iEdgβπ΅)(π£ β ((iEdgβπ΅)βπ)) = ((iEdgβπΆ)β(π€βπ)))) β βπ β dom (iEdgβπ΄)((π£ β π) β ((iEdgβπ΄)βπ)) = ((iEdgβπΆ)β((π€ β π)βπ))) | ||
Theorem | isomgrtr 46507 | The isomorphy relation is transitive for hypergraphs. (Contributed by AV, 5-Dec-2022.) |
β’ ((π΄ β UHGraph β§ π΅ β UHGraph β§ πΆ β π) β ((π΄ IsomGr π΅ β§ π΅ IsomGr πΆ) β π΄ IsomGr πΆ)) | ||
Theorem | strisomgrop 46508 | A graph represented as an extensible structure with vertices as base set and indexed edges is isomorphic to a hypergraph represented as ordered pair with the same vertices and edges. (Contributed by AV, 11-Nov-2022.) |
β’ πΊ = β¨π, πΈβ© & β’ π» = {β¨(Baseβndx), πβ©, β¨(.efβndx), πΈβ©} β β’ ((πΊ β UHGraph β§ π β π β§ πΈ β π) β πΊ IsomGr π») | ||
Theorem | ushrisomgr 46509 | A simple hypergraph (with arbitrarily indexed edges) is isomorphic to a graph with the same vertices and the same edges, indexed by the edges themselves. (Contributed by AV, 11-Nov-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π» = β¨π, ( I βΎ πΈ)β© β β’ (πΊ β USHGraph β πΊ IsomGr π») | ||
Theorem | 1hegrlfgr 46510* | A graph πΊ with one hyperedge joining at least two vertices is a loop-free graph. (Contributed by AV, 23-Feb-2021.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π΅ β πΆ) & β’ (π β πΈ β π« π) & β’ (π β (iEdgβπΊ) = {β¨π΄, πΈβ©}) & β’ (π β {π΅, πΆ} β πΈ) β β’ (π β (iEdgβπΊ):{π΄}βΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)}) | ||
Syntax | cupwlks 46511 | Extend class notation with walks (of a pseudograph). |
class UPWalks | ||
Definition | df-upwlks 46512* |
Define the set of all walks (in a pseudograph), called "simple walks"
in
the following.
According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A walk of length k in a graph is an alternating sequence of vertices and edges, v0 , e0 , v1 , e1 , v2 , ... , v(k-1) , e(k-1) , v(k) which begins and ends with vertices. If the graph is undirected, then the endpoints of e(i) are v(i) and v(i+1)." According to Bollobas: " A walk W in a graph is an alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) where e(i) = x(i-1)x(i), 0<i<=l.", see Definition of [Bollobas] p. 4. Therefore, a walk can be represented by two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices. So the walk is represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). Although this definition is also applicable for arbitrary hypergraphs, it allows only walks consisting of not proper hyperedges (i.e. edges connecting at most two vertices). Therefore, it should be used for pseudographs only. (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.) |
β’ UPWalks = (π β V β¦ {β¨π, πβ© β£ (π β Word dom (iEdgβπ) β§ π:(0...(β―βπ))βΆ(Vtxβπ) β§ βπ β (0..^(β―βπ))((iEdgβπ)β(πβπ)) = {(πβπ), (πβ(π + 1))})}) | ||
Theorem | upwlksfval 46513* | The set of simple walks (in an undirected graph). (Contributed by Alexander van der Vekens, 19-Oct-2017.) (Revised by AV, 28-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΊ β π β (UPWalksβπΊ) = {β¨π, πβ© β£ (π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})}) | ||
Theorem | isupwlk 46514* | Properties of a pair of functions to be a simple walk. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 28-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ ((πΊ β π β§ πΉ β π β§ π β π) β (πΉ(UPWalksβπΊ)π β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) | ||
Theorem | isupwlkg 46515* | Generalization of isupwlk 46514: Conditions for two classes to represent a simple walk. (Contributed by AV, 5-Nov-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΊ β π β (πΉ(UPWalksβπΊ)π β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) | ||
Theorem | upwlkbprop 46516 | Basic properties of a simple walk. (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 29-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΉ(UPWalksβπΊ)π β (πΊ β V β§ πΉ β V β§ π β V)) | ||
Theorem | upwlkwlk 46517 | A simple walk is a walk. (Contributed by AV, 30-Dec-2020.) (Proof shortened by AV, 27-Feb-2021.) |
β’ (πΉ(UPWalksβπΊ)π β πΉ(WalksβπΊ)π) | ||
Theorem | upgrwlkupwlk 46518 | In a pseudograph, a walk is a simple walk. (Contributed by AV, 30-Dec-2020.) (Proof shortened by AV, 2-Jan-2021.) |
β’ ((πΊ β UPGraph β§ πΉ(WalksβπΊ)π) β πΉ(UPWalksβπΊ)π) | ||
Theorem | upgrwlkupwlkb 46519 | In a pseudograph, the definitions for a walk and a simple walk are equivalent. (Contributed by AV, 30-Dec-2020.) |
β’ (πΊ β UPGraph β (πΉ(WalksβπΊ)π β πΉ(UPWalksβπΊ)π)) | ||
Theorem | upgrisupwlkALT 46520* | Alternate proof of upgriswlk 28898 using the definition of UPGraph and related theorems. (Contributed by AV, 2-Jan-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ ((πΊ β UPGraph β§ πΉ β π β§ π β π) β (πΉ(WalksβπΊ)π β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) | ||
Theorem | upgredgssspr 46521 | The set of edges of a pseudograph is a subset of the set of unordered pairs of vertices. (Contributed by AV, 24-Nov-2021.) |
β’ (πΊ β UPGraph β (EdgβπΊ) β (Pairsβ(VtxβπΊ))) | ||
Theorem | uspgropssxp 46522* | The set πΊ of "simple pseudographs" for a fixed set π of vertices is a subset of a Cartesian product. For more details about the class πΊ of all "simple pseudographs" see comments on uspgrbisymrel 46532. (Contributed by AV, 24-Nov-2021.) |
β’ π = π« (Pairsβπ) & β’ πΊ = {β¨π£, πβ© β£ (π£ = π β§ βπ β USPGraph ((Vtxβπ) = π£ β§ (Edgβπ) = π))} β β’ (π β π β πΊ β (π Γ π)) | ||
Theorem | uspgrsprfv 46523* | The value of the function πΉ which maps a "simple pseudograph" for a fixed set π of vertices to the set of edges (i.e. range of the edge function) of the graph. Solely for πΊ as defined here, the function πΉ is a bijection between the "simple pseudographs" and the subsets of the set of pairs π over the fixed set π of vertices, see uspgrbispr 46529. (Contributed by AV, 24-Nov-2021.) |
β’ π = π« (Pairsβπ) & β’ πΊ = {β¨π£, πβ© β£ (π£ = π β§ βπ β USPGraph ((Vtxβπ) = π£ β§ (Edgβπ) = π))} & β’ πΉ = (π β πΊ β¦ (2nd βπ)) β β’ (π β πΊ β (πΉβπ) = (2nd βπ)) | ||
Theorem | uspgrsprf 46524* | The mapping πΉ is a function from the "simple pseudographs" with a fixed set of vertices π into the subsets of the set of pairs over the set π. (Contributed by AV, 24-Nov-2021.) |
β’ π = π« (Pairsβπ) & β’ πΊ = {β¨π£, πβ© β£ (π£ = π β§ βπ β USPGraph ((Vtxβπ) = π£ β§ (Edgβπ) = π))} & β’ πΉ = (π β πΊ β¦ (2nd βπ)) β β’ πΉ:πΊβΆπ | ||
Theorem | uspgrsprf1 46525* | The mapping πΉ is a one-to-one function from the "simple pseudographs" with a fixed set of vertices π into the subsets of the set of pairs over the set π. (Contributed by AV, 25-Nov-2021.) |
β’ π = π« (Pairsβπ) & β’ πΊ = {β¨π£, πβ© β£ (π£ = π β§ βπ β USPGraph ((Vtxβπ) = π£ β§ (Edgβπ) = π))} & β’ πΉ = (π β πΊ β¦ (2nd βπ)) β β’ πΉ:πΊβ1-1βπ | ||
Theorem | uspgrsprfo 46526* | The mapping πΉ is a function from the "simple pseudographs" with a fixed set of vertices π onto the subsets of the set of pairs over the set π. (Contributed by AV, 25-Nov-2021.) |
β’ π = π« (Pairsβπ) & β’ πΊ = {β¨π£, πβ© β£ (π£ = π β§ βπ β USPGraph ((Vtxβπ) = π£ β§ (Edgβπ) = π))} & β’ πΉ = (π β πΊ β¦ (2nd βπ)) β β’ (π β π β πΉ:πΊβontoβπ) | ||
Theorem | uspgrsprf1o 46527* | The mapping πΉ is a bijection between the "simple pseudographs" with a fixed set of vertices π and the subsets of the set of pairs over the set π. See also the comments on uspgrbisymrel 46532. (Contributed by AV, 25-Nov-2021.) |
β’ π = π« (Pairsβπ) & β’ πΊ = {β¨π£, πβ© β£ (π£ = π β§ βπ β USPGraph ((Vtxβπ) = π£ β§ (Edgβπ) = π))} & β’ πΉ = (π β πΊ β¦ (2nd βπ)) β β’ (π β π β πΉ:πΊβ1-1-ontoβπ) | ||
Theorem | uspgrex 46528* | 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 46529* | 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 46530* | 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 46531* | 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 46532. (Contributed by AV, 27-Nov-2021.) |
β’ πΊ = {β¨π£, πβ© β£ (π£ = π β§ βπ β USPGraph ((Vtxβπ) = π£ β§ (Edgβπ) = π))} & β’ π = {π β π« (π Γ π) β£ βπ₯ β π βπ¦ β π (π₯ππ¦ β π¦ππ₯)} β β’ (π β π β πΊ β π ) | ||
Theorem | uspgrbisymrel 46532* |
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 46528) 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 46533* | Alternate proof of uspgrbisymrel 46532 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 46534 | 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 6935. (Contributed by AV, 27-Jan-2020.) |
β’ ((π΄πΉπ΅) β β β (β¨π΄, π΅β© β dom πΉ β§ Fun (πΉ βΎ {β¨π΄, π΅β©}))) | ||
Theorem | xpsnopab 46535* | A Cartesian product with a singleton expressed as ordered-pair class abstraction. (Contributed by AV, 27-Jan-2020.) |
β’ ({π} Γ πΆ) = {β¨π, πβ© β£ (π = π β§ π β πΆ)} | ||
Theorem | xpiun 46536* | A Cartesian product expressed as indexed union of ordered-pair class abstractions. (Contributed by AV, 27-Jan-2020.) |
β’ (π΅ Γ πΆ) = βͺ π₯ β π΅ {β¨π, πβ© β£ (π = π₯ β§ π β πΆ)} | ||
Theorem | ovn0ssdmfun 46537* | 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 6935. (Contributed by AV, 27-Jan-2020.) |
β’ (βπ β π· βπ β πΈ (ππΉπ) β β β ((π· Γ πΈ) β dom πΉ β§ Fun (πΉ βΎ (π· Γ πΈ)))) | ||
Theorem | fnxpdmdm 46538 | The domain of the domain of a function over a Cartesian square. (Contributed by AV, 13-Jan-2020.) |
β’ (πΉ Fn (π΄ Γ π΄) β dom dom πΉ = π΄) | ||
Theorem | cnfldsrngbas 46539 | The base set of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.) |
β’ π = (βfld βΎs π) β β’ (π β β β π = (Baseβπ )) | ||
Theorem | cnfldsrngadd 46540 | The group addition operation of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.) |
β’ π = (βfld βΎs π) β β’ (π β π β + = (+gβπ )) | ||
Theorem | cnfldsrngmul 46541 | The ring multiplication operation of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.) |
β’ π = (βfld βΎs π) β β’ (π β π β Β· = (.rβπ )) | ||
Theorem | plusfreseq 46542 | 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 46543 | 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 46544 | A set with an empty base set is always a magma. (Contributed by AV, 25-Feb-2020.) |
β’ (Baseβπ) = β β β’ (π β π β π β Mgm) | ||
Theorem | mgmpropd 46545* | 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 46546* | Deduce a magma from its properties. (Contributed by AV, 25-Feb-2020.) |
β’ (π β π΅ = (BaseβπΊ)) & β’ (π β πΊ β π) & β’ (π β + = (+gβπΊ)) & β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) β π΅) β β’ (π β πΊ β Mgm) | ||
Syntax | cmgmhm 46547 | Hom-set generator class for magmas. |
class MgmHom | ||
Syntax | csubmgm 46548 | Class function taking a magma to its lattice of submagmas. |
class SubMgm | ||
Definition | df-mgmhm 46549* | 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 46550* | 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 46551 | Reverse closure of a magma homomorphism. (Contributed by AV, 24-Feb-2020.) |
β’ (πΉ β (π MgmHom π) β (π β Mgm β§ π β Mgm)) | ||
Theorem | submgmrcl 46552 | Reverse closure for submagmas. (Contributed by AV, 24-Feb-2020.) |
β’ (π β (SubMgmβπ) β π β Mgm) | ||
Theorem | ismgmhm 46553* | Property of a magma homomorphism. (Contributed by AV, 25-Feb-2020.) |
β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) β β’ (πΉ β (π MgmHom π) β ((π β Mgm β§ π β Mgm) β§ (πΉ:π΅βΆπΆ β§ βπ₯ β π΅ βπ¦ β π΅ (πΉβ(π₯ + π¦)) = ((πΉβπ₯) ⨣ (πΉβπ¦))))) | ||
Theorem | mgmhmf 46554 | A magma homomorphism is a function. (Contributed by AV, 25-Feb-2020.) |
β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π MgmHom π) β πΉ:π΅βΆπΆ) | ||
Theorem | mgmhmpropd 46555* | 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 46556 | A magma homomorphism preserves the binary operation. (Contributed by AV, 25-Feb-2020.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) β β’ ((πΉ β (π MgmHom π) β§ π β π΅ β§ π β π΅) β (πΉβ(π + π)) = ((πΉβπ) ⨣ (πΉβπ))) | ||
Theorem | mgmhmf1o 46557 | 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 46558 | The identity homomorphism on a magma. (Contributed by AV, 27-Feb-2020.) |
β’ π΅ = (Baseβπ) β β’ (π β Mgm β ( I βΎ π΅) β (π MgmHom π)) | ||
Theorem | issubmgm 46559* | Expand definition of a submagma. (Contributed by AV, 25-Feb-2020.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) β β’ (π β Mgm β (π β (SubMgmβπ) β (π β π΅ β§ βπ₯ β π βπ¦ β π (π₯ + π¦) β π))) | ||
Theorem | issubmgm2 46560 | Submagmas are subsets that are also magmas. (Contributed by AV, 25-Feb-2020.) |
β’ π΅ = (Baseβπ) & β’ π» = (π βΎs π) β β’ (π β Mgm β (π β (SubMgmβπ) β (π β π΅ β§ π» β Mgm))) | ||
Theorem | rabsubmgmd 46561* | Deduction for proving that a restricted class abstraction is a submagma. (Contributed by AV, 26-Feb-2020.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β π β Mgm) & β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π β§ π))) β π) & β’ (π§ = π₯ β (π β π)) & β’ (π§ = π¦ β (π β π)) & β’ (π§ = (π₯ + π¦) β (π β π)) β β’ (π β {π§ β π΅ β£ π} β (SubMgmβπ)) | ||
Theorem | submgmss 46562 | Submagmas are subsets of the base set. (Contributed by AV, 26-Feb-2020.) |
β’ π΅ = (Baseβπ) β β’ (π β (SubMgmβπ) β π β π΅) | ||
Theorem | submgmid 46563 | Every magma is trivially a submagma of itself. (Contributed by AV, 26-Feb-2020.) |
β’ π΅ = (Baseβπ) β β’ (π β Mgm β π΅ β (SubMgmβπ)) | ||
Theorem | submgmcl 46564 | Submagmas are closed under the magma operation. (Contributed by AV, 26-Feb-2020.) |
β’ + = (+gβπ) β β’ ((π β (SubMgmβπ) β§ π β π β§ π β π) β (π + π) β π) | ||
Theorem | submgmmgm 46565 | Submagmas are themselves magmas under the given operation. (Contributed by AV, 26-Feb-2020.) |
β’ π» = (π βΎs π) β β’ (π β (SubMgmβπ) β π» β Mgm) | ||
Theorem | submgmbas 46566 | The base set of a submagma. (Contributed by AV, 26-Feb-2020.) |
β’ π» = (π βΎs π) β β’ (π β (SubMgmβπ) β π = (Baseβπ»)) | ||
Theorem | subsubmgm 46567 | A submagma of a submagma is a submagma. (Contributed by AV, 26-Feb-2020.) |
β’ π» = (πΊ βΎs π) β β’ (π β (SubMgmβπΊ) β (π΄ β (SubMgmβπ») β (π΄ β (SubMgmβπΊ) β§ π΄ β π))) | ||
Theorem | resmgmhm 46568 | Restriction of a magma homomorphism to a submagma is a homomorphism. (Contributed by AV, 26-Feb-2020.) |
β’ π = (π βΎs π) β β’ ((πΉ β (π MgmHom π) β§ π β (SubMgmβπ)) β (πΉ βΎ π) β (π MgmHom π)) | ||
Theorem | resmgmhm2 46569 | One direction of resmgmhm2b 46570. (Contributed by AV, 26-Feb-2020.) |
β’ π = (π βΎs π) β β’ ((πΉ β (π MgmHom π) β§ π β (SubMgmβπ)) β πΉ β (π MgmHom π)) | ||
Theorem | resmgmhm2b 46570 | Restriction of the codomain of a homomorphism. (Contributed by AV, 26-Feb-2020.) |
β’ π = (π βΎs π) β β’ ((π β (SubMgmβπ) β§ ran πΉ β π) β (πΉ β (π MgmHom π) β πΉ β (π MgmHom π))) | ||
Theorem | mgmhmco 46571 | The composition of magma homomorphisms is a homomorphism. (Contributed by AV, 27-Feb-2020.) |
β’ ((πΉ β (π MgmHom π) β§ πΊ β (π MgmHom π)) β (πΉ β πΊ) β (π MgmHom π)) | ||
Theorem | mgmhmima 46572 | The homomorphic image of a submagma is a submagma. (Contributed by AV, 27-Feb-2020.) |
β’ ((πΉ β (π MgmHom π) β§ π β (SubMgmβπ)) β (πΉ β π) β (SubMgmβπ)) | ||
Theorem | mgmhmeql 46573 | The equalizer of two magma homomorphisms is a submagma. (Contributed by AV, 27-Feb-2020.) |
β’ ((πΉ β (π MgmHom π) β§ πΊ β (π MgmHom π)) β dom (πΉ β© πΊ) β (SubMgmβπ)) | ||
Theorem | submgmacs 46574 | Submagmas are an algebraic closure system. (Contributed by AV, 27-Feb-2020.) |
β’ π΅ = (BaseβπΊ) β β’ (πΊ β Mgm β (SubMgmβπΊ) β (ACSβπ΅)) | ||
Theorem | ismhm0 46575 | 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 46576 | Each monoid homomorphism is a magma homomorphism. (Contributed by AV, 29-Feb-2020.) |
β’ (πΉ β (π MndHom π) β πΉ β (π MgmHom π)) | ||
Theorem | opmpoismgm 46577* | 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 46578* | 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 46579* | 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 46580* | 0 is not an odd integer. (Contributed by AV, 3-Feb-2020.) |
β’ π = {π§ β β€ β£ βπ₯ β β€ π§ = ((2 Β· π₯) + 1)} β β’ 0 β π | ||
Theorem | 1odd 46581* | 1 is an odd integer. (Contributed by AV, 3-Feb-2020.) |
β’ π = {π§ β β€ β£ βπ₯ β β€ π§ = ((2 Β· π₯) + 1)} β β’ 1 β π | ||
Theorem | 2nodd 46582* | 2 is not an odd integer. (Contributed by AV, 3-Feb-2020.) |
β’ π = {π§ β β€ β£ βπ₯ β β€ π§ = ((2 Β· π₯) + 1)} β β’ 2 β π | ||
Theorem | oddibas 46583* | Lemma 1 for oddinmgm 46585: 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 46584* | Lemma 2 for oddinmgm 46585: 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 46585* | 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 46842, and even a non-unital ring, see 2zrng 46833. (Contributed by AV, 3-Feb-2020.) |
β’ π = {π§ β β€ β£ βπ₯ β β€ π§ = ((2 Β· π₯) + 1)} & β’ π = (βfld βΎs π) β β’ π β Mgm | ||
Theorem | nnsgrpmgm 46586 | 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 46587 | 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 46588 | 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 46589 | 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 46590* | 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 46591* | Extract a summand from a finitely supported group sum. (Contributed by AV, 4-Sep-2019.) |
β’ β²ππ & β’ β²ππ & β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β (π β π΄ β¦ π) finSupp (0gβπΊ)) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β π β π΄) & β’ (π β π β π΅) & β’ ((π β§ π = π) β π = π) β β’ (π β (πΊ Ξ£g (π β π΄ β¦ π)) = ((πΊ Ξ£g (π β (π΄ β {π}) β¦ π)) + π)) | ||
Theorem | gsumfsupp 46592 | 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 7414, binary operations are defined by a rule, and with df-ov 7412, 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 46609. If, in addition, the result is also contained in the set π, the operation is called closed internal binary operation, see df-clintop 46610. 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 46610 ). 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 46610 and df-assintop 46611), 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 46596 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 46604, or for an alternate definition df-mgm2 46629 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 46593 | Extend class notation for the closure law. |
class clLaw | ||
Syntax | casslaw 46594 | Extend class notation for the associative law. |
class assLaw | ||
Syntax | ccomlaw 46595 | Extend class notation for the commutative law. |
class comLaw | ||
Definition | df-cllaw 46596* | 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 46597* | 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 46598* | 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 46599* | The predicate "is a closed operation". (Contributed by AV, 13-Jan-2020.) |
β’ (( β¬ β π β§ π β π) β ( β¬ clLaw π β βπ₯ β π βπ¦ β π (π₯ β¬ π¦) β π)) | ||
Theorem | iscomlaw 46600* | The predicate "is a commutative operation". (Contributed by AV, 20-Jan-2020.) |
β’ (( β¬ β π β§ π β π) β ( β¬ comLaw π β βπ₯ β π βπ¦ β π (π₯ β¬ π¦) = (π¦ β¬ π₯))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |