Home | Metamath
Proof ExplorerTheorem List
(p. 209 of 322)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs

Color key: | Metamath Proof Explorer
(1-21498) |
Hilbert Space Explorer
(21499-23021) |
Users' Mathboxes
(23022-32154) |

Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|

Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded5.8-2 20801 | A more efficient proof of Theorem 5.8 of [Clemente] p. 20. For a longer line-by-line translation, see ex-natded5.8 20800. (Contributed by Mario Carneiro, 9-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded5.13 20802 |
Theorem 5.13 of [Clemente] p. 20, translated line by line using the
interpretation of natural deduction in Metamath.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
A much more efficient proof, using more of Metamath and MPE's
capabilities, is shown in ex-natded5.13-2 20803.
The original proof, which uses Fitch style, was written as follows
(the leading "..." shows an embedded ND hypothesis, beginning with
the initial assumption of the ND hypothesis):
The original used Latin letters; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including and uses the Metamath equivalents of the natural deduction rules. To add an assumption, the antecedent is modified to include it (typically by using adantr 451; simpr 447 is useful when you want to depend directly on the new assumption). (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded5.13-2 20803 | A more efficient proof of Theorem 5.13 of [Clemente] p. 20. Compare with ex-natded5.13 20802. (Contributed by Mario Carneiro, 9-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded9.20 20804 |
Theorem 9.20 of [Clemente] p. 43, translated line by line using the
usual translation of natural deduction (ND) in the
Metamath Proof Explorer (MPE) notation.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
The original proof, which uses Fitch style, was written as follows
(the leading "..." shows an embedded ND hypothesis, beginning with
the initial assumption of the ND hypothesis):
The original used Latin letters; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including and uses the Metamath equivalents of the natural deduction rules. To add an assumption, the antecedent is modified to include it (typically by using adantr 451; simpr 447 is useful when you want to depend directly on the new assumption). Below is the final metamath proof (which reorders some steps). A much more efficient proof is ex-natded9.20-2 20805. (Proof modification is discouraged.) (Contributed by David A. Wheeler, 19-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded9.20-2 20805 | A more efficient proof of Theorem 9.20 of [Clemente] p. 45. Compare with ex-natded9.20 20804. (Proof modification is discouraged.) (Contributed by David A. Wheeler, 19-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded9.26 20806* |
Theorem 9.26 of [Clemente] p. 45, translated line by line using an
interpretation of natural deduction in Metamath. This proof has some
additional complications due to the fact that Metamath's existential
elimination rule does not change bound variables, so we need to verify
that is bound in the conclusion.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
The original proof, which uses Fitch style, was written as follows
(the leading "..." shows an embedded ND hypothesis, beginning with
the initial assumption of the ND hypothesis):
The original used Latin letters for predicates; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including and uses the Metamath equivalents of the natural deduction rules. Below is the final metamath proof (which reorders some steps). Note that in the original proof, has explicit parameters. In Metamath, these parameters are always implicit, and the parameters upon which a wff variable can depend are recorded in the "allowed substitution hints" below. A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded9.26-2 20807. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by David A. Wheeler, 18-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded9.26-2 20807* | A more efficient proof of Theorem 9.26 of [Clemente] p. 45. Compare with ex-natded9.26 20806. (Contributed by Mario Carneiro, 9-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

14.1.4 Definitional examples | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-or 20808 | Example for df-or 359. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-an 20809 | Example for df-an 360. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-dif 20810 | Example for df-dif 3155. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-un 20811 | Example for df-un 3157. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-in 20812 | Example for df-in 3159. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-uni 20813 | Example for df-uni 3828. Example by David A. Wheeler. (Contributed by Mario Carneiro, 2-Jul-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-ss 20814 | Example for df-ss 3166. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-pss 20815 | Example for df-pss 3168. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-pw 20816 | Example for df-pw 3627. Example by David A. Wheeler. (Contributed by Mario Carneiro, 2-Jul-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-pr 20817 | Example for df-pr 3647. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-br 20818 | Example for df-br 4024. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-opab 20819* | Example for df-opab 4078. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-eprel 20820 | Example for df-eprel 4305. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-id 20821 | Example for df-id 4309. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-po 20822 | Example for df-po 4314. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-xp 20823 | Example for df-xp 4695. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-cnv 20824 | Example for df-cnv 4697. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-co 20825 | Example for df-co 4698. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-dm 20826 | Example for df-dm 4699. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-rn 20827 | Example for df-rn 4700. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-res 20828 | Example for df-res 4701. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-ima 20829 | Example for df-ima 4702. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-fv 20830 | Example for df-fv 5263. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-1st 20831 | Example for df-1st 6122. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-2nd 20832 | Example for df-2nd 6123. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 1kp2ke3k 20833 |
Example for df-dec 10125, 1000 + 2000 = 3000.
This proof disproves (by counter-example) the assertion of Hao Wang, who
stated, "There is a theorem in the primitive notation of set theory
that
corresponds to the arithmetic theorem 1000 + 2000 = 3000. The formula
would be forbiddingly long... even if (one) knows the definitions and is
asked to simplify the long formula according to them, chances are he will
make errors and arrive at some incorrect result." (Hao Wang,
"Theory and
practice in mathematics" , In Thomas Tymoczko, editor,
This is noted in The proof here starts with , commutes it, and repeatedly multiplies both sides by ten. This is certainly longer than traditional mathematical proofs, e.g., there are a number of steps explicitly shown here to show that we're allowed to do operations such as multiplication. However, while longer, the proof is clearly a manageable size - even though every step is rigorously derived all the way back to the primitive notions of set theory and logic. And while there's a risk of making errors, the many independent verifiers make it much less likely that an incorrect result will be accepted. This proof heavily relies on the decimal constructor df-dec 10125 developed by Mario Carneiro in 2015. The underlying Metamath language has an intentionally very small set of primitives; it doesn't even have a built-in construct for numbers. Instead, the digits are defined using these primitives, and the decimal constructor is used to make it easy to express larger numbers as combinations of digits. (Contributed by David A. Wheeler, 29-Jun-2016.) (Shortened by Mario Carneiro using the arithmetic algorithm in mmj2, 30-Jun-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

;;; ;;; ;;; | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-fl 20834 | Example for df-fl 10925. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-dvds 20835 | 3 divides into 6. A demonstration of df-dvds 12532. (Contributed by David A. Wheeler, 19-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

14.2 Humor | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

14.2.1 April Fool's theorem | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | avril1 20836 |
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.)
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 2bornot2b 20837 |
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.)
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | helloworld 20838 | The classic "Hello world" benchmark has been translated into 314 computer programming languages - see http://www.roesler-ac.de/wolfram/hello.htm. 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 put it rest with a remarkably short proof only 4 lines long. (Contributed by Prof. Loof Lirpa, 1-Apr-2007.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 1p1e2apr1 20839 |
One plus one equals two. Using proof-shortening techniques pioneered by
Mr. Mel 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.)
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | eqid1 20840 |
Law of identity (reflexivity of class equality). Theorem 6.4 of [Quine]
p. 41.
This law is thought to have originated with Aristotle
( | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 1div0apr 20841 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

14.3 (Future - to be reviewed and
classified) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

14.3.1 Planar incidence geometry | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | cplig 20842 | Extend class notation with the class of all planar incidence geometries. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-plig 20843* | Planar incidence geometry. I use Hilbert's "axioms" adapted to planar geometry. is the incidence relation. I could take a generic incidence relation but I'm lazy and I'm not sure the gain is worth the extra work. Much of what follows is directly borrowed from Aitken. http://public.csusm.edu/aitken_html/m410/betweenness.08.pdf (Contributed by FL, 2-Aug-2009.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | isplig 20844* | The predicate "is a planar incidence geometry". (Contributed by FL, 2-Aug-2009.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | tncp 20845* | There exist three non colinear points. (Contributed by FL, 3-Aug-2009.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | lpni 20846* | For any line, there exists a point not on the line. (Contributed by Jeff Hankins, 15-Aug-2009.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

14.3.2 Algebra preliminaries | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | crpm 20847 | Ring primes. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

RPrime | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-rprm 20848* | Define the set of prime elements in a ring. A prime element is a nonzero non-unit that satisfies an equivalent of Euclid's lemma euclemma 12787. (Contributed by Mario Carneiro, 17-Feb-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

RPrime Unit
_{r} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

14.3.3 Transitive closure | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | ctcl 20849 | Extend class notation to include the transitive closure symbol. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | crtcl 20850 | Extend class notation with transitive closure. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-trcl 20851* | Transitive closure of a relation. Experimental. (Contributed by FL, 27-Jun-2011.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-rtrcl 20852* | Reflexive-transitive closure of a relation. Experimental. (Contributed by FL, 27-Jun-2011.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

PART 15 ADDITIONAL MATERIAL ON GROUPS, RINGS,
AND FIELDS (DEPRECATED)This part contains an earlier development of groups, rings, and fields that was defined before extensible structures were introduced. Theorem grpo2grp 20901 shows the relationship between the older group definition and the extensible structure definition. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

15.1 Additional material on group
theory | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

15.1.1 Definitions and basic properties for
groups | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | cgr 20853 | Extend class notation with the class of all group operations. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | cgi 20854 | Extend class notation with a function mapping a group operation to the group's identity element. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | cgn 20855 | Extend class notation with a function mapping a group operation to the inverse function for the group. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | cgs 20856 | Extend class notation with a function mapping a group operation to the division (or subtraction) operation for the group. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | cgx 20857 | Extend class notation with a function mapping a group operation to the power operation for the group. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-grpo 20858* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-gid 20859* | 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 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-ginv 20860* | Define a function that maps a group operation to the group's inverse function. (Contributed by NM, 26-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-gdiv 20861* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-gx 20862* | Define a function that maps a group operation to the group's power operation. (Contributed by Paul Chapman, 17-Apr-2009.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | isgrpo 20863* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | isgrpo2 20864* | The predicate "is a group operation." (Contributed by NM, 23-Oct-2012.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | isgrpoi 20865* | Properties that determine a group operation. Read as . (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpofo 20866 | A group operation maps onto the group's underlying set. (Contributed by NM, 30-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpocl 20867 | Closure law for a group operation. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpolidinv 20868* | A group has a left identity element, and every member has a left inverse. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpon0 20869 | The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpoass 20870 | A group operation is associative. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpoidinvlem1 20871 | Lemma for grpoidinv 20875. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpoidinvlem2 20872 | Lemma for grpoidinv 20875. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpoidinvlem3 20873* | Lemma for grpoidinv 20875. (Contributed by NM, 11-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpoidinvlem4 20874* | Lemma for grpoidinv 20875. (Contributed by NM, 14-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpoidinv 20875* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpoideu 20876* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grporndm 20877 | A group's range in terms of its domain. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 0ngrp 20878 | The empty set is not a group. (Contributed by NM, 25-Apr-2007.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grporn 20879 | The range of a group operation. Useful for satisfying group base set hypotheses of the form . (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | gidval 20880* | The value of the identity element of a group. (Contributed by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | fngid 20881 | GId is a function. (Contributed by FL, 5-Feb-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grposn 20882 | The group operation for the singleton group. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpoidval 20883* | Lemma for grpoidcl 20884 and others. (Contributed by NM, 5-Feb-2010.) (Proof shortened by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpoidcl 20884 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpoidinv2 20885* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpolid 20886 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grporid 20887 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grporcan 20888 | Right cancellation law for groups. (Contributed by NM, 26-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpoinveu 20889* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpoid 20890 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpoinvfval 20891* | The inverse function of a group. (Contributed by NM, 26-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpoinvval 20892* | The inverse of a group element. (Contributed by NM, 26-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpoinvcl 20893 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpoinv 20894 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpolinv 20895 | The left inverse of a group element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grporinv 20896 | The right inverse of a group element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpoinvid1 20897 | The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpoinvid2 20898 | The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpoinvid 20899 | The inverse of the identity element of a group. (Contributed by NM, 4-Dec-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpolcan 20900 | Left cancellation law for groups. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |