![]() |
Metamath
Proof Explorer Theorem List (p. 298 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 | ex-ceil 29701 | Example for df-ceil 13758. (Contributed by AV, 4-Sep-2021.) |
⊢ ((⌈‘(3 / 2)) = 2 ∧ (⌈‘-(3 / 2)) = -1) | ||
Theorem | ex-mod 29702 | Example for df-mod 13835. (Contributed by AV, 3-Sep-2021.) |
⊢ ((5 mod 3) = 2 ∧ (-7 mod 2) = 1) | ||
Theorem | ex-exp 29703 | Example for df-exp 14028. (Contributed by AV, 4-Sep-2021.) |
⊢ ((5↑2) = ;25 ∧ (-3↑-2) = (1 / 9)) | ||
Theorem | ex-fac 29704 | Example for df-fac 14234. (Contributed by AV, 4-Sep-2021.) |
⊢ (!‘5) = ;;120 | ||
Theorem | ex-bc 29705 | Example for df-bc 14263. (Contributed by AV, 4-Sep-2021.) |
⊢ (5C3) = ;10 | ||
Theorem | ex-hash 29706 | Example for df-hash 14291. (Contributed by AV, 4-Sep-2021.) |
⊢ (♯‘{0, 1, 2}) = 3 | ||
Theorem | ex-sqrt 29707 | Example for df-sqrt 15182. (Contributed by AV, 4-Sep-2021.) |
⊢ (√‘;25) = 5 | ||
Theorem | ex-abs 29708 | Example for df-abs 15183. (Contributed by AV, 4-Sep-2021.) |
⊢ (abs‘-2) = 2 | ||
Theorem | ex-dvds 29709 | Example for df-dvds 16198: 3 divides into 6. (Contributed by David A. Wheeler, 19-May-2015.) |
⊢ 3 ∥ 6 | ||
Theorem | ex-gcd 29710 | Example for df-gcd 16436. (Contributed by AV, 5-Sep-2021.) |
⊢ (-6 gcd 9) = 3 | ||
Theorem | ex-lcm 29711 | Example for df-lcm 16527. (Contributed by AV, 5-Sep-2021.) |
⊢ (6 lcm 9) = ;18 | ||
Theorem | ex-prmo 29712 | Example for df-prmo 16965: (#p‘10) = 2 · 3 · 5 · 7. (Contributed by AV, 6-Sep-2021.) |
⊢ (#p‘;10) = ;;210 | ||
Theorem | aevdemo 29713* | Proof illustrating the comment of aev2 2062. (Contributed by BJ, 30-Mar-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ((∃𝑎∀𝑏 𝑐 = 𝑑 ∨ ∃𝑒 𝑓 = 𝑔) ∧ ∀ℎ(𝑖 = 𝑗 → 𝑘 = 𝑙))) | ||
Theorem | ex-ind-dvds 29714 | Example of a proof by induction (divisibility result). (Contributed by Stanislas Polu, 9-Mar-2020.) (Revised by BJ, 24-Mar-2020.) |
⊢ (𝑁 ∈ ℕ0 → 3 ∥ ((4↑𝑁) + 2)) | ||
Theorem | ex-fpar 29715 | Formalized example provided in the comment for fpar 8102. (Contributed by AV, 3-Jan-2024.) |
⊢ 𝐻 = ((◡(1st ↾ (V × V)) ∘ (𝐹 ∘ (1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V))))) & ⊢ 𝐴 = (0[,)+∞) & ⊢ 𝐵 = ℝ & ⊢ 𝐹 = (√ ↾ 𝐴) & ⊢ 𝐺 = (sin ↾ 𝐵) ⇒ ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋( + ∘ 𝐻)𝑌) = ((√‘𝑋) + (sin‘𝑌))) | ||
Theorem | avril1 29716 |
Poisson d'Avril's Theorem. This theorem is noted for its
Selbstdokumentieren property, which means, literally,
"self-documenting" and recalls the principle of quidquid
german dictum
sit, altum viditur, often used in set theory. Starting with the
seemingly simple yet profound fact that any object 𝑥 equals
itself
(proved by Tarski in 1965; see Lemma 6 of [Tarski] p. 68), we
demonstrate that the power set of the real numbers, as a relation on the
value of the imaginary unit, does not conjoin with an empty relation on
the product of the additive and multiplicative identity elements,
leading to this startling conclusion that has left even seasoned
professional mathematicians scratching their heads. (Contributed by
Prof. Loof Lirpa, 1-Apr-2005.) (Proof modification is discouraged.)
(New usage is discouraged.)
A reply to skeptics can be found at mmnotes.txt, under the 1-Apr-2006 entry. |
⊢ ¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1)) | ||
Theorem | 2bornot2b 29717 | The law of excluded middle. Act III, Theorem 1 of Shakespeare, Hamlet, Prince of Denmark (1602). Its author leaves its proof as an exercise for the reader - "To be, or not to be: that is the question" - starting a trend that has become standard in modern-day textbooks, serving to make the frustrated reader feel inferior, or in some cases to mask the fact that the author does not know its solution. (Contributed by Prof. Loof Lirpa, 1-Apr-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (2 · 𝐵 ∨ ¬ 2 · 𝐵) | ||
Theorem | helloworld 29718 | The classic "Hello world" benchmark has been translated into 314 computer programming languages - see http://helloworldcollection.de. However, for many years it eluded a proof that it is more than just a conjecture, even though a wily mathematician once claimed, "I have discovered a truly marvelous proof of this, which this margin is too narrow to contain." Using an IBM 709 mainframe, a team of mathematicians led by Prof. Loof Lirpa, at the New College of Tahiti, were finally able to put it to rest with a remarkably short proof only four lines long. (Contributed by Prof. Loof Lirpa, 1-Apr-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ (ℎ ∈ (𝐿𝐿0) ∧ 𝑊∅(R1𝑑)) | ||
Theorem | 1p1e2apr1 29719 | One plus one equals two. Using proof-shortening techniques pioneered by Mr. Mel L. O'Cat, along with the latest supercomputer technology, Prof. Loof Lirpa and colleagues were able to shorten Whitehead and Russell's 360-page proof that 1+1=2 in Principia Mathematica to this remarkable proof only two steps long, thus establishing a new world's record for this famous theorem. (Contributed by Prof. Loof Lirpa, 1-Apr-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (1 + 1) = 2 | ||
Theorem | eqid1 29720 |
Law of identity (reflexivity of class equality). Theorem 6.4 of [Quine]
p. 41.
This law is thought to have originated with Aristotle (Metaphysics, Book VII, Part 17). It is one of the three axioms of Ayn Rand's philosophy (Atlas Shrugged, Part Three, Chapter VII). While some have proposed extending Rand's axiomatization to include Compassion and Kindness, others fear that such an extension may flirt with logical inconsistency. (Contributed by Stefan Allan, 1-Apr-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 = 𝐴 | ||
Theorem | 1div0apr 29721 | Division by zero is forbidden! If we try, we encounter the DO NOT ENTER sign, which in mathematics means it is foolhardy to venture any further, possibly putting the underlying fabric of reality at risk. Based on a dare by David A. Wheeler. (Contributed by Mario Carneiro, 1-Apr-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (1 / 0) = ∅ | ||
Theorem | topnfbey 29722 | Nothing seems to be impossible to Prof. Lirpa. After years of intensive research, he managed to find a proof that when given a chance to reach infinity, one could indeed go beyond, thus giving formal soundness to Buzz Lightyear's motto "To infinity... and beyond!" (Contributed by Prof. Loof Lirpa, 1-Apr-2020.) (Revised by Thierry Arnoux, 2-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐵 ∈ (0...+∞) → +∞ < 𝐵) | ||
Theorem | 9p10ne21 29723 | 9 + 10 is not equal to 21. This disproves a popular meme which asserts that 9 + 10 does equal 21. See https://www.quora.com/Can-someone-try-to-prove-to-me-that-9+10-21 for attempts to prove that 9 + 10 = 21, and see https://tinyurl.com/9p10e21 for the history of the 9 + 10 = 21 meme. (Contributed by BTernaryTau, 25-Aug-2023.) |
⊢ (9 + ;10) ≠ ;21 | ||
Theorem | 9p10ne21fool 29724 | 9 + 10 equals 21. This astonishing thesis lives as a meme on the internet, and may be believed by quite some people. At least repeated requests to falsify it are a permanent part of the story. Prof. Loof Lirpa did not rest until he finally came up with a computer verifiable mathematical proof, that only a fool can think so. (Contributed by Prof. Loof Lirpa, 26-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((9 + ;10) = ;21 → 𝐹∅(0 · 1)) | ||
Axiom | ax-flt 29725 | This factoid is e.g. useful for nrt2irr 29726. Andrew has a proof, I'll have a go at formalizing it after my coffee break. In the mean time let's add it as an axiom. (Contributed by Prof. Loof Lirpa, 1-Apr-2025.) (New usage is discouraged.) |
⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ (𝑋 ∈ ℕ ∧ 𝑌 ∈ ℕ ∧ 𝑍 ∈ ℕ)) → ((𝑋↑𝑁) + (𝑌↑𝑁)) ≠ (𝑍↑𝑁)) | ||
Theorem | nrt2irr 29726 | The 𝑁-th root of 2 is irrational for 𝑁 greater than 2. For 𝑁 = 2, see sqrt2irr 16192. This short and rather elegant proof has the minor disadvantage that it refers to ax-flt 29725, which is still to be formalized. For a proof not requiring ax-flt 29725, see rtprmirr 41237. (Contributed by Prof. Loof Lirpa, 1-Apr-2025.) (Proof modification is discouraged.) |
⊢ (𝑁 ∈ (ℤ≥‘3) → ¬ (2↑𝑐(1 / 𝑁)) ∈ ℚ) | ||
Syntax | cplig 29727 | Extend class notation with the class of all planar incidence geometries. |
class Plig | ||
Definition | df-plig 29728* |
Define the class of planar incidence geometries. We use Hilbert's
axioms and adapt them to planar geometry. We use ∈ for the
incidence relation. We could have used a generic binary relation, but
using ∈ allows to reuse previous results.
Much of what follows is
directly borrowed from Aitken, Incidence-Betweenness Geometry,
2008,
http://public.csusm.edu/aitken_html/m410/betweenness.08.pdf.
The class Plig is the class of planar incidence geometries, where a planar incidence geometry is defined as a set of lines satisfying three axioms. In the definition below, 𝑥 denotes a planar incidence geometry, so ∪ 𝑥 denotes the union of its lines, that is, the set of points in the plane, 𝑙 denotes a line, and 𝑎, 𝑏, 𝑐 denote points. Therefore, the axioms are: 1) for all pairs of (distinct) points, there exists a unique line containing them; 2) all lines contain at least two points; 3) there exist three non-collinear points. (Contributed by FL, 2-Aug-2009.) |
⊢ Plig = {𝑥 ∣ (∀𝑎 ∈ ∪ 𝑥∀𝑏 ∈ ∪ 𝑥(𝑎 ≠ 𝑏 → ∃!𝑙 ∈ 𝑥 (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙)) ∧ ∀𝑙 ∈ 𝑥 ∃𝑎 ∈ ∪ 𝑥∃𝑏 ∈ ∪ 𝑥(𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙) ∧ ∃𝑎 ∈ ∪ 𝑥∃𝑏 ∈ ∪ 𝑥∃𝑐 ∈ ∪ 𝑥∀𝑙 ∈ 𝑥 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙))} | ||
Theorem | isplig 29729* | The predicate "is a planar incidence geometry" for sets. (Contributed by FL, 2-Aug-2009.) |
⊢ 𝑃 = ∪ 𝐺 ⇒ ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ Plig ↔ (∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 → ∃!𝑙 ∈ 𝐺 (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙)) ∧ ∀𝑙 ∈ 𝐺 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙) ∧ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙)))) | ||
Theorem | ispligb 29730* | The predicate "is a planar incidence geometry". (Contributed by BJ, 2-Dec-2021.) |
⊢ 𝑃 = ∪ 𝐺 ⇒ ⊢ (𝐺 ∈ Plig ↔ (𝐺 ∈ V ∧ (∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 → ∃!𝑙 ∈ 𝐺 (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙)) ∧ ∀𝑙 ∈ 𝐺 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙) ∧ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙)))) | ||
Theorem | tncp 29731* | In any planar incidence geometry, there exist three non-collinear points. (Contributed by FL, 3-Aug-2009.) |
⊢ 𝑃 = ∪ 𝐺 ⇒ ⊢ (𝐺 ∈ Plig → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙)) | ||
Theorem | l2p 29732* | For any line in a planar incidence geometry, there exist two different points on the line. (Contributed by AV, 28-Nov-2021.) |
⊢ 𝑃 = ∪ 𝐺 ⇒ ⊢ ((𝐺 ∈ Plig ∧ 𝐿 ∈ 𝐺) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝐿)) | ||
Theorem | lpni 29733* | For any line in a planar incidence geometry, there exists a point not on the line. (Contributed by Jeff Hankins, 15-Aug-2009.) |
⊢ 𝑃 = ∪ 𝐺 ⇒ ⊢ ((𝐺 ∈ Plig ∧ 𝐿 ∈ 𝐺) → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿) | ||
Theorem | nsnlplig 29734 | There is no "one-point line" in a planar incidence geometry. (Contributed by BJ, 2-Dec-2021.) (Proof shortened by AV, 5-Dec-2021.) |
⊢ (𝐺 ∈ Plig → ¬ {𝐴} ∈ 𝐺) | ||
Theorem | nsnlpligALT 29735 | Alternate version of nsnlplig 29734 using the predicate ∉ instead of ¬ ∈ and whose proof is shorter. (Contributed by AV, 5-Dec-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐺 ∈ Plig → {𝐴} ∉ 𝐺) | ||
Theorem | n0lplig 29736 | There is no "empty line" in a planar incidence geometry. (Contributed by AV, 28-Nov-2021.) (Proof shortened by BJ, 2-Dec-2021.) |
⊢ (𝐺 ∈ Plig → ¬ ∅ ∈ 𝐺) | ||
Theorem | n0lpligALT 29737 | Alternate version of n0lplig 29736 using the predicate ∉ instead of ¬ ∈ and whose proof bypasses nsnlplig 29734. (Contributed by AV, 28-Nov-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐺 ∈ Plig → ∅ ∉ 𝐺) | ||
Theorem | eulplig 29738* | Through two distinct points of a planar incidence geometry, there is a unique line. (Contributed by BJ, 2-Dec-2021.) |
⊢ 𝑃 = ∪ 𝐺 ⇒ ⊢ ((𝐺 ∈ Plig ∧ ((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ 𝐴 ≠ 𝐵)) → ∃!𝑙 ∈ 𝐺 (𝐴 ∈ 𝑙 ∧ 𝐵 ∈ 𝑙)) | ||
Theorem | pliguhgr 29739 | Any planar incidence geometry 𝐺 can be regarded as a hypergraph with its points as vertices and its lines as edges. See incistruhgr 28339 for a generalization of this case for arbitrary incidence structures (planar incidence geometries are such incidence structures). (Proposed by Gerard Lang, 24-Nov-2021.) (Contributed by AV, 28-Nov-2021.) |
⊢ (𝐺 ∈ Plig → ⟨∪ 𝐺, ( I ↾ 𝐺)⟩ ∈ UHGraph) | ||
This section contains a few aliases that we temporarily keep to prevent broken links. If you land on any of these, please let the originating site and/or us know that the link that made you land here should be changed. | ||
Theorem | dummylink 29740 |
Alias for a1ii 2 that may be referenced in some older works, and
kept
here to prevent broken links.
If you landed here, please let the originating site and/or us know that the link that made you land here should be changed to a link to a1ii 2. (Contributed by NM, 7-Feb-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 ⇒ ⊢ 𝜑 | ||
Theorem | id1 29741 |
Alias for idALT 23 that may be referenced in some older works, and
kept
here to prevent broken links.
If you landed here, please let the originating site and/or us know that the link that made you land here should be changed to a link to idALT 23. (Contributed by NM, 30-Sep-1992.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜑) | ||
The intent is for this deprecated section to be deleted once its theorems have extensible structure versions (or are not useful). You can make a list of "terminal" theorems (i.e., theorems not referenced by anything else) and for each theorem see if there exists an extensible structure version (or decide it is not useful), and if so, delete it. Then, repeat this recursively. One way to search for terminal theorems is to log the output ("MM> OPEN LOG xxx.txt") of "MM> SHOW USAGE <label-match>" in the Metamath program and search for "(None)". | ||
This section contains an earlier development of groups that was defined before extensible structures were introduced. The intent is for this deprecated section to be deleted once the corresponding definitions and theorems for complex topological vector spaces, which are using them, are revised accordingly. | ||
Syntax | cgr 29742 | Extend class notation with the class of all group operations. |
class GrpOp | ||
Syntax | cgi 29743 | Extend class notation with a function mapping a group operation to the group's identity element. |
class GId | ||
Syntax | cgn 29744 | Extend class notation with a function mapping a group operation to the inverse function for the group. |
class inv | ||
Syntax | cgs 29745 | Extend class notation with a function mapping a group operation to the division (or subtraction) operation for the group. |
class /𝑔 | ||
Definition | df-grpo 29746* | Define the class of all group operations. The base set for a group can be determined from its group operation. Based on the definition in Exercise 28 of [Herstein] p. 54. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) |
⊢ GrpOp = {𝑔 ∣ ∃𝑡(𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢))} | ||
Definition | df-gid 29747* | Define a function that maps a group operation to the group's identity element. (Contributed by FL, 5-Feb-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ GId = (𝑔 ∈ V ↦ (℩𝑢 ∈ ran 𝑔∀𝑥 ∈ ran 𝑔((𝑢𝑔𝑥) = 𝑥 ∧ (𝑥𝑔𝑢) = 𝑥))) | ||
Definition | df-ginv 29748* | Define a function that maps a group operation to the group's inverse function. (Contributed by NM, 26-Oct-2006.) (New usage is discouraged.) |
⊢ inv = (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔 ↦ (℩𝑧 ∈ ran 𝑔(𝑧𝑔𝑥) = (GId‘𝑔)))) | ||
Definition | df-gdiv 29749* | Define a function that maps a group operation to the group's division (or subtraction) operation. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
⊢ /𝑔 = (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔, 𝑦 ∈ ran 𝑔 ↦ (𝑥𝑔((inv‘𝑔)‘𝑦)))) | ||
Theorem | isgrpo 29750* | The predicate "is a group operation." Note that 𝑋 is the base set of the group. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ GrpOp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢)))) | ||
Theorem | isgrpoi 29751* | Properties that determine a group operation. Read 𝑁 as 𝑁(𝑥). (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
⊢ 𝑋 ∈ V & ⊢ 𝐺:(𝑋 × 𝑋)⟶𝑋 & ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))) & ⊢ 𝑈 ∈ 𝑋 & ⊢ (𝑥 ∈ 𝑋 → (𝑈𝐺𝑥) = 𝑥) & ⊢ (𝑥 ∈ 𝑋 → 𝑁 ∈ 𝑋) & ⊢ (𝑥 ∈ 𝑋 → (𝑁𝐺𝑥) = 𝑈) ⇒ ⊢ 𝐺 ∈ GrpOp | ||
Theorem | grpofo 29752 | A group operation maps onto the group's underlying set. (Contributed by NM, 30-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ GrpOp → 𝐺:(𝑋 × 𝑋)–onto→𝑋) | ||
Theorem | grpocl 29753 | Closure law for a group operation. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋) | ||
Theorem | grpolidinv 29754* | A group has a left identity element, and every member has a left inverse. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ GrpOp → ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢)) | ||
Theorem | grpon0 29755 | The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ GrpOp → 𝑋 ≠ ∅) | ||
Theorem | grpoass 29756 | A group operation is associative. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = (𝐴𝐺(𝐵𝐺𝐶))) | ||
Theorem | grpoidinvlem1 29757 | Lemma for grpoidinv 29761. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝐺 ∈ GrpOp ∧ (𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) ∧ ((𝑌𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝐴) = 𝐴)) → (𝑈𝐺𝐴) = 𝑈) | ||
Theorem | grpoidinvlem2 29758 | Lemma for grpoidinv 29761. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝐺 ∈ GrpOp ∧ (𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) ∧ ((𝑈𝐺𝑌) = 𝑌 ∧ (𝑌𝐺𝐴) = 𝑈)) → ((𝐴𝐺𝑌)𝐺(𝐴𝐺𝑌)) = (𝐴𝐺𝑌)) | ||
Theorem | grpoidinvlem3 29759* | Lemma for grpoidinv 29761. (Contributed by NM, 11-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥) & ⊢ (𝜓 ↔ ∀𝑥 ∈ 𝑋 ∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈) ⇒ ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)) | ||
Theorem | grpoidinvlem4 29760* | Lemma for grpoidinv 29761. (Contributed by NM, 14-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)) → (𝐴𝐺𝑈) = (𝑈𝐺𝐴)) | ||
Theorem | grpoidinv 29761* | A group has a left and right identity element, and every member has a left and right inverse. (Contributed by NM, 14-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ GrpOp → ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑥) = 𝑢 ∧ (𝑥𝐺𝑦) = 𝑢))) | ||
Theorem | grpoideu 29762* | The left identity element of a group is unique. Lemma 2.2.1(a) of [Herstein] p. 55. (Contributed by NM, 14-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ GrpOp → ∃!𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥) | ||
Theorem | grporndm 29763 | A group's range in terms of its domain. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.) |
⊢ (𝐺 ∈ GrpOp → ran 𝐺 = dom dom 𝐺) | ||
Theorem | 0ngrp 29764 | The empty set is not a group. (Contributed by NM, 25-Apr-2007.) (New usage is discouraged.) |
⊢ ¬ ∅ ∈ GrpOp | ||
Theorem | gidval 29765* | The value of the identity element of a group. (Contributed by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ 𝑉 → (GId‘𝐺) = (℩𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥))) | ||
Theorem | grpoidval 29766* | Lemma for grpoidcl 29767 and others. (Contributed by NM, 5-Feb-2010.) (Proof shortened by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ (𝐺 ∈ GrpOp → 𝑈 = (℩𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥)) | ||
Theorem | grpoidcl 29767 | The identity element of a group belongs to the group. (Contributed by NM, 24-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ (𝐺 ∈ GrpOp → 𝑈 ∈ 𝑋) | ||
Theorem | grpoidinv2 29768* | A group's properties using the explicit identity element. (Contributed by NM, 5-Feb-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (((𝑈𝐺𝐴) = 𝐴 ∧ (𝐴𝐺𝑈) = 𝐴) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈))) | ||
Theorem | grpolid 29769 | The identity element of a group is a left identity. (Contributed by NM, 24-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝑈𝐺𝐴) = 𝐴) | ||
Theorem | grporid 29770 | The identity element of a group is a right identity. (Contributed by NM, 24-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝑈) = 𝐴) | ||
Theorem | grporcan 29771 | Right cancellation law for groups. (Contributed by NM, 26-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐶) = (𝐵𝐺𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | grpoinveu 29772* | The left inverse element of a group is unique. Lemma 2.2.1(b) of [Herstein] p. 55. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → ∃!𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈) | ||
Theorem | grpoid 29773 | Two ways of saying that an element of a group is the identity element. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝐴 = 𝑈 ↔ (𝐴𝐺𝐴) = 𝐴)) | ||
Theorem | grporn 29774 | The range of a group operation. Useful for satisfying group base set hypotheses of the form 𝑋 = ran 𝐺. (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 ∈ GrpOp & ⊢ dom 𝐺 = (𝑋 × 𝑋) ⇒ ⊢ 𝑋 = ran 𝐺 | ||
Theorem | grpoinvfval 29775* | The inverse function of a group. (Contributed by NM, 26-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ (𝐺 ∈ GrpOp → 𝑁 = (𝑥 ∈ 𝑋 ↦ (℩𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈))) | ||
Theorem | grpoinvval 29776* | The inverse of a group element. (Contributed by NM, 26-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (℩𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)) | ||
Theorem | grpoinvcl 29777 | A group element's inverse is a group element. (Contributed by NM, 27-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ 𝑋) | ||
Theorem | grpoinv 29778 | The properties of a group element's inverse. (Contributed by NM, 27-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (((𝑁‘𝐴)𝐺𝐴) = 𝑈 ∧ (𝐴𝐺(𝑁‘𝐴)) = 𝑈)) | ||
Theorem | grpolinv 29779 | The left inverse of a group element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝐴)𝐺𝐴) = 𝑈) | ||
Theorem | grporinv 29780 | The right inverse of a group element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺(𝑁‘𝐴)) = 𝑈) | ||
Theorem | grpoinvid1 29781 | The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘𝐴) = 𝐵 ↔ (𝐴𝐺𝐵) = 𝑈)) | ||
Theorem | grpoinvid2 29782 | The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘𝐴) = 𝐵 ↔ (𝐵𝐺𝐴) = 𝑈)) | ||
Theorem | grpolcan 29783 | Left cancellation law for groups. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐶𝐺𝐴) = (𝐶𝐺𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | grpo2inv 29784 | Double inverse law for groups. Lemma 2.2.1(c) of [Herstein] p. 55. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝑁‘(𝑁‘𝐴)) = 𝐴) | ||
Theorem | grpoinvf 29785 | Mapping of the inverse function of a group. (Contributed by NM, 29-Mar-2008.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ (𝐺 ∈ GrpOp → 𝑁:𝑋–1-1-onto→𝑋) | ||
Theorem | grpoinvop 29786 | The inverse of the group operation reverses the arguments. Lemma 2.2.1(d) of [Herstein] p. 55. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐺𝐵)) = ((𝑁‘𝐵)𝐺(𝑁‘𝐴))) | ||
Theorem | grpodivfval 29787* | Group division (or subtraction) operation. (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ (𝐺 ∈ GrpOp → 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝐺(𝑁‘𝑦)))) | ||
Theorem | grpodivval 29788 | Group division (or subtraction) operation value. (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐴𝐺(𝑁‘𝐵))) | ||
Theorem | grpodivinv 29789 | Group division by an inverse. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷(𝑁‘𝐵)) = (𝐴𝐺𝐵)) | ||
Theorem | grpoinvdiv 29790 | Inverse of a group division. (Contributed by NM, 24-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐷𝐵)) = (𝐵𝐷𝐴)) | ||
Theorem | grpodivf 29791 | Mapping for group division. (Contributed by NM, 10-Apr-2008.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ (𝐺 ∈ GrpOp → 𝐷:(𝑋 × 𝑋)⟶𝑋) | ||
Theorem | grpodivcl 29792 | Closure of group division (or subtraction) operation. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ 𝑋) | ||
Theorem | grpodivdiv 29793 | Double group division. (Contributed by NM, 24-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷(𝐵𝐷𝐶)) = (𝐴𝐺(𝐶𝐷𝐵))) | ||
Theorem | grpomuldivass 29794 | Associative-type law for multiplication and division. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐷𝐶) = (𝐴𝐺(𝐵𝐷𝐶))) | ||
Theorem | grpodivid 29795 | Division of a group member by itself. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 𝑈) | ||
Theorem | grponpcan 29796 | Cancellation law for group division. (npcan 11469 analog.) (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐷𝐵)𝐺𝐵) = 𝐴) | ||
Syntax | cablo 29797 | Extend class notation with the class of all Abelian group operations. |
class AbelOp | ||
Definition | df-ablo 29798* | Define the class of all Abelian group operations. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
⊢ AbelOp = {𝑔 ∈ GrpOp ∣ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(𝑥𝑔𝑦) = (𝑦𝑔𝑥)} | ||
Theorem | isablo 29799* | The predicate "is an Abelian (commutative) group operation." (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ AbelOp ↔ (𝐺 ∈ GrpOp ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐺𝑦) = (𝑦𝐺𝑥))) | ||
Theorem | ablogrpo 29800 | An Abelian group operation is a group operation. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
⊢ (𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |