![]() |
Metamath
Proof Explorer Theorem List (p. 472 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | grimco 47101 | The composition of graph isomorphisms is a graph isomorphism. (Contributed by AV, 3-May-2025.) |
β’ ((πΉ β (π GraphIso π) β§ πΊ β (π GraphIso π)) β (πΉ β πΊ) β (π GraphIso π)) | ||
Theorem | brgric 47102 | The relation "is isomorphic to" for graphs. (Contributed by AV, 28-Apr-2025.) |
β’ (π βππ π β (π GraphIso π) β β ) | ||
Theorem | brgrici 47103 | Prove that two graphs are isomorphic by an explicit isomorphism. (Contributed by AV, 28-Apr-2025.) |
β’ (πΉ β (π GraphIso π) β π βππ π) | ||
Theorem | dfgric2 47104* | Alternate, explicit definition of the "is isomorphic to" relation for two graphs. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 5-May-2025.) |
β’ π = (Vtxβπ΄) & β’ π = (Vtxβπ΅) & β’ πΌ = (iEdgβπ΄) & β’ π½ = (iEdgβπ΅) β β’ ((π΄ β π β§ π΅ β π) β (π΄ βππ π΅ β βπ(π:πβ1-1-ontoβπ β§ βπ(π:dom πΌβ1-1-ontoβdom π½ β§ βπ β dom πΌ(π β (πΌβπ)) = (π½β(πβπ)))))) | ||
Theorem | gricbri 47105* | Implications of two graphs being isomorphic. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 5-May-2025.) |
β’ π = (Vtxβπ΄) & β’ π = (Vtxβπ΅) & β’ πΌ = (iEdgβπ΄) & β’ π½ = (iEdgβπ΅) β β’ (π΄ βππ π΅ β βπ(π:πβ1-1-ontoβπ β§ βπ(π:dom πΌβ1-1-ontoβdom π½ β§ βπ β dom πΌ(π β (πΌβπ)) = (π½β(πβπ))))) | ||
Theorem | gricushgr 47106* | The "is isomorphic to" relation for two simple hypergraphs. (Contributed by AV, 28-Nov-2022.) |
β’ π = (Vtxβπ΄) & β’ π = (Vtxβπ΅) & β’ πΈ = (Edgβπ΄) & β’ πΎ = (Edgβπ΅) β β’ ((π΄ β USHGraph β§ π΅ β USHGraph) β (π΄ βππ π΅ β βπ(π:πβ1-1-ontoβπ β§ βπ(π:πΈβ1-1-ontoβπΎ β§ βπ β πΈ (π β π) = (πβπ))))) | ||
Theorem | gricuspgr 47107* | The "is isomorphic to" relation for two simple pseudographs. This corresponds to the definition in [Bollobas] p. 3. (Contributed by AV, 1-Dec-2022.) (Proof shortened by AV, 5-May-2025.) |
β’ π = (Vtxβπ΄) & β’ π = (Vtxβπ΅) & β’ πΈ = (Edgβπ΄) & β’ πΎ = (Edgβπ΅) β β’ ((π΄ β USPGraph β§ π΅ β USPGraph) β (π΄ βππ π΅ β βπ(π:πβ1-1-ontoβπ β§ βπ β π βπ β π ({π, π} β πΈ β {(πβπ), (πβπ)} β πΎ)))) | ||
Theorem | gricrel 47108 | The "is isomorphic to" relation for graphs is a relation. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 5-May-2025.) |
β’ Rel βππ | ||
Theorem | gricref 47109 | Graph isomorphism is reflexive for hypergraphs. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 29-Apr-2025.) |
β’ (πΊ β UHGraph β πΊ βππ πΊ) | ||
Theorem | gricsym 47110 | Graph isomorphism is symmetric for hypergraphs. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 3-May-2025.) |
β’ (πΊ β UHGraph β (πΊ βππ π β π βππ πΊ)) | ||
Theorem | gricsymb 47111 | Graph isomorphism is symmetric in both directions for hypergraphs. (Contributed by AV, 11-Nov-2022.) (Proof shortened by AV, 3-May-2025.) |
β’ ((π΄ β UHGraph β§ π΅ β UHGraph) β (π΄ βππ π΅ β π΅ βππ π΄)) | ||
Theorem | grictr 47112 | Graph isomorphism is transitive. (Contributed by AV, 5-Dec-2022.) (Revised by AV, 3-May-2025.) |
β’ ((π βππ π β§ π βππ π) β π βππ π) | ||
Theorem | gricer 47113 | Isomorphism is an equivalence relation on hypergraphs. (Contributed by AV, 3-May-2025.) |
β’ ( βππ β© (UHGraph Γ UHGraph)) Er UHGraph | ||
Theorem | gricen 47114 | Isomorphic graphs have equinumerous sets of vertices. (Contributed by AV, 3-May-2025.) |
β’ π΅ = (Vtxβπ ) & β’ πΆ = (Vtxβπ) β β’ (π βππ π β π΅ β πΆ) | ||
Theorem | opstrgric 47115 | 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.) (Revised by AV, 4-May-2025.) |
β’ πΊ = β¨π, πΈβ© & β’ π» = {β¨(Baseβndx), πβ©, β¨(.efβndx), πΈβ©} β β’ ((πΊ β UHGraph β§ π β π β§ πΈ β π) β πΊ βππ π») | ||
Theorem | ushggricedg 47116 | 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 β πΊ βππ π») | ||
Theorem | 1hegrlfgr 47117* | 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 47118 | Extend class notation with walks (of a pseudograph). |
class UPWalks | ||
Definition | df-upwlks 47119* |
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 47120* | 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 47121* | 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 47122* | Generalization of isupwlk 47121: 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 47123 | 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 47124 | A simple walk is a walk. (Contributed by AV, 30-Dec-2020.) (Proof shortened by AV, 27-Feb-2021.) |
β’ (πΉ(UPWalksβπΊ)π β πΉ(WalksβπΊ)π) | ||
Theorem | upgrwlkupwlk 47125 | 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 47126 | 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 47127* | Alternate proof of upgriswlk 29442 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 47128 | 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 47129* | 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 47139. (Contributed by AV, 24-Nov-2021.) |
β’ π = π« (Pairsβπ) & β’ πΊ = {β¨π£, πβ© β£ (π£ = π β§ βπ β USPGraph ((Vtxβπ) = π£ β§ (Edgβπ) = π))} β β’ (π β π β πΊ β (π Γ π)) | ||
Theorem | uspgrsprfv 47130* | 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 47136. (Contributed by AV, 24-Nov-2021.) |
β’ π = π« (Pairsβπ) & β’ πΊ = {β¨π£, πβ© β£ (π£ = π β§ βπ β USPGraph ((Vtxβπ) = π£ β§ (Edgβπ) = π))} & β’ πΉ = (π β πΊ β¦ (2nd βπ)) β β’ (π β πΊ β (πΉβπ) = (2nd βπ)) | ||
Theorem | uspgrsprf 47131* | 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 47132* | 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 47133* | 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 47134* | 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 47139. (Contributed by AV, 25-Nov-2021.) |
β’ π = π« (Pairsβπ) & β’ πΊ = {β¨π£, πβ© β£ (π£ = π β§ βπ β USPGraph ((Vtxβπ) = π£ β§ (Edgβπ) = π))} & β’ πΉ = (π β πΊ β¦ (2nd βπ)) β β’ (π β π β πΉ:πΊβ1-1-ontoβπ) | ||
Theorem | uspgrex 47135* | 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 47136* | 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 47137* | 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 47138* | 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 47139. (Contributed by AV, 27-Nov-2021.) |
β’ πΊ = {β¨π£, πβ© β£ (π£ = π β§ βπ β USPGraph ((Vtxβπ) = π£ β§ (Edgβπ) = π))} & β’ π = {π β π« (π Γ π) β£ βπ₯ β π βπ¦ β π (π₯ππ¦ β π¦ππ₯)} β β’ (π β π β πΊ β π ) | ||
Theorem | uspgrbisymrel 47139* |
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 47135) 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 47140* | Alternate proof of uspgrbisymrel 47139 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 47141 | 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 6934. (Contributed by AV, 27-Jan-2020.) |
β’ ((π΄πΉπ΅) β β β (β¨π΄, π΅β© β dom πΉ β§ Fun (πΉ βΎ {β¨π΄, π΅β©}))) | ||
Theorem | xpsnopab 47142* | A Cartesian product with a singleton expressed as ordered-pair class abstraction. (Contributed by AV, 27-Jan-2020.) |
β’ ({π} Γ πΆ) = {β¨π, πβ© β£ (π = π β§ π β πΆ)} | ||
Theorem | xpiun 47143* | A Cartesian product expressed as indexed union of ordered-pair class abstractions. (Contributed by AV, 27-Jan-2020.) |
β’ (π΅ Γ πΆ) = βͺ π₯ β π΅ {β¨π, πβ© β£ (π = π₯ β§ π β πΆ)} | ||
Theorem | ovn0ssdmfun 47144* | 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 6934. (Contributed by AV, 27-Jan-2020.) |
β’ (βπ β π· βπ β πΈ (ππΉπ) β β β ((π· Γ πΈ) β dom πΉ β§ Fun (πΉ βΎ (π· Γ πΈ)))) | ||
Theorem | fnxpdmdm 47145 | The domain of the domain of a function over a Cartesian square. (Contributed by AV, 13-Jan-2020.) |
β’ (πΉ Fn (π΄ Γ π΄) β dom dom πΉ = π΄) | ||
Theorem | cnfldsrngbas 47146 | The base set of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.) |
β’ π = (βfld βΎs π) β β’ (π β β β π = (Baseβπ )) | ||
Theorem | cnfldsrngadd 47147 | The group addition operation of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.) |
β’ π = (βfld βΎs π) β β’ (π β π β + = (+gβπ )) | ||
Theorem | cnfldsrngmul 47148 | The ring multiplication operation of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.) |
β’ π = (βfld βΎs π) β β’ (π β π β Β· = (.rβπ )) | ||
Theorem | plusfreseq 47149 | 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 47150 | 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 47151 | A set with an empty base set is always a magma. (Contributed by AV, 25-Feb-2020.) |
β’ (Baseβπ) = β β β’ (π β π β π β Mgm) | ||
Theorem | opmpoismgm 47152* | 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 47153* | 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 47154* | 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 47155* | 0 is not an odd integer. (Contributed by AV, 3-Feb-2020.) |
β’ π = {π§ β β€ β£ βπ₯ β β€ π§ = ((2 Β· π₯) + 1)} β β’ 0 β π | ||
Theorem | 1odd 47156* | 1 is an odd integer. (Contributed by AV, 3-Feb-2020.) |
β’ π = {π§ β β€ β£ βπ₯ β β€ π§ = ((2 Β· π₯) + 1)} β β’ 1 β π | ||
Theorem | 2nodd 47157* | 2 is not an odd integer. (Contributed by AV, 3-Feb-2020.) |
β’ π = {π§ β β€ β£ βπ₯ β β€ π§ = ((2 Β· π₯) + 1)} β β’ 2 β π | ||
Theorem | oddibas 47158* | Lemma 1 for oddinmgm 47160: 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 47159* | Lemma 2 for oddinmgm 47160: 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 47160* | 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 47235, and even a non-unital ring, see 2zrng 47226. (Contributed by AV, 3-Feb-2020.) |
β’ π = {π§ β β€ β£ βπ₯ β β€ π§ = ((2 Β· π₯) + 1)} & β’ π = (βfld βΎs π) β β’ π β Mgm | ||
Theorem | nnsgrpmgm 47161 | 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 47162 | 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 47163 | 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 47164 | 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 47165* | 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 47166* | Extract a summand from a finitely supported group sum. (Contributed by AV, 4-Sep-2019.) |
β’ β²ππ & β’ β²ππ & β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β (π β π΄ β¦ π) finSupp (0gβπΊ)) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β π β π΄) & β’ (π β π β π΅) & β’ ((π β§ π = π) β π = π) β β’ (π β (πΊ Ξ£g (π β π΄ β¦ π)) = ((πΊ Ξ£g (π β (π΄ β {π}) β¦ π)) + π)) | ||
Theorem | gsumfsupp 47167 | 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 7419, binary operations are defined by a rule, and with df-ov 7417, 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 47184. If, in addition, the result is also contained in the set π, the operation is called closed internal binary operation, see df-clintop 47185. 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 47185 ). 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 47185 and df-assintop 47186), 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 47171 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 47179, or for an alternate definition df-mgm2 47204 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 47168 | Extend class notation for the closure law. |
class clLaw | ||
Syntax | casslaw 47169 | Extend class notation for the associative law. |
class assLaw | ||
Syntax | ccomlaw 47170 | Extend class notation for the commutative law. |
class comLaw | ||
Definition | df-cllaw 47171* | 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 47172* | 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 47173* | 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 47174* | The predicate "is a closed operation". (Contributed by AV, 13-Jan-2020.) |
β’ (( β¬ β π β§ π β π) β ( β¬ clLaw π β βπ₯ β π βπ¦ β π (π₯ β¬ π¦) β π)) | ||
Theorem | iscomlaw 47175* | The predicate "is a commutative operation". (Contributed by AV, 20-Jan-2020.) |
β’ (( β¬ β π β§ π β π) β ( β¬ comLaw π β βπ₯ β π βπ¦ β π (π₯ β¬ π¦) = (π¦ β¬ π₯))) | ||
Theorem | clcllaw 47176 | Closure of a closed operation. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 21-Jan-2020.) |
β’ (( β¬ clLaw π β§ π β π β§ π β π) β (π β¬ π) β π) | ||
Theorem | isasslaw 47177* | The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.) (Revised by AV, 13-Jan-2020.) |
β’ (( β¬ β π β§ π β π) β ( β¬ assLaw π β βπ₯ β π βπ¦ β π βπ§ β π ((π₯ β¬ π¦) β¬ π§) = (π₯ β¬ (π¦ β¬ π§)))) | ||
Theorem | asslawass 47178* | Associativity of an associative operation. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 21-Jan-2020.) |
β’ ( β¬ assLaw π β βπ₯ β π βπ¦ β π βπ§ β π ((π₯ β¬ π¦) β¬ π§) = (π₯ β¬ (π¦ β¬ π§))) | ||
Theorem | mgmplusgiopALT 47179 | 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 47180 | 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 47181 | Extend class notation with class of internal (binary) operations for a set. |
class intOp | ||
Syntax | cclintop 47182 | Extend class notation with class of closed operations for a set. |
class clIntOp | ||
Syntax | cassintop 47183 | Extend class notation with class of associative operations for a set. |
class assIntOp | ||
Definition | df-intop 47184* | 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 47185 | 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 47186* | 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 47187 | The internal (binary) operations for a set. (Contributed by AV, 20-Jan-2020.) |
β’ ((π β π β§ π β π) β (π intOp π) = (π βm (π Γ π))) | ||
Theorem | intop 47188 | An internal (binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
β’ ( β¬ β (π intOp π) β β¬ :(π Γ π)βΆπ) | ||
Theorem | clintopval 47189 | The closed (internal binary) operations for a set. (Contributed by AV, 20-Jan-2020.) |
β’ (π β π β ( clIntOp βπ) = (π βm (π Γ π))) | ||
Theorem | assintopval 47190* | The associative (closed internal binary) operations for a set. (Contributed by AV, 20-Jan-2020.) |
β’ (π β π β ( assIntOp βπ) = {π β ( clIntOp βπ) β£ π assLaw π}) | ||
Theorem | assintopmap 47191* | The associative (closed internal binary) operations for a set, expressed with set exponentiation. (Contributed by AV, 20-Jan-2020.) |
β’ (π β π β ( assIntOp βπ) = {π β (π βm (π Γ π)) β£ π assLaw π}) | ||
Theorem | isclintop 47192 | 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 47193 | A closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
β’ ( β¬ β ( clIntOp βπ) β β¬ :(π Γ π)βΆπ) | ||
Theorem | assintop 47194 | An associative (closed internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
β’ ( β¬ β ( assIntOp βπ) β ( β¬ :(π Γ π)βΆπ β§ β¬ assLaw π)) | ||
Theorem | isassintop 47195* | 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 47196 | The closure law holds for a closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
β’ ( β¬ β ( clIntOp βπ) β β¬ clLaw π) | ||
Theorem | assintopcllaw 47197 | 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 47198 | 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 47199* | 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 47200 | Extend class notation with class of all magmas. |
class MgmALT |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |