Home | Metamath
Proof Explorer Theorem List (p. 182 of 450) | < 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: | Metamath Proof Explorer
(1-28698) |
Hilbert Space Explorer
(28699-30221) |
Users' Mathboxes
(30222-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sgrpssmgm 18101 | The class of all semigroups is a proper subclass of the class of all magmas. (Contributed by AV, 29-Jan-2020.) |
⊢ Smgrp ⊊ Mgm | ||
Theorem | mndsssgrp 18102 | The class of all monoids is a proper subclass of the class of all semigroups. (Contributed by AV, 29-Jan-2020.) |
⊢ Mnd ⊊ Smgrp | ||
Theorem | pwmndgplus 18103* | The operation of the monoid of the power set of a class 𝐴 under union. (Contributed by AV, 27-Feb-2024.) |
⊢ (Base‘𝑀) = 𝒫 𝐴 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝒫 𝐴, 𝑦 ∈ 𝒫 𝐴 ↦ (𝑥 ∪ 𝑦)) ⇒ ⊢ ((𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴) → (𝑋(+g‘𝑀)𝑌) = (𝑋 ∪ 𝑌)) | ||
Theorem | pwmndid 18104* | The identity of the monoid of the power set of a class 𝐴 under union is the empty set. (Contributed by AV, 27-Feb-2024.) |
⊢ (Base‘𝑀) = 𝒫 𝐴 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝒫 𝐴, 𝑦 ∈ 𝒫 𝐴 ↦ (𝑥 ∪ 𝑦)) ⇒ ⊢ (0g‘𝑀) = ∅ | ||
Theorem | pwmnd 18105* | The power set of a class 𝐴 is a monoid under union. (Contributed by AV, 27-Feb-2024.) |
⊢ (Base‘𝑀) = 𝒫 𝐴 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝒫 𝐴, 𝑦 ∈ 𝒫 𝐴 ↦ (𝑥 ∪ 𝑦)) ⇒ ⊢ 𝑀 ∈ Mnd | ||
Syntax | cgrp 18106 | Extend class notation with class of all groups. |
class Grp | ||
Syntax | cminusg 18107 | Extend class notation with inverse of group element. |
class invg | ||
Syntax | csg 18108 | Extend class notation with group subtraction (or division) operation. |
class -g | ||
Definition | df-grp 18109* | Define class of all groups. A group is a monoid (df-mnd 17915) whose internal operation is such that every element admits a left inverse (which can be proven to be a two-sided inverse). Thus, a group 𝐺 is an algebraic structure formed from a base set of elements (notated (Base‘𝐺) per df-base 16492) and an internal group operation (notated (+g‘𝐺) per df-plusg 16581). The operation combines any two elements of the group base set and must satisfy the 4 group axioms: closure (the result of the group operation must always be a member of the base set, see grpcl 18114), associativity (so ((𝑎+g𝑏)+g𝑐) = (𝑎+g(𝑏+g𝑐)) for any a, b, c, see grpass 18115), identity (there must be an element 𝑒 = (0g‘𝐺) such that 𝑒+g𝑎 = 𝑎+g𝑒 = 𝑎 for any a), and inverse (for each element a in the base set, there must be an element 𝑏 = invg𝑎 in the base set such that 𝑎+g𝑏 = 𝑏+g𝑎 = 𝑒). It can be proven that the identity element is unique (grpideu 18117). Groups need not be commutative; a commutative group is an Abelian group (see df-abl 18912). Subgroups can often be formed from groups, see df-subg 18279. An example of an (Abelian) group is the set of complex numbers ℂ over the group operation + (addition), as proven in cnaddablx 18991; an Abelian group is a group as proven in ablgrp 18914. Other structures include groups, including unital rings (df-ring 19302) and fields (df-field 19508). (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ Grp = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)} | ||
Definition | df-minusg 18110* | Define inverse of group element. (Contributed by NM, 24-Aug-2011.) |
⊢ invg = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔)))) | ||
Definition | df-sbg 18111* | Define group subtraction (also called division for multiplicative groups). (Contributed by NM, 31-Mar-2014.) |
⊢ -g = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦)))) | ||
Theorem | isgrp 18112* | The predicate "is a group." (This theorem demonstrates the use of symbols as variable names, first proposed by FL in 2010.) (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp ↔ (𝐺 ∈ Mnd ∧ ∀𝑎 ∈ 𝐵 ∃𝑚 ∈ 𝐵 (𝑚 + 𝑎) = 0 )) | ||
Theorem | grpmnd 18113 | A group is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | ||
Theorem | grpcl 18114 | Closure of the operation of a group. (Contributed by NM, 14-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) | ||
Theorem | grpass 18115 | A group operation is associative. (Contributed by NM, 14-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) | ||
Theorem | grpinvex 18116* | Every member of a group has a left inverse. (Contributed by NM, 16-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑋) = 0 ) | ||
Theorem | grpideu 18117* | The two-sided identity element of a group is unique. Lemma 2.2.1(a) of [Herstein] p. 55. (Contributed by NM, 16-Aug-2011.) (Revised by Mario Carneiro, 8-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → ∃!𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑢 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑢) = 𝑥)) | ||
Theorem | grpplusf 18118 | The group addition operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐹 = (+𝑓‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝐹:(𝐵 × 𝐵)⟶𝐵) | ||
Theorem | grpplusfo 18119 | The group addition operation is a function onto the base set/set of group elements. (Contributed by NM, 30-Oct-2006.) (Revised by AV, 30-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐹 = (+𝑓‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝐹:(𝐵 × 𝐵)–onto→𝐵) | ||
Theorem | resgrpplusfrn 18120 | The underlying set of a group operation which is a restriction of a structure. (Contributed by Paul Chapman, 25-Mar-2008.) (Revised by AV, 30-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) & ⊢ 𝐹 = (+𝑓‘𝐻) ⇒ ⊢ ((𝐻 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → 𝑆 = ran 𝐹) | ||
Theorem | grppropd 18121* | If two structures have the same group components (properties), one is a group iff the other one is. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ Grp ↔ 𝐿 ∈ Grp)) | ||
Theorem | grpprop 18122 | If two structures have the same group components (properties), one is a group iff the other one is. (Contributed by NM, 11-Oct-2013.) |
⊢ (Base‘𝐾) = (Base‘𝐿) & ⊢ (+g‘𝐾) = (+g‘𝐿) ⇒ ⊢ (𝐾 ∈ Grp ↔ 𝐿 ∈ Grp) | ||
Theorem | grppropstr 18123 | Generalize a specific 2-element group 𝐿 to show that any set 𝐾 with the same (relevant) properties is also a group. (Contributed by NM, 28-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ (Base‘𝐾) = 𝐵 & ⊢ (+g‘𝐾) = + & ⊢ 𝐿 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉} ⇒ ⊢ (𝐾 ∈ Grp ↔ 𝐿 ∈ Grp) | ||
Theorem | grpss 18124 | Show that a structure extending a constructed group (e.g., a ring) is also a group. This allows us to prove that a constructed potential ring 𝑅 is a group before we know that it is also a ring. (Theorem ringgrp 19305, on the other hand, requires that we know in advance that 𝑅 is a ring.) (Contributed by NM, 11-Oct-2013.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉} & ⊢ 𝑅 ∈ V & ⊢ 𝐺 ⊆ 𝑅 & ⊢ Fun 𝑅 ⇒ ⊢ (𝐺 ∈ Grp ↔ 𝑅 ∈ Grp) | ||
Theorem | isgrpd2e 18125* | Deduce a group from its properties. In this version of isgrpd2 18126, we don't assume there is an expression for the inverse of 𝑥. (Contributed by NM, 10-Aug-2013.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ (𝜑 → 0 = (0g‘𝐺)) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 ) ⇒ ⊢ (𝜑 → 𝐺 ∈ Grp) | ||
Theorem | isgrpd2 18126* | Deduce a group from its properties. 𝑁 (negative) is normally dependent on 𝑥 i.e. read it as 𝑁(𝑥). Note: normally we don't use a 𝜑 antecedent on hypotheses that name structure components, since they can be eliminated with eqid 2824, but we make an exception for theorems such as isgrpd2 18126, ismndd 17936, and islmodd 19643 since theorems using them often rewrite the structure components. (Contributed by NM, 10-Aug-2013.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ (𝜑 → 0 = (0g‘𝐺)) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑁 + 𝑥) = 0 ) ⇒ ⊢ (𝜑 → 𝐺 ∈ Grp) | ||
Theorem | isgrpde 18127* | Deduce a group from its properties. In this version of isgrpd 18128, we don't assume there is an expression for the inverse of 𝑥. (Contributed by NM, 6-Jan-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 0 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 ) ⇒ ⊢ (𝜑 → 𝐺 ∈ Grp) | ||
Theorem | isgrpd 18128* | Deduce a group from its properties. Unlike isgrpd2 18126, this one goes straight from the base properties rather than going through Mnd. 𝑁 (negative) is normally dependent on 𝑥 i.e. read it as 𝑁(𝑥). (Contributed by NM, 6-Jun-2013.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 0 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑁 + 𝑥) = 0 ) ⇒ ⊢ (𝜑 → 𝐺 ∈ Grp) | ||
Theorem | isgrpi 18129* | Properties that determine a group. 𝑁 (negative) is normally dependent on 𝑥 i.e. read it as 𝑁(𝑥). (Contributed by NM, 3-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ 0 ∈ 𝐵 & ⊢ (𝑥 ∈ 𝐵 → ( 0 + 𝑥) = 𝑥) & ⊢ (𝑥 ∈ 𝐵 → 𝑁 ∈ 𝐵) & ⊢ (𝑥 ∈ 𝐵 → (𝑁 + 𝑥) = 0 ) ⇒ ⊢ 𝐺 ∈ Grp | ||
Theorem | grpsgrp 18130 | A group is a semigroup. (Contributed by AV, 28-Aug-2021.) |
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Smgrp) | ||
Theorem | dfgrp2 18131* | Alternate definition of a group as semigroup with a left identity and a left inverse for each element. This "definition" is weaker than df-grp 18109, based on the definition of a monoid which provides a left and a right identity. (Contributed by AV, 28-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp ↔ (𝐺 ∈ Smgrp ∧ ∃𝑛 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖 ∈ 𝐵 (𝑖 + 𝑥) = 𝑛))) | ||
Theorem | dfgrp2e 18132* | Alternate definition of a group as a set with a closed, associative operation, a left identity and a left inverse for each element. Alternate definition in [Lang] p. 7. (Contributed by NM, 10-Oct-2006.) (Revised by AV, 28-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp ↔ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) ∧ ∃𝑛 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖 ∈ 𝐵 (𝑖 + 𝑥) = 𝑛))) | ||
Theorem | isgrpix 18133* | Properties that determine a group. Read 𝑁 as 𝑁(𝑥). Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use. (New usage is discouraged.) (Contributed by NM, 4-Sep-2011.) |
⊢ 𝐵 ∈ V & ⊢ + ∈ V & ⊢ 𝐺 = {〈1, 𝐵〉, 〈2, + 〉} & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ 0 ∈ 𝐵 & ⊢ (𝑥 ∈ 𝐵 → ( 0 + 𝑥) = 𝑥) & ⊢ (𝑥 ∈ 𝐵 → 𝑁 ∈ 𝐵) & ⊢ (𝑥 ∈ 𝐵 → (𝑁 + 𝑥) = 0 ) ⇒ ⊢ 𝐺 ∈ Grp | ||
Theorem | grpidcl 18134 | The identity element of a group belongs to the group. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵) | ||
Theorem | grpbn0 18135 | The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅) | ||
Theorem | grplid 18136 | The identity element of a group is a left identity. (Contributed by NM, 18-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) | ||
Theorem | grprid 18137 | The identity element of a group is a right identity. (Contributed by NM, 18-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋) | ||
Theorem | grpn0 18138 | A group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (Revised by Mario Carneiro, 2-Dec-2014.) |
⊢ (𝐺 ∈ Grp → 𝐺 ≠ ∅) | ||
Theorem | hashfingrpnn 18139 | A finite group has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ) | ||
Theorem | grprcan 18140 | Right cancellation law for groups. (Contributed by NM, 24-Aug-2011.) (Proof shortened by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑍) = (𝑌 + 𝑍) ↔ 𝑋 = 𝑌)) | ||
Theorem | grpinveu 18141* | The left inverse element of a group is unique. Lemma 2.2.1(b) of [Herstein] p. 55. (Contributed by NM, 24-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ∃!𝑦 ∈ 𝐵 (𝑦 + 𝑋) = 0 ) | ||
Theorem | grpid 18142 | Two ways of saying that an element of a group is the identity element. Provides a convenient way to compute the value of the identity element. (Contributed by NM, 24-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ((𝑋 + 𝑋) = 𝑋 ↔ 0 = 𝑋)) | ||
Theorem | isgrpid2 18143 | Properties showing that an element 𝑍 is the identity element of a group. (Contributed by NM, 7-Aug-2013.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → ((𝑍 ∈ 𝐵 ∧ (𝑍 + 𝑍) = 𝑍) ↔ 0 = 𝑍)) | ||
Theorem | grpidd2 18144* | Deduce the identity element of a group from its properties. Useful in conjunction with isgrpd 18128. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ (𝜑 → 0 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) & ⊢ (𝜑 → 𝐺 ∈ Grp) ⇒ ⊢ (𝜑 → 0 = (0g‘𝐺)) | ||
Theorem | grpinvfval 18145* | The inverse function of a group. For a shorter proof using ax-rep 5193, see grpinvfvalALT 18146. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 7-Aug-2013.) Remove dependency on ax-rep 5193. (Revised by Rohan Ridenour, 13-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ 𝑁 = (𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 )) | ||
Theorem | grpinvfvalALT 18146* | Shorter proof of grpinvfval 18145 using ax-rep 5193. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 7-Aug-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ 𝑁 = (𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 )) | ||
Theorem | grpinvval 18147* | The inverse of a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 7-Aug-2013.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝐵 → (𝑁‘𝑋) = (℩𝑦 ∈ 𝐵 (𝑦 + 𝑋) = 0 )) | ||
Theorem | grpinvfn 18148 | Functionality of the group inverse function. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ 𝑁 Fn 𝐵 | ||
Theorem | grpinvfvi 18149 | The group inverse function is compatible with identity-function protection. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ 𝑁 = (invg‘( I ‘𝐺)) | ||
Theorem | grpsubfval 18150* | Group subtraction (division) operation. For a shorter proof using ax-rep 5193, see grpsubfvalALT 18151. (Contributed by NM, 31-Mar-2014.) (Revised by Stefan O'Rear, 27-Mar-2015.) Remove dependency on ax-rep 5193. (Revised by Rohan Ridenour, 17-Aug-2023.) (Proof shortened by AV, 19-Feb-2024.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ − = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦))) | ||
Theorem | grpsubfvalALT 18151* | Shorter proof of grpsubfval 18150 using ax-rep 5193. (Contributed by NM, 31-Mar-2014.) (Revised by Stefan O'Rear, 27-Mar-2015.) (Proof shortened by AV, 19-Feb-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ − = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦))) | ||
Theorem | grpsubval 18152 | Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 13-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 + (𝐼‘𝑌))) | ||
Theorem | grpinvf 18153 | The group inversion operation is a function on the base set. (Contributed by Mario Carneiro, 4-May-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝑁:𝐵⟶𝐵) | ||
Theorem | grpinvcl 18154 | A group element's inverse is a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 4-May-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) ∈ 𝐵) | ||
Theorem | grplinv 18155 | The left inverse of a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ((𝑁‘𝑋) + 𝑋) = 0 ) | ||
Theorem | grprinv 18156 | The right inverse of a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 + (𝑁‘𝑋)) = 0 ) | ||
Theorem | grpinvid1 18157 | The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 24-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑁‘𝑋) = 𝑌 ↔ (𝑋 + 𝑌) = 0 )) | ||
Theorem | grpinvid2 18158 | The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 24-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑁‘𝑋) = 𝑌 ↔ (𝑌 + 𝑋) = 0 )) | ||
Theorem | isgrpinv 18159* | Properties showing that a function 𝑀 is the inverse function of a group. (Contributed by NM, 7-Aug-2013.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → ((𝑀:𝐵⟶𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑀‘𝑥) + 𝑥) = 0 ) ↔ 𝑁 = 𝑀)) | ||
Theorem | grplrinv 18160* | In a group, every member has a left and right inverse. (Contributed by AV, 1-Sep-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑦 + 𝑥) = 0 ∧ (𝑥 + 𝑦) = 0 )) | ||
Theorem | grpidinv2 18161* | A group's properties using the explicit identity element. (Contributed by NM, 5-Feb-2010.) (Revised by AV, 1-Sep-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵) → ((( 0 + 𝐴) = 𝐴 ∧ (𝐴 + 0 ) = 𝐴) ∧ ∃𝑦 ∈ 𝐵 ((𝑦 + 𝐴) = 0 ∧ (𝐴 + 𝑦) = 0 ))) | ||
Theorem | grpidinv 18162* | A group has a left and right identity element, and every member has a left and right inverse. (Contributed by NM, 14-Oct-2006.) (Revised by AV, 1-Sep-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → ∃𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 (((𝑢 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑢) = 𝑥) ∧ ∃𝑦 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑢 ∧ (𝑥 + 𝑦) = 𝑢))) | ||
Theorem | grpinvid 18163 | The inverse of the identity element of a group. (Contributed by NM, 24-Aug-2011.) |
⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → (𝑁‘ 0 ) = 0 ) | ||
Theorem | grplcan 18164 | Left cancellation law for groups. (Contributed by NM, 25-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑍 + 𝑋) = (𝑍 + 𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | grpasscan1 18165 | An associative cancellation law for groups. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by AV, 30-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + ((𝑁‘𝑋) + 𝑌)) = 𝑌) | ||
Theorem | grpasscan2 18166 | An associative cancellation law for groups. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 + (𝑁‘𝑌)) + 𝑌) = 𝑋) | ||
Theorem | grpidrcan 18167 | If right adding an element of a group to an arbitrary element of the group results in this element, the added element is the identity element and vice versa. (Contributed by AV, 15-Mar-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑍) = 𝑋 ↔ 𝑍 = 0 )) | ||
Theorem | grpidlcan 18168 | If left adding an element of a group to an arbitrary element of the group results in this element, the added element is the identity element and vice versa. (Contributed by AV, 15-Mar-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑍 + 𝑋) = 𝑋 ↔ 𝑍 = 0 )) | ||
Theorem | grpinvinv 18169 | Double inverse law for groups. Lemma 2.2.1(c) of [Herstein] p. 55. (Contributed by NM, 31-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁‘(𝑁‘𝑋)) = 𝑋) | ||
Theorem | grpinvcnv 18170 | The group inverse is its own inverse function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → ◡𝑁 = 𝑁) | ||
Theorem | grpinv11 18171 | The group inverse is one-to-one. (Contributed by NM, 22-Mar-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑁‘𝑋) = (𝑁‘𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | grpinvf1o 18172 | The group inverse is a one-to-one onto function. (Contributed by NM, 22-Oct-2014.) (Proof shortened by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) ⇒ ⊢ (𝜑 → 𝑁:𝐵–1-1-onto→𝐵) | ||
Theorem | grpinvnz 18173 | The inverse of a nonzero group element is not zero. (Contributed by Stefan O'Rear, 27-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝑁‘𝑋) ≠ 0 ) | ||
Theorem | grpinvnzcl 18174 | The inverse of a nonzero group element is a nonzero group element. (Contributed by Stefan O'Rear, 27-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ (𝐵 ∖ { 0 })) → (𝑁‘𝑋) ∈ (𝐵 ∖ { 0 })) | ||
Theorem | grpsubinv 18175 | Subtraction of an inverse. (Contributed by NM, 7-Apr-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 − (𝑁‘𝑌)) = (𝑋 + 𝑌)) | ||
Theorem | grplmulf1o 18176* | Left multiplication by a group element is a bijection on any group. (Contributed by Mario Carneiro, 17-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑋 + 𝑥)) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → 𝐹:𝐵–1-1-onto→𝐵) | ||
Theorem | grpinvpropd 18177* | If two structures have the same group components (properties), they have the same group inversion function. (Contributed by Mario Carneiro, 27-Nov-2014.) (Revised by Stefan O'Rear, 21-Mar-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (invg‘𝐾) = (invg‘𝐿)) | ||
Theorem | grpidssd 18178* | If the base set of a group is contained in the base set of another group, and the group operation of the group is the restriction of the group operation of the other group to its base set, then both groups have the same identity element. (Contributed by AV, 15-Mar-2019.) |
⊢ (𝜑 → 𝑀 ∈ Grp) & ⊢ (𝜑 → 𝑆 ∈ Grp) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝐵 ⊆ (Base‘𝑀)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥(+g‘𝑀)𝑦) = (𝑥(+g‘𝑆)𝑦)) ⇒ ⊢ (𝜑 → (0g‘𝑀) = (0g‘𝑆)) | ||
Theorem | grpinvssd 18179* | If the base set of a group is contained in the base set of another group, and the group operation of the group is the restriction of the group operation of the other group to its base set, then the elements of the first group have the same inverses in both groups. (Contributed by AV, 15-Mar-2019.) |
⊢ (𝜑 → 𝑀 ∈ Grp) & ⊢ (𝜑 → 𝑆 ∈ Grp) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ (𝜑 → 𝐵 ⊆ (Base‘𝑀)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥(+g‘𝑀)𝑦) = (𝑥(+g‘𝑆)𝑦)) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐵 → ((invg‘𝑆)‘𝑋) = ((invg‘𝑀)‘𝑋))) | ||
Theorem | grpinvadd 18180 | The inverse of the group operation reverses the arguments. Lemma 2.2.1(d) of [Herstein] p. 55. (Contributed by NM, 27-Oct-2006.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑁‘(𝑋 + 𝑌)) = ((𝑁‘𝑌) + (𝑁‘𝑋))) | ||
Theorem | grpsubf 18181 | Functionality of group subtraction. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → − :(𝐵 × 𝐵)⟶𝐵) | ||
Theorem | grpsubcl 18182 | Closure of group subtraction. (Contributed by NM, 31-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) ∈ 𝐵) | ||
Theorem | grpsubrcan 18183 | Right cancellation law for group subtraction. (Contributed by NM, 31-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑍) = (𝑌 − 𝑍) ↔ 𝑋 = 𝑌)) | ||
Theorem | grpinvsub 18184 | Inverse of a group subtraction. (Contributed by NM, 9-Sep-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑁‘(𝑋 − 𝑌)) = (𝑌 − 𝑋)) | ||
Theorem | grpinvval2 18185 | A df-neg 10876-like equation for inverse in terms of group subtraction. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) = ( 0 − 𝑋)) | ||
Theorem | grpsubid 18186 | Subtraction of a group element from itself. (Contributed by NM, 31-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 − 𝑋) = 0 ) | ||
Theorem | grpsubid1 18187 | Subtraction of the identity from a group element. (Contributed by Mario Carneiro, 14-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 − 0 ) = 𝑋) | ||
Theorem | grpsubeq0 18188 | If the difference between two group elements is zero, they are equal. (subeq0 10915 analog.) (Contributed by NM, 31-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 − 𝑌) = 0 ↔ 𝑋 = 𝑌)) | ||
Theorem | grpsubadd0sub 18189 | Subtraction expressed as addition of the difference of the identity element and the subtrahend. (Contributed by AV, 9-Nov-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 + ( 0 − 𝑌))) | ||
Theorem | grpsubadd 18190 | Relationship between group subtraction and addition. (Contributed by NM, 31-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) = 𝑍 ↔ (𝑍 + 𝑌) = 𝑋)) | ||
Theorem | grpsubsub 18191 | Double group subtraction. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 − (𝑌 − 𝑍)) = (𝑋 + (𝑍 − 𝑌))) | ||
Theorem | grpaddsubass 18192 | Associative-type law for group subtraction and addition. (Contributed by NM, 16-Apr-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) − 𝑍) = (𝑋 + (𝑌 − 𝑍))) | ||
Theorem | grppncan 18193 | Cancellation law for subtraction (pncan 10895 analog). (Contributed by NM, 16-Apr-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 + 𝑌) − 𝑌) = 𝑋) | ||
Theorem | grpnpcan 18194 | Cancellation law for subtraction (npcan 10898 analog). (Contributed by NM, 19-Apr-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 − 𝑌) + 𝑌) = 𝑋) | ||
Theorem | grpsubsub4 18195 | Double group subtraction (subsub4 10922 analog). (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) − 𝑍) = (𝑋 − (𝑍 + 𝑌))) | ||
Theorem | grppnpcan2 18196 | Cancellation law for mixed addition and subtraction. (pnpcan2 10929 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑍) − (𝑌 + 𝑍)) = (𝑋 − 𝑌)) | ||
Theorem | grpnpncan 18197 | Cancellation law for group subtraction. (npncan 10910 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) + (𝑌 − 𝑍)) = (𝑋 − 𝑍)) | ||
Theorem | grpnpncan0 18198 | Cancellation law for group subtraction (npncan2 10916 analog). (Contributed by AV, 24-Nov-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑋 − 𝑌) + (𝑌 − 𝑋)) = 0 ) | ||
Theorem | grpnnncan2 18199 | Cancellation law for group subtraction. (nnncan2 10926 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑍) − (𝑌 − 𝑍)) = (𝑋 − 𝑌)) | ||
Theorem | dfgrp3lem 18200* | Lemma for dfgrp3 18201. (Contributed by AV, 28-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)) → ∃𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ((𝑢 + 𝑎) = 𝑎 ∧ ∃𝑖 ∈ 𝐵 (𝑖 + 𝑎) = 𝑢)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |