Home | Metamath
Proof Explorer Theorem List (p. 183 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mulgneg2 18201 | Group multiple (exponentiation) operation at a negative integer. (Contributed by Mario Carneiro, 13-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑁 · 𝑋) = (𝑁 · (𝐼‘𝑋))) | ||
Theorem | mulgnnass 18202 | Product of group multiples, for positive multiples in a semigroup. (Contributed by Mario Carneiro, 13-Dec-2014.) (Revised by AV, 29-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) | ||
Theorem | mulgnn0ass 18203 | Product of group multiples, generalized to ℕ0. (Contributed by Mario Carneiro, 13-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) | ||
Theorem | mulgass 18204 | Product of group multiples, generalized to ℤ. (Contributed by Mario Carneiro, 13-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) | ||
Theorem | mulgassr 18205 | Reversed product of group multiples. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑁 · 𝑀) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) | ||
Theorem | mulgmodid 18206 | Casting out multiples of the identity element leaves the group multiple unchanged. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → ((𝑁 mod 𝑀) · 𝑋) = (𝑁 · 𝑋)) | ||
Theorem | mulgsubdir 18207 | Subtraction of a group element from itself. (Contributed by Mario Carneiro, 13-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 − 𝑁) · 𝑋) = ((𝑀 · 𝑋) − (𝑁 · 𝑋))) | ||
Theorem | mhmmulg 18208 | A homomorphism of monoids preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ × = (.g‘𝐻) ⇒ ⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑁 · 𝑋)) = (𝑁 × (𝐹‘𝑋))) | ||
Theorem | mulgpropd 18209* | Two structures with the same group-nature have the same group multiple function. 𝐾 is expected to either be V (when strong equality is available) or 𝐵 (when closure is available). (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ · = (.g‘𝐺) & ⊢ × = (.g‘𝐻) & ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐻)) & ⊢ (𝜑 → 𝐵 ⊆ 𝐾) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑥(+g‘𝐺)𝑦) ∈ 𝐾) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦)) ⇒ ⊢ (𝜑 → · = × ) | ||
Theorem | submmulgcl 18210 | Closure of the group multiple (exponentiation) operation in a submonoid. (Contributed by Mario Carneiro, 13-Jan-2015.) |
⊢ ∙ = (.g‘𝐺) ⇒ ⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆) → (𝑁 ∙ 𝑋) ∈ 𝑆) | ||
Theorem | submmulg 18211 | A group multiple is the same if evaluated in a submonoid. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ ∙ = (.g‘𝐺) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) & ⊢ · = (.g‘𝐻) ⇒ ⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆) → (𝑁 ∙ 𝑋) = (𝑁 · 𝑋)) | ||
Theorem | pwsmulg 18212 | Value of a group multiple in a structure power. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ ∙ = (.g‘𝑌) & ⊢ · = (.g‘𝑅) ⇒ ⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉) ∧ (𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼)) → ((𝑁 ∙ 𝑋)‘𝐴) = (𝑁 · (𝑋‘𝐴))) | ||
Syntax | csubg 18213 | Extend class notation with all subgroups of a group. |
class SubGrp | ||
Syntax | cnsg 18214 | Extend class notation with all normal subgroups of a group. |
class NrmSGrp | ||
Syntax | cqg 18215 | Quotient group equivalence class. |
class ~QG | ||
Definition | df-subg 18216* | Define a subgroup of a group as a set of elements that is a group in its own right. Equivalently (issubg2 18234), a subgroup is a subset of the group that is closed for the group internal operation (see subgcl 18229), contains the neutral element of the group (see subg0 18225) and contains the inverses for all of its elements (see subginvcl 18228). (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ SubGrp = (𝑤 ∈ Grp ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Grp}) | ||
Definition | df-nsg 18217* | Define the equivalence relation in a quotient ring or quotient group (where 𝑖 is a two-sided ideal or a normal subgroup). For non-normal subgroups this generates the left cosets. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ NrmSGrp = (𝑤 ∈ Grp ↦ {𝑠 ∈ (SubGrp‘𝑤) ∣ [(Base‘𝑤) / 𝑏][(+g‘𝑤) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)}) | ||
Definition | df-eqg 18218* | Define the equivalence relation in a group generated by a subgroup. More precisely, if 𝐺 is a group and 𝐻 is a subgroup, then 𝐺 ~QG 𝐻 is the equivalence relation on 𝐺 associated with the left cosets of 𝐻. A typical application of this definition is the construction of the quotient group (resp. ring) of a group (resp. ring) by a normal subgroup (resp. two-sided ideal). (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ ~QG = (𝑟 ∈ V, 𝑖 ∈ V ↦ {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑟) ∧ (((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦) ∈ 𝑖)}) | ||
Theorem | issubg 18219 | The subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)) | ||
Theorem | subgss 18220 | A subgroup is a subset. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝐵) | ||
Theorem | subgid 18221 | A group is a subgroup of itself. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝐵 ∈ (SubGrp‘𝐺)) | ||
Theorem | subggrp 18222 | A subgroup is a group. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp) | ||
Theorem | subgbas 18223 | The base of the restricted group in a subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 = (Base‘𝐻)) | ||
Theorem | subgrcl 18224 | Reverse closure for the subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) | ||
Theorem | subg0 18225 | A subgroup of a group must have the same identity as the group. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 = (0g‘𝐻)) | ||
Theorem | subginv 18226 | The inverse of an element in a subgroup is the same as the inverse in the larger group. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ 𝐽 = (invg‘𝐻) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝑆) → (𝐼‘𝑋) = (𝐽‘𝑋)) | ||
Theorem | subg0cl 18227 | The group identity is an element of any subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑆) | ||
Theorem | subginvcl 18228 | The inverse of an element is closed in a subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝑆) → (𝐼‘𝑋) ∈ 𝑆) | ||
Theorem | subgcl 18229 | A subgroup is closed under group operation. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) ∈ 𝑆) | ||
Theorem | subgsubcl 18230 | A subgroup is closed under group subtraction. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 − 𝑌) ∈ 𝑆) | ||
Theorem | subgsub 18231 | The subtraction of elements in a subgroup is the same as subtraction in the group. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ − = (-g‘𝐺) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) & ⊢ 𝑁 = (-g‘𝐻) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 − 𝑌) = (𝑋𝑁𝑌)) | ||
Theorem | subgmulgcl 18232 | Closure of the group multiple (exponentiation) operation in a subgroup. (Contributed by Mario Carneiro, 13-Jan-2015.) |
⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) ∈ 𝑆) | ||
Theorem | subgmulg 18233 | A group multiple is the same if evaluated in a subgroup. (Contributed by Mario Carneiro, 15-Jan-2015.) |
⊢ · = (.g‘𝐺) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) & ⊢ ∙ = (.g‘𝐻) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) = (𝑁 ∙ 𝑋)) | ||
Theorem | issubg2 18234* | Characterize the subgroups of a group by closure properties. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)))) | ||
Theorem | issubgrpd2 18235* | Prove a subgroup by closure (definition version). (Contributed by Stefan O'Rear, 7-Dec-2014.) |
⊢ (𝜑 → 𝑆 = (𝐼 ↾s 𝐷)) & ⊢ (𝜑 → 0 = (0g‘𝐼)) & ⊢ (𝜑 → + = (+g‘𝐼)) & ⊢ (𝜑 → 𝐷 ⊆ (Base‘𝐼)) & ⊢ (𝜑 → 0 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 + 𝑦) ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((invg‘𝐼)‘𝑥) ∈ 𝐷) & ⊢ (𝜑 → 𝐼 ∈ Grp) ⇒ ⊢ (𝜑 → 𝐷 ∈ (SubGrp‘𝐼)) | ||
Theorem | issubgrpd 18236* | Prove a subgroup by closure. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
⊢ (𝜑 → 𝑆 = (𝐼 ↾s 𝐷)) & ⊢ (𝜑 → 0 = (0g‘𝐼)) & ⊢ (𝜑 → + = (+g‘𝐼)) & ⊢ (𝜑 → 𝐷 ⊆ (Base‘𝐼)) & ⊢ (𝜑 → 0 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 + 𝑦) ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((invg‘𝐼)‘𝑥) ∈ 𝐷) & ⊢ (𝜑 → 𝐼 ∈ Grp) ⇒ ⊢ (𝜑 → 𝑆 ∈ Grp) | ||
Theorem | issubg3 18237* | A subgroup is a symmetric submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ∈ (SubMnd‘𝐺) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆))) | ||
Theorem | issubg4 18238* | A subgroup is a nonempty subset of the group closed under subtraction. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 − 𝑦) ∈ 𝑆))) | ||
Theorem | grpissubg 18239 | 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 (base set of the) group is subgroup of the other group. (Contributed by AV, 14-Mar-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑆 = (Base‘𝐻) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) → ((𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) → 𝑆 ∈ (SubGrp‘𝐺))) | ||
Theorem | resgrpisgrp 18240 | 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 other group restricted to the base set of the group is a group. (Contributed by AV, 14-Mar-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑆 = (Base‘𝐻) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) → ((𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) → (𝐺 ↾s 𝑆) ∈ Grp)) | ||
Theorem | subgsubm 18241 | A subgroup is a submonoid. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ∈ (SubMnd‘𝐺)) | ||
Theorem | subsubg 18242 | A subgroup of a subgroup is a subgroup. (Contributed by Mario Carneiro, 19-Jan-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐴 ∈ (SubGrp‘𝐻) ↔ (𝐴 ∈ (SubGrp‘𝐺) ∧ 𝐴 ⊆ 𝑆))) | ||
Theorem | subgint 18243 | The intersection of a nonempty collection of subgroups is a subgroup. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ ((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ (SubGrp‘𝐺)) | ||
Theorem | 0subg 18244 | The zero subgroup of an arbitrary group. (Contributed by Stefan O'Rear, 10-Dec-2014.) |
⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → { 0 } ∈ (SubGrp‘𝐺)) | ||
Theorem | trivsubgd 18245 | The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 = { 0 }) & ⊢ (𝜑 → 𝐴 ∈ (SubGrp‘𝐺)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | trivsubgsnd 18246 | The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 = { 0 }) ⇒ ⊢ (𝜑 → (SubGrp‘𝐺) = {𝐵}) | ||
Theorem | isnsg 18247* | Property of being a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆))) | ||
Theorem | isnsg2 18248* | Weaken the condition of isnsg 18247 to only one side of the implication. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 → (𝑦 + 𝑥) ∈ 𝑆))) | ||
Theorem | nsgbi 18249 | Defining property of a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 + 𝐵) ∈ 𝑆 ↔ (𝐵 + 𝐴) ∈ 𝑆)) | ||
Theorem | nsgsubg 18250 | A normal subgroup is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝑆 ∈ (SubGrp‘𝐺)) | ||
Theorem | nsgconj 18251 | The conjugation of an element of a normal subgroup is in the subgroup. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑆) → ((𝐴 + 𝐵) − 𝐴) ∈ 𝑆) | ||
Theorem | isnsg3 18252* | A subgroup is normal iff the conjugation of all the elements of the subgroup is in the subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑆 ((𝑥 + 𝑦) − 𝑥) ∈ 𝑆)) | ||
Theorem | subgacs 18253 | Subgroups are an algebraic closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘𝐵)) | ||
Theorem | nsgacs 18254 | Normal subgroups form an algebraic closure system. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → (NrmSGrp‘𝐺) ∈ (ACS‘𝐵)) | ||
Theorem | elnmz 18255* | Elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)} ⇒ ⊢ (𝐴 ∈ 𝑁 ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑧 ∈ 𝑋 ((𝐴 + 𝑧) ∈ 𝑆 ↔ (𝑧 + 𝐴) ∈ 𝑆))) | ||
Theorem | nmzbi 18256* | Defining property of the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)} ⇒ ⊢ ((𝐴 ∈ 𝑁 ∧ 𝐵 ∈ 𝑋) → ((𝐴 + 𝐵) ∈ 𝑆 ↔ (𝐵 + 𝐴) ∈ 𝑆)) | ||
Theorem | nmzsubg 18257* | The normalizer NG(S) of a subset 𝑆 of the group is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)} & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝑁 ∈ (SubGrp‘𝐺)) | ||
Theorem | ssnmz 18258* | A subgroup is a subset of its normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)} & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝑁) | ||
Theorem | isnsg4 18259* | A subgroup is normal iff its normalizer is the entire group. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)} & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 = 𝑋)) | ||
Theorem | nmznsg 18260* | Any subgroup is a normal subgroup of its normalizer. (Contributed by Mario Carneiro, 19-Jan-2015.) |
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)} & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐻 = (𝐺 ↾s 𝑁) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ∈ (NrmSGrp‘𝐻)) | ||
Theorem | 0nsg 18261 | The zero subgroup is normal. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → { 0 } ∈ (NrmSGrp‘𝐺)) | ||
Theorem | nsgid 18262 | The whole group is a normal subgroup of itself. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝐵 ∈ (NrmSGrp‘𝐺)) | ||
Theorem | 0idnsgd 18263 | The whole group and the zero subgroup are normal subgroups of a group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) ⇒ ⊢ (𝜑 → {{ 0 }, 𝐵} ⊆ (NrmSGrp‘𝐺)) | ||
Theorem | trivnsgd 18264 | The only normal subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 = { 0 }) ⇒ ⊢ (𝜑 → (NrmSGrp‘𝐺) = {𝐵}) | ||
Theorem | triv1nsgd 18265 | A trivial group has exactly one normal subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 = { 0 }) ⇒ ⊢ (𝜑 → (NrmSGrp‘𝐺) ≈ 1o) | ||
Theorem | 1nsgtrivd 18266 | A group with exactly one normal subgroup is trivial. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → (NrmSGrp‘𝐺) ≈ 1o) ⇒ ⊢ (𝜑 → 𝐵 = { 0 }) | ||
Theorem | releqg 18267 | The left coset equivalence relation is a relation. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝑅 = (𝐺 ~QG 𝑆) ⇒ ⊢ Rel 𝑅 | ||
Theorem | eqgfval 18268* | Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑅 = (𝐺 ~QG 𝑆) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) → 𝑅 = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)}) | ||
Theorem | eqgval 18269 | Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015.) (Revised by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑅 = (𝐺 ~QG 𝑆) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) → (𝐴𝑅𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝑁‘𝐴) + 𝐵) ∈ 𝑆))) | ||
Theorem | eqger 18270 | The subgroup coset equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝑌) ⇒ ⊢ (𝑌 ∈ (SubGrp‘𝐺) → ∼ Er 𝑋) | ||
Theorem | eqglact 18271* | A left coset can be expressed as the image of a left action. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝑌) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((𝑥 ∈ 𝑋 ↦ (𝐴 + 𝑥)) “ 𝑌)) | ||
Theorem | eqgid 18272 | The left coset containing the identity is the original subgroup. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝑌) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝑌 ∈ (SubGrp‘𝐺) → [ 0 ] ∼ = 𝑌) | ||
Theorem | eqgen 18273 | Each coset is equipotent to the subgroup itself (which is also the coset containing the identity). (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝑌) ⇒ ⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ (𝑋 / ∼ )) → 𝑌 ≈ 𝐴) | ||
Theorem | eqgcpbl 18274 | The subgroup coset equivalence relation is compatible with addition when the subgroup is normal. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝑌) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝑌 ∈ (NrmSGrp‘𝐺) → ((𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷) → (𝐴 + 𝐵) ∼ (𝐶 + 𝐷))) | ||
Theorem | qusgrp 18275 | If 𝑌 is a normal subgroup of 𝐺, then 𝐻 = 𝐺 / 𝑌 is a group, called the quotient of 𝐺 by 𝑌. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆)) ⇒ ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝐻 ∈ Grp) | ||
Theorem | quseccl 18276 | Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆)) & ⊢ 𝑉 = (Base‘𝐺) & ⊢ 𝐵 = (Base‘𝐻) ⇒ ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑋 ∈ 𝑉) → [𝑋](𝐺 ~QG 𝑆) ∈ 𝐵) | ||
Theorem | qusadd 18277 | Value of the group operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆)) & ⊢ 𝑉 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ✚ = (+g‘𝐻) ⇒ ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ([𝑋](𝐺 ~QG 𝑆) ✚ [𝑌](𝐺 ~QG 𝑆)) = [(𝑋 + 𝑌)](𝐺 ~QG 𝑆)) | ||
Theorem | qus0 18278 | Value of the group identity operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆)) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → [ 0 ](𝐺 ~QG 𝑆) = (0g‘𝐻)) | ||
Theorem | qusinv 18279 | Value of the group inverse operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆)) & ⊢ 𝑉 = (Base‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ 𝑁 = (invg‘𝐻) ⇒ ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑋 ∈ 𝑉) → (𝑁‘[𝑋](𝐺 ~QG 𝑆)) = [(𝐼‘𝑋)](𝐺 ~QG 𝑆)) | ||
Theorem | qussub 18280 | Value of the group subtraction operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆)) & ⊢ 𝑉 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝑁 = (-g‘𝐻) ⇒ ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ([𝑋](𝐺 ~QG 𝑆)𝑁[𝑌](𝐺 ~QG 𝑆)) = [(𝑋 − 𝑌)](𝐺 ~QG 𝑆)) | ||
Theorem | lagsubg2 18281 | Lagrange's theorem for finite groups. Call the "order" of a group the cardinal number of the basic set of the group, and "index of a subgroup" the cardinal number of the set of left (or right, this is the same) cosets of this subgroup. Then the order of the group is the (cardinal) product of the order of any of its subgroups by the index of this subgroup. (Contributed by Mario Carneiro, 11-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝑌) & ⊢ (𝜑 → 𝑌 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → (♯‘𝑋) = ((♯‘(𝑋 / ∼ )) · (♯‘𝑌))) | ||
Theorem | lagsubg 18282 | Lagrange's theorem for Groups: the order of any subgroup of a finite group is a divisor of the order of the group. This is Metamath 100 proof #71. (Contributed by Mario Carneiro, 11-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin) → (♯‘𝑌) ∥ (♯‘𝑋)) | ||
This section contains some preliminary results about cyclic monoids and groups before the class CycGrp of cyclic groups (see df-cyg 18928) is defined in the context of Abelian groups. | ||
Theorem | cycsubmel 18283* | Characterization of an element of the set of nonnegative integer powers of an element 𝐴. Although this theorem holds for any class 𝐺, the definition of 𝐹 is only meaningful if 𝐺 is a monoid or at least a unital magma. (Contributed by AV, 28-Dec-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ ℕ0 ↦ (𝑥 · 𝐴)) & ⊢ 𝐶 = ran 𝐹 ⇒ ⊢ (𝑋 ∈ 𝐶 ↔ ∃𝑖 ∈ ℕ0 𝑋 = (𝑖 · 𝐴)) | ||
Theorem | cycsubmcl 18284* | The set of nonnegative integer powers of an element 𝐴 contains 𝐴. Although this theorem holds for any class 𝐺, the definition of 𝐹 is only meaningful if 𝐺 is a monoid or at least a unital magma. (Contributed by AV, 28-Dec-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ ℕ0 ↦ (𝑥 · 𝐴)) & ⊢ 𝐶 = ran 𝐹 ⇒ ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐶) | ||
Theorem | cycsubm 18285* | The set of nonnegative integer powers of an element 𝐴 of a monoid forms a submonoid containing 𝐴 (see cycsubmcl 18284), called the cyclic monoid generated by the element 𝐴. This corresponds to the statement in [Lang] p. 6. (Contributed by AV, 28-Dec-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ ℕ0 ↦ (𝑥 · 𝐴)) & ⊢ 𝐶 = ran 𝐹 ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → 𝐶 ∈ (SubMnd‘𝐺)) | ||
Theorem | cyccom 18286* | Condition for an operation to be commutative. Lemma for cycsubmcom 18287 and cygabl 18941. Formerly part of proof for cygabl 18941. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 20-Jan-2024.) |
⊢ (𝜑 → ∀𝑐 ∈ 𝐶 ∃𝑥 ∈ 𝑍 𝑐 = (𝑥 · 𝐴)) & ⊢ (𝜑 → ∀𝑚 ∈ 𝑍 ∀𝑛 ∈ 𝑍 ((𝑚 + 𝑛) · 𝐴) = ((𝑚 · 𝐴) + (𝑛 · 𝐴))) & ⊢ (𝜑 → 𝑋 ∈ 𝐶) & ⊢ (𝜑 → 𝑌 ∈ 𝐶) & ⊢ (𝜑 → 𝑍 ⊆ ℂ) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
Theorem | cycsubmcom 18287* | The operation of a monoid is commutative over the set of nonnegative integer powers of an element 𝐴 of the monoid. (Contributed by AV, 20-Jan-2024.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ ℕ0 ↦ (𝑥 · 𝐴)) & ⊢ 𝐶 = ran 𝐹 & ⊢ + = (+g‘𝐺) ⇒ ⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
Theorem | cycsubggend 18288* | The cyclic subgroup generated by 𝐴 includes its generator. Although this theorem holds for any class 𝐺, the definition of 𝐹 is only meaningful if 𝐺 is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 𝐴)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ ran 𝐹) | ||
Theorem | cycsubgcl 18289* | The set of integer powers of an element 𝐴 of a group forms a subgroup containing 𝐴, called the cyclic group generated by the element 𝐴. (Contributed by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (ran 𝐹 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ ran 𝐹)) | ||
Theorem | cycsubgss 18290* | The cyclic subgroup generated by an element 𝐴 is a subset of any subgroup containing 𝐴. (Contributed by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑆) → ran 𝐹 ⊆ 𝑆) | ||
Theorem | cycsubg 18291* | The cyclic group generated by 𝐴 is the smallest subgroup containing 𝐴. (Contributed by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ran 𝐹 = ∩ {𝑠 ∈ (SubGrp‘𝐺) ∣ 𝐴 ∈ 𝑠}) | ||
Theorem | cycsubgcld 18292* | The cyclic subgroup generated by 𝐴 is a subgroup. Deduction related to cycsubgcl 18289. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 𝐴)) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ran 𝐹 ∈ (SubGrp‘𝐺)) | ||
Theorem | cycsubg2 18293* | The subgroup generated by an element is exhausted by its multiples. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐾‘{𝐴}) = ran 𝐹) | ||
Theorem | cycsubg2cl 18294 | Any multiple of an element is contained in the generated cyclic subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ) → (𝑁 · 𝐴) ∈ (𝐾‘{𝐴})) | ||
Syntax | cghm 18295 | Extend class notation with the generator of group hom-sets. |
class GrpHom | ||
Definition | df-ghm 18296* | A homomorphism of groups is a map between two structures which preserves the group operation. Requiring both sides to be groups simplifies most theorems at the cost of complicating the theorem which pushes forward a group structure. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ GrpHom = (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑔 ∣ [(Base‘𝑠) / 𝑤](𝑔:𝑤⟶(Base‘𝑡) ∧ ∀𝑥 ∈ 𝑤 ∀𝑦 ∈ 𝑤 (𝑔‘(𝑥(+g‘𝑠)𝑦)) = ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦)))}) | ||
Theorem | reldmghm 18297 | Lemma for group homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ Rel dom GrpHom | ||
Theorem | isghm 18298* | Property of being a homomorphism of groups. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ 𝑋 = (Base‘𝑆) & ⊢ 𝑌 = (Base‘𝑇) & ⊢ + = (+g‘𝑆) & ⊢ ⨣ = (+g‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣))))) | ||
Theorem | isghm3 18299* | Property of a group homomorphism, similar to ismhm 17948. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝑋 = (Base‘𝑆) & ⊢ 𝑌 = (Base‘𝑇) & ⊢ + = (+g‘𝑆) & ⊢ ⨣ = (+g‘𝑇) ⇒ ⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣))))) | ||
Theorem | ghmgrp1 18300 | A group homomorphism is only defined when the domain is a group. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Grp) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |