Home | Metamath
Proof ExplorerTheorem List
(p. 209 of 323)
| < 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-21500) |
Hilbert Space Explorer
(21501-23023) |
Users' Mathboxes
(23024-32227) |

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

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

Theorem | ex-natded5.7-2 20801 | A more efficient proof of Theorem 5.7 of [Clemente] p. 19. Compare with ex-natded5.7 20800. (Contributed by Mario Carneiro, 9-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded5.8 20802 |
Theorem 5.8 of [Clemente] p. 20, 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, using more of Metamath and MPE's capabilities, is shown in ex-natded5.8-2 20803. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

Theorem | ex-natded5.13 20804 |
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 20805.
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 20805 | A more efficient proof of Theorem 5.13 of [Clemente] p. 20. Compare with ex-natded5.13 20804. (Contributed by Mario Carneiro, 9-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | ex-natded9.20 20806 |
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 20807. (Proof modification is discouraged.) (Contributed by David A. Wheeler, 19-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

Theorem | ex-natded9.26 20808* |
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 20809. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by David A. Wheeler, 18-Feb-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem | 1kp2ke3k 20835 |
Example for df-dec 10127, 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 10127 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 20836 | Example for df-fl 10927. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

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

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

Theorem | avril1 20838 |
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 20839 |
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 20840 | 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 20841 |
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 20842 |
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 20843 | 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 20844 | Extend class notation with the class of all planar incidence geometries. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Definition | df-plig 20845* | 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 20846* | The predicate "is a planar incidence geometry". (Contributed by FL, 2-Aug-2009.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

Theorem | lpni 20848* | 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 20849 | Ring primes. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

Definition | df-rprm 20850* | 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 12789. (Contributed by Mario Carneiro, 17-Feb-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

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

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

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

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

Definition | df-rtrcl 20854* | 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 20903 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 20855 | Extend class notation with the class of all group operations. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

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

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

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

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

Definition | df-grpo 20860* | 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 20861* | 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 20862* | 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 20863* | 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 20864* | 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 20865* | 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 20866* | The predicate "is a group operation." (Contributed by NM, 23-Oct-2012.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

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

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

Theorem | grpolidinv 20870* | 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 20871 | The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

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

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

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

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

Theorem | grpoidinv 20877* | 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 20878* | 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 20879 | A group's range in terms of its domain. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

Theorem | grporn 20881 | 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 20882* | The value of the identity element of a group. (Contributed by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

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

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

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

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

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

Theorem | grpoidcl 20886 | 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 20887* | 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 20888 | 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 20889 | 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 20890 | Right cancellation law for groups. (Contributed by NM, 26-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | grpoinveu 20891* | 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 20892 | 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 20893* | 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 20894* | 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 20895 | 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 20896 | 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 20897 | The left inverse of a group element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

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

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

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

Theorem | grpoinvid1 20899 | 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 20900 | The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

GId |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |