HomeTheorem List (p. 194 of 510)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 194 of 510) | < 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-31502) |
Hilbert Space Explorer
(31503-33025) |
Users' Mathboxes
(33026-50934) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | mulgass 19301 | Product of group multiples, generalized to ℤ. (Contributed by Mario Carneiro, 13-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) | ||
| Theorem | mulgassr 19302 | Reversed product of group multiples. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑁 · 𝑀) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) | ||
| Theorem | mulgmodid 19303 | 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 19304 | Distribution of group multiples over subtraction for group elements, subdir 11731 analog. (Contributed by Mario Carneiro, 13-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 − 𝑁) · 𝑋) = ((𝑀 · 𝑋) − (𝑁 · 𝑋))) | ||
| Theorem | mhmmulg 19305 | A homomorphism of monoids preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ × = (.g‘𝐻) ⇒ ⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑁 · 𝑋)) = (𝑁 × (𝐹‘𝑋))) | ||
| Theorem | mulgpropd 19306* | 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 19307 | Closure of the group multiple (exponentiation) operation in a submonoid. (Contributed by Mario Carneiro, 13-Jan-2015.) |
| ⊢ ∙ = (.g‘𝐺) ⇒ ⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆) → (𝑁 ∙ 𝑋) ∈ 𝑆) | ||
| Theorem | submmulg 19308 | 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 19309 | Value of a group multiple in a structure power. (Contributed by Mario Carneiro, 15-Jun-2015.) |
| ⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ ∙ = (.g‘𝑌) & ⊢ · = (.g‘𝑅) ⇒ ⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉) ∧ (𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼)) → ((𝑁 ∙ 𝑋)‘𝐴) = (𝑁 · (𝑋‘𝐴))) | ||
| Syntax | csubg 19310 | Extend class notation with all subgroups of a group. |
| class SubGrp | ||
| Syntax | cnsg 19311 | Extend class notation with all normal subgroups of a group. |
| class NrmSGrp | ||
| Syntax | cqg 19312 | Quotient group equivalence class. |
| class ~QG | ||
| Definition | df-subg 19313* | Define a subgroup of a group as a set of elements that is a group in its own right. Equivalently (issubg2 19332), a subgroup is a subset of the group that is closed for the group internal operation (see subgcl 19326), contains the neutral element of the group (see subg0 19322) and contains the inverses for all of its elements (see subginvcl 19325). (Contributed by Mario Carneiro, 2-Dec-2014.) |
| ⊢ SubGrp = (𝑤 ∈ Grp ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Grp}) | ||
| Definition | df-nsg 19314* | 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 19315* | 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 19316 | The subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)) | ||
| Theorem | subgss 19317 | A subgroup is a subset. (Contributed by Mario Carneiro, 2-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝐵) | ||
| Theorem | subgid 19318 | A group is a subgroup of itself. (Contributed by Mario Carneiro, 7-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝐵 ∈ (SubGrp‘𝐺)) | ||
| Theorem | subggrp 19319 | A subgroup is a group. (Contributed by Mario Carneiro, 2-Dec-2014.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp) | ||
| Theorem | subgbas 19320 | The base of the restricted group in a subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 = (Base‘𝐻)) | ||
| Theorem | subgrcl 19321 | Reverse closure for the subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.) |
| ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) | ||
| Theorem | subg0 19322 | 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 19323 | 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 19324 | The group identity is an element of any subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.) |
| ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑆) | ||
| Theorem | subginvcl 19325 | The inverse of an element is closed in a subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.) |
| ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝑆) → (𝐼‘𝑋) ∈ 𝑆) | ||
| Theorem | subgcl 19326 | A subgroup is closed under group operation. (Contributed by Mario Carneiro, 2-Dec-2014.) |
| ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) ∈ 𝑆) | ||
| Theorem | subgcld 19327 | A subgroup is closed under group operation. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝑆) | ||
| Theorem | subgsubcl 19328 | A subgroup is closed under group subtraction. (Contributed by Mario Carneiro, 18-Jan-2015.) |
| ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 − 𝑌) ∈ 𝑆) | ||
| Theorem | subgsub 19329 | 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 19330 | Closure of the group multiple (exponentiation) operation in a subgroup. (Contributed by Mario Carneiro, 13-Jan-2015.) |
| ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) ∈ 𝑆) | ||
| Theorem | subgmulg 19331 | A group multiple is the same if evaluated in a subgroup. (Contributed by Mario Carneiro, 15-Jan-2015.) |
| ⊢ · = (.g‘𝐺) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) & ⊢ ∙ = (.g‘𝐻) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) = (𝑁 ∙ 𝑋)) | ||
| Theorem | issubg2 19332* | Characterize the subgroups of a group by closure properties. (Contributed by Mario Carneiro, 2-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)))) | ||
| Theorem | issubgrpd2 19333* | 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 19334* | Prove a subgroup by closure. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
| ⊢ (𝜑 → 𝑆 = (𝐼 ↾s 𝐷)) & ⊢ (𝜑 → 0 = (0g‘𝐼)) & ⊢ (𝜑 → + = (+g‘𝐼)) & ⊢ (𝜑 → 𝐷 ⊆ (Base‘𝐼)) & ⊢ (𝜑 → 0 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 + 𝑦) ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((invg‘𝐼)‘𝑥) ∈ 𝐷) & ⊢ (𝜑 → 𝐼 ∈ Grp) ⇒ ⊢ (𝜑 → 𝑆 ∈ Grp) | ||
| Theorem | issubg3 19335* | A subgroup is a symmetric submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.) |
| ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ∈ (SubMnd‘𝐺) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆))) | ||
| Theorem | issubg4 19336* | 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 19337 | 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 19338 | 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 19339 | A subgroup is a submonoid. (Contributed by Mario Carneiro, 18-Jun-2015.) |
| ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ∈ (SubMnd‘𝐺)) | ||
| Theorem | subsubg 19340 | A subgroup of a subgroup is a subgroup. (Contributed by Mario Carneiro, 19-Jan-2015.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐴 ∈ (SubGrp‘𝐻) ↔ (𝐴 ∈ (SubGrp‘𝐺) ∧ 𝐴 ⊆ 𝑆))) | ||
| Theorem | subgint 19341 | The intersection of a nonempty collection of subgroups is a subgroup. (Contributed by Mario Carneiro, 7-Dec-2014.) |
| ⊢ ((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ (SubGrp‘𝐺)) | ||
| Theorem | 0subg 19342 | The zero subgroup of an arbitrary group. (Contributed by Stefan O'Rear, 10-Dec-2014.) (Proof shortened by SN, 31-Jan-2025.) |
| ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → { 0 } ∈ (SubGrp‘𝐺)) | ||
| Theorem | trivsubgd 19343 | The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 = { 0 }) & ⊢ (𝜑 → 𝐴 ∈ (SubGrp‘𝐺)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
| Theorem | trivsubgsnd 19344 | The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 = { 0 }) ⇒ ⊢ (𝜑 → (SubGrp‘𝐺) = {𝐵}) | ||
| Theorem | isnsg 19345* | Property of being a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆))) | ||
| Theorem | isnsg2 19346* | Weaken the condition of isnsg 19345 to only one side of the implication. (Contributed by Mario Carneiro, 18-Jan-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 → (𝑦 + 𝑥) ∈ 𝑆))) | ||
| Theorem | nsgbi 19347 | Defining property of a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 + 𝐵) ∈ 𝑆 ↔ (𝐵 + 𝐴) ∈ 𝑆)) | ||
| Theorem | nsgsubg 19348 | A normal subgroup is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
| ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝑆 ∈ (SubGrp‘𝐺)) | ||
| Theorem | nsgconj 19349 | 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 19350* | 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 19351 | 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 19352 | Normal subgroups form an algebraic closure system. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → (NrmSGrp‘𝐺) ∈ (ACS‘𝐵)) | ||
| Theorem | elnmz 19353* | Elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
| ⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)} ⇒ ⊢ (𝐴 ∈ 𝑁 ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑧 ∈ 𝑋 ((𝐴 + 𝑧) ∈ 𝑆 ↔ (𝑧 + 𝐴) ∈ 𝑆))) | ||
| Theorem | nmzbi 19354* | Defining property of the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
| ⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)} ⇒ ⊢ ((𝐴 ∈ 𝑁 ∧ 𝐵 ∈ 𝑋) → ((𝐴 + 𝐵) ∈ 𝑆 ↔ (𝐵 + 𝐴) ∈ 𝑆)) | ||
| Theorem | nmzsubg 19355* | 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 19356* | A subgroup is a subset of its normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
| ⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)} & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝑁) | ||
| Theorem | isnsg4 19357* | A subgroup is normal iff its normalizer is the entire group. (Contributed by Mario Carneiro, 18-Jan-2015.) |
| ⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)} & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 = 𝑋)) | ||
| Theorem | nmznsg 19358* | Any subgroup is a normal subgroup of its normalizer. (Contributed by Mario Carneiro, 19-Jan-2015.) |
| ⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)} & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐻 = (𝐺 ↾s 𝑁) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ∈ (NrmSGrp‘𝐻)) | ||
| Theorem | 0nsg 19359 | The zero subgroup is normal. (Contributed by Mario Carneiro, 4-Feb-2015.) |
| ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → { 0 } ∈ (NrmSGrp‘𝐺)) | ||
| Theorem | nsgid 19360 | The whole group is a normal subgroup of itself. (Contributed by Mario Carneiro, 4-Feb-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝐵 ∈ (NrmSGrp‘𝐺)) | ||
| Theorem | 0idnsgd 19361 | 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 19362 | 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 19363 | A trivial group has exactly one normal subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 = { 0 }) ⇒ ⊢ (𝜑 → (NrmSGrp‘𝐺) ≈ 1o) | ||
| Theorem | 1nsgtrivd 19364 | 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 19365 | The left coset equivalence relation is a relation. (Contributed by Mario Carneiro, 14-Jun-2015.) |
| ⊢ 𝑅 = (𝐺 ~QG 𝑆) ⇒ ⊢ Rel 𝑅 | ||
| Theorem | ecxpid 19366 | The equivalence class of a cartesian product is the whole set. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
| ⊢ (𝑋 ∈ 𝐴 → [𝑋](𝐴 × 𝐴) = 𝐴) | ||
| Theorem | qsxpid 19367 | The quotient set of a cartesian product is trivial. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
| ⊢ (𝐴 ≠ ∅ → (𝐴 / (𝐴 × 𝐴)) = {𝐴}) | ||
| Theorem | eqgfval 19368* | Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑅 = (𝐺 ~QG 𝑆) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) → 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)}) | ||
| Theorem | eqgval 19369 | 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 19370 | The subgroup coset equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 13-Jan-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝑌) ⇒ ⊢ (𝑌 ∈ (SubGrp‘𝐺) → ∼ Er 𝑋) | ||
| Theorem | eqglact 19371* | 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 19372 | 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 19373 | 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 19374 | 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 | qusxpid 19375 | The Group quotient equivalence relation for the whole group is the cartesian product, i.e. all elements are in the same equivalence class. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → (𝐺 ~QG 𝐵) = (𝐵 × 𝐵)) | ||
| Theorem | qustriv 19376 | The quotient of a group 𝐺 by itself is trivial. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐵)) ⇒ ⊢ (𝐺 ∈ Grp → (Base‘𝑄) = {𝐵}) | ||
| Theorem | qustrivr 19377 | Converse of qustriv 19376. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐻)) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐻 ∈ (SubGrp‘𝐺) ∧ (Base‘𝑄) = {𝐻}) → 𝐻 = 𝐵) | ||
| Theorem | eqg0el 19378 | Equivalence class of a quotient group for a subgroup. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
| ⊢ ∼ = (𝐺 ~QG 𝐻) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐻 ∈ (SubGrp‘𝐺)) → ([𝑋] ∼ = 𝐻 ↔ 𝑋 ∈ 𝐻)) | ||
| Theorem | quselbas 19379* | Membership in the base set of a quotient group. (Contributed by AV, 1-Mar-2025.) |
| ⊢ ∼ = (𝐺 ~QG 𝑆) & ⊢ 𝑈 = (𝐺 /s ∼ ) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → (𝑋 ∈ (Base‘𝑈) ↔ ∃𝑥 ∈ 𝐵 𝑋 = [𝑥] ∼ )) | ||
| Theorem | quseccl0 19380 | Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) Generalization of quseccl 19382 for arbitrary sets 𝐺. (Revised by AV, 24-Feb-2025.) |
| ⊢ ∼ = (𝐺 ~QG 𝑆) & ⊢ 𝐻 = (𝐺 /s ∼ ) & ⊢ 𝐶 = (Base‘𝐺) & ⊢ 𝐵 = (Base‘𝐻) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶) → [𝑋] ∼ ∈ 𝐵) | ||
| Theorem | qusgrp 19381 | 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 19382 | Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) (Proof shortened by AV, 9-Mar-2025.) |
| ⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆)) & ⊢ 𝑉 = (Base‘𝐺) & ⊢ 𝐵 = (Base‘𝐻) ⇒ ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑋 ∈ 𝑉) → [𝑋](𝐺 ~QG 𝑆) ∈ 𝐵) | ||
| Theorem | qusadd 19383 | 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 19384 | 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 19385 | 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 19386 | 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 | ecqusaddd 19387 | Addition of equivalence classes in a quotient group. (Contributed by AV, 25-Feb-2025.) |
| ⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅)) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∼ = (𝑅 ~QG 𝐼) & ⊢ 𝑄 = (𝑅 /s ∼ ) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵)) → [(𝐴(+g‘𝑅)𝐶)] ∼ = ([𝐴] ∼ (+g‘𝑄)[𝐶] ∼ )) | ||
| Theorem | ecqusaddcl 19388 | Closure of the addition in a quotient group. (Contributed by AV, 24-Feb-2025.) |
| ⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅)) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ ∼ = (𝑅 ~QG 𝐼) & ⊢ 𝑄 = (𝑅 /s ∼ ) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵)) → ([𝐴] ∼ (+g‘𝑄)[𝐶] ∼ ) ∈ (Base‘𝑄)) | ||
| Theorem | lagsubg2 19389 | 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 19390 | 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) → (♯‘𝑌) ∥ (♯‘𝑋)) | ||
| Theorem | eqg0subg 19391 | The coset equivalence relation for the trivial (zero) subgroup of a group is the identity relation restricted to the base set of the group. (Contributed by AV, 25-Feb-2025.) |
| ⊢ 0 = (0g‘𝐺) & ⊢ 𝑆 = { 0 } & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑅 = (𝐺 ~QG 𝑆) ⇒ ⊢ (𝐺 ∈ Grp → 𝑅 = ( I ↾ 𝐵)) | ||
| Theorem | eqg0subgecsn 19392 | The equivalence classes modulo the coset equivalence relation for the trivial (zero) subgroup of a group are singletons. (Contributed by AV, 26-Feb-2025.) |
| ⊢ 0 = (0g‘𝐺) & ⊢ 𝑆 = { 0 } & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑅 = (𝐺 ~QG 𝑆) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → [𝑋]𝑅 = {𝑋}) | ||
| Theorem | qus0subgbas 19393* | The base set of a quotient of a group by the trivial (zero) subgroup. (Contributed by AV, 26-Feb-2025.) |
| ⊢ 0 = (0g‘𝐺) & ⊢ 𝑆 = { 0 } & ⊢ ∼ = (𝐺 ~QG 𝑆) & ⊢ 𝑈 = (𝐺 /s ∼ ) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → (Base‘𝑈) = {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}}) | ||
| Theorem | qus0subgadd 19394* | The addition in a quotient of a group by the trivial (zero) subgroup. (Contributed by AV, 26-Feb-2025.) |
| ⊢ 0 = (0g‘𝐺) & ⊢ 𝑆 = { 0 } & ⊢ ∼ = (𝐺 ~QG 𝑆) & ⊢ 𝑈 = (𝐺 /s ∼ ) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ({𝑎} (+g‘𝑈){𝑏}) = {(𝑎(+g‘𝐺)𝑏)}) | ||
This section contains some preliminary results about cyclic monoids and groups before the class CycGrp of cyclic groups (see df-cyg 20072) is defined in the context of Abelian groups. | ||
| Theorem | cycsubmel 19395* | 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 19396* | 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 19397* | The set of nonnegative integer powers of an element 𝐴 of a monoid forms a submonoid containing 𝐴 (see cycsubmcl 19396), 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 19398* | Condition for an operation to be commutative. Lemma for cycsubmcom 19399 and cygabl 20085. Formerly part of proof for cygabl 20085. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 20-Jan-2024.) |
| ⊢ (𝜑 → ∀𝑐 ∈ 𝐶 ∃𝑥 ∈ 𝑍 𝑐 = (𝑥 · 𝐴)) & ⊢ (𝜑 → ∀𝑚 ∈ 𝑍 ∀𝑛 ∈ 𝑍 ((𝑚 + 𝑛) · 𝐴) = ((𝑚 · 𝐴) + (𝑛 · 𝐴))) & ⊢ (𝜑 → 𝑋 ∈ 𝐶) & ⊢ (𝜑 → 𝑌 ∈ 𝐶) & ⊢ (𝜑 → 𝑍 ⊆ ℂ) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
| Theorem | cycsubmcom 19399* | 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 19400* | 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 𝐹) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |