![]() |
Metamath
Proof Explorer Theorem List (p. 194 of 491) | < 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: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | brgici 19301 | Prove isomorphic by an explicit isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝐹 ∈ (𝑅 GrpIso 𝑆) → 𝑅 ≃𝑔 𝑆) | ||
Theorem | gicref 19302 | Isomorphism is reflexive. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ (𝑅 ∈ Grp → 𝑅 ≃𝑔 𝑅) | ||
Theorem | giclcl 19303 | Isomorphism implies the left side is a group. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝑅 ≃𝑔 𝑆 → 𝑅 ∈ Grp) | ||
Theorem | gicrcl 19304 | Isomorphism implies the right side is a group. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ (𝑅 ≃𝑔 𝑆 → 𝑆 ∈ Grp) | ||
Theorem | gicsym 19305 | Isomorphism is symmetric. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ (𝑅 ≃𝑔 𝑆 → 𝑆 ≃𝑔 𝑅) | ||
Theorem | gictr 19306 | Isomorphism is transitive. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ ((𝑅 ≃𝑔 𝑆 ∧ 𝑆 ≃𝑔 𝑇) → 𝑅 ≃𝑔 𝑇) | ||
Theorem | gicer 19307 | Isomorphism is an equivalence relation on groups. (Contributed by Mario Carneiro, 21-Apr-2016.) (Proof shortened by AV, 1-May-2021.) |
⊢ ≃𝑔 Er Grp | ||
Theorem | gicen 19308 | Isomorphic groups have equinumerous base sets. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝑅 ≃𝑔 𝑆 → 𝐵 ≈ 𝐶) | ||
Theorem | gicsubgen 19309 | A less trivial example of a group invariant: cardinality of the subgroup lattice. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝑅 ≃𝑔 𝑆 → (SubGrp‘𝑅) ≈ (SubGrp‘𝑆)) | ||
Theorem | ghmqusnsglem1 19310* | Lemma for ghmqusnsg 19312. (Contributed by Thierry Arnoux, 13-May-2025.) |
⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞)) & ⊢ (𝜑 → 𝑁 ⊆ 𝐾) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐺)) ⇒ ⊢ (𝜑 → (𝐽‘[𝑋](𝐺 ~QG 𝑁)) = (𝐹‘𝑋)) | ||
Theorem | ghmqusnsglem2 19311* | Lemma for ghmqusnsg 19312. (Contributed by Thierry Arnoux, 13-May-2025.) |
⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞)) & ⊢ (𝜑 → 𝑁 ⊆ 𝐾) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝑄)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 (𝐽‘𝑌) = (𝐹‘𝑥)) | ||
Theorem | ghmqusnsg 19312* | The mapping 𝐻 induced by a surjective group homomorphism 𝐹 from the quotient group 𝑄 over a normal subgroup 𝑁 of 𝐹's kernel 𝐾 is a group isomorphism. In this case, one says that 𝐹 factors through 𝑄, which is also called the factor group. (Contributed by Thierry Arnoux, 13-May-2025.) |
⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞)) & ⊢ (𝜑 → 𝑁 ⊆ 𝐾) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) ⇒ ⊢ (𝜑 → 𝐽 ∈ (𝑄 GrpHom 𝐻)) | ||
Theorem | ghmquskerlem1 19313* | Lemma for ghmqusker 19317. (Contributed by Thierry Arnoux, 14-Feb-2025.) |
⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾)) & ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞)) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐺)) ⇒ ⊢ (𝜑 → (𝐽‘[𝑋](𝐺 ~QG 𝐾)) = (𝐹‘𝑋)) | ||
Theorem | ghmquskerco 19314* | In the case of theorem ghmqusker 19317, the composition of the natural homomorphism 𝐿 with the constructed homomorphism 𝐽 equals the original homomorphism 𝐹. One says that 𝐹 factors through 𝑄. (Proposed by Saveliy Skresanov, 15-Feb-2025.) (Contributed by Thierry Arnoux, 15-Feb-2025.) |
⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾)) & ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞)) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐿 = (𝑥 ∈ 𝐵 ↦ [𝑥](𝐺 ~QG 𝐾)) ⇒ ⊢ (𝜑 → 𝐹 = (𝐽 ∘ 𝐿)) | ||
Theorem | ghmquskerlem2 19315* | Lemma for ghmqusker 19317. (Contributed by Thierry Arnoux, 14-Feb-2025.) |
⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾)) & ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞)) & ⊢ (𝜑 → 𝑌 ∈ (Base‘𝑄)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 (𝐽‘𝑌) = (𝐹‘𝑥)) | ||
Theorem | ghmquskerlem3 19316* | The mapping 𝐻 induced by a surjective group homomorphism 𝐹 from the quotient group 𝑄 over 𝐹's kernel 𝐾 is a group isomorphism. In this case, one says that 𝐹 factors through 𝑄, which is also called the factor group. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾)) & ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞)) ⇒ ⊢ (𝜑 → 𝐽 ∈ (𝑄 GrpHom 𝐻)) | ||
Theorem | ghmqusker 19317* | A surjective group homomorphism 𝐹 from 𝐺 to 𝐻 induces an isomorphism 𝐽 from 𝑄 to 𝐻, where 𝑄 is the factor group of 𝐺 by 𝐹's kernel 𝐾. (Contributed by Thierry Arnoux, 15-Feb-2025.) |
⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾)) & ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞)) & ⊢ (𝜑 → ran 𝐹 = (Base‘𝐻)) ⇒ ⊢ (𝜑 → 𝐽 ∈ (𝑄 GrpIso 𝐻)) | ||
Theorem | gicqusker 19318 | The image 𝐻 of a group homomorphism 𝐹 is isomorphic with the quotient group 𝑄 over 𝐹's kernel 𝐾. Together with ghmker 19272 and ghmima 19267, this is sometimes called the first isomorphism theorem for groups. (Contributed by Thierry Arnoux, 10-Mar-2025.) |
⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾)) & ⊢ (𝜑 → ran 𝐹 = (Base‘𝐻)) ⇒ ⊢ (𝜑 → 𝑄 ≃𝑔 𝐻) | ||
Syntax | cga 19319 | Extend class definition to include the class of group actions. |
class GrpAct | ||
Definition | df-ga 19320* | Define the class of all group actions. A group 𝐺 acts on a set 𝑆 if a permutation on 𝑆 is associated with every element of 𝐺 in such a way that the identity permutation on 𝑆 is associated with the neutral element of 𝐺, and the composition of the permutations associated with two elements of 𝐺 is identical with the permutation associated with the composition of these two elements (in the same order) in the group 𝐺. (Contributed by Jeff Hankins, 10-Aug-2009.) |
⊢ GrpAct = (𝑔 ∈ Grp, 𝑠 ∈ V ↦ ⦋(Base‘𝑔) / 𝑏⦌{𝑚 ∈ (𝑠 ↑m (𝑏 × 𝑠)) ∣ ∀𝑥 ∈ 𝑠 (((0g‘𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))}) | ||
Theorem | isga 19321* | The predicate "is a (left) group action". The group 𝐺 is said to act on the base set 𝑌 of the action, which is not assumed to have any special properties. There is a related notion of right group action, but as the Wikipedia article explains, it is not mathematically interesting. The way actions are usually thought of is that each element 𝑔 of 𝐺 is a permutation of the elements of 𝑌 (see gapm 19336). Since group theory was classically about symmetry groups, it is therefore likely that the notion of group action was useful even in early group theory. (Contributed by Jeff Hankins, 10-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) ↔ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) ∧ ( ⊕ :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥)))))) | ||
Theorem | gagrp 19322 | The left argument of a group action is a group. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → 𝐺 ∈ Grp) | ||
Theorem | gaset 19323 | The right argument of a group action is a set. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → 𝑌 ∈ V) | ||
Theorem | gagrpid 19324 | The identity of the group does not alter the base set. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
⊢ 0 = (0g‘𝐺) ⇒ ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → ( 0 ⊕ 𝐴) = 𝐴) | ||
Theorem | gaf 19325 | The mapping of the group action operation. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → ⊕ :(𝑋 × 𝑌)⟶𝑌) | ||
Theorem | gafo 19326 | A group action is onto its base set. (Contributed by Jeff Hankins, 10-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → ⊕ :(𝑋 × 𝑌)–onto→𝑌) | ||
Theorem | gaass 19327 | An "associative" property for group actions. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌)) → ((𝐴 + 𝐵) ⊕ 𝐶) = (𝐴 ⊕ (𝐵 ⊕ 𝐶))) | ||
Theorem | ga0 19328 | The action of a group on the empty set. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
⊢ (𝐺 ∈ Grp → ∅ ∈ (𝐺 GrpAct ∅)) | ||
Theorem | gaid 19329 | The trivial action of a group on any set. Each group element corresponds to the identity permutation. (Contributed by Jeff Hankins, 11-Aug-2009.) (Proof shortened by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ∈ 𝑉) → (2nd ↾ (𝑋 × 𝑆)) ∈ (𝐺 GrpAct 𝑆)) | ||
Theorem | subgga 19330* | A subgroup acts on its parent group. (Contributed by Jeff Hankins, 13-Aug-2009.) (Proof shortened by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐻 = (𝐺 ↾s 𝑌) & ⊢ 𝐹 = (𝑥 ∈ 𝑌, 𝑦 ∈ 𝑋 ↦ (𝑥 + 𝑦)) ⇒ ⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝐹 ∈ (𝐻 GrpAct 𝑋)) | ||
Theorem | gass 19331* | A subset of a group action is a group action iff it is closed under the group action operation. (Contributed by Mario Carneiro, 17-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) → (( ⊕ ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍)) | ||
Theorem | gasubg 19332 | The restriction of a group action to a subgroup is a group action. (Contributed by Mario Carneiro, 17-Jan-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ( ⊕ ↾ (𝑆 × 𝑌)) ∈ (𝐻 GrpAct 𝑌)) | ||
Theorem | gaid2 19333* | A group operation is a left group action of the group on itself. (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥 + 𝑦)) ⇒ ⊢ (𝐺 ∈ Grp → 𝐹 ∈ (𝐺 GrpAct 𝑋)) | ||
Theorem | galcan 19334 | The action of a particular group element is left-cancelable. (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((𝐴 ⊕ 𝐵) = (𝐴 ⊕ 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | gacan 19335 | Group inverses cancel in a group action. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((𝐴 ⊕ 𝐵) = 𝐶 ↔ ((𝑁‘𝐴) ⊕ 𝐶) = 𝐵)) | ||
Theorem | gapm 19336* | The action of a particular group element is a permutation of the base set. (Contributed by Jeff Hankins, 11-Aug-2009.) (Proof shortened by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ 𝑌 ↦ (𝐴 ⊕ 𝑥)) ⇒ ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑋) → 𝐹:𝑌–1-1-onto→𝑌) | ||
Theorem | gaorb 19337* | The orbit equivalence relation puts two points in the group action in the same equivalence class iff there is a group element that takes one element to the other. (Contributed by Mario Carneiro, 14-Jan-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} ⇒ ⊢ (𝐴 ∼ 𝐵 ↔ (𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ∧ ∃ℎ ∈ 𝑋 (ℎ ⊕ 𝐴) = 𝐵)) | ||
Theorem | gaorber 19338* | The orbit equivalence relation is an equivalence relation on the target set of the group action. (Contributed by NM, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} & ⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → ∼ Er 𝑌) | ||
Theorem | gastacl 19339* | The stabilizer subgroup in a group action. (Contributed by Mario Carneiro, 15-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴} ⇒ ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐻 ∈ (SubGrp‘𝐺)) | ||
Theorem | gastacos 19340* | Write the coset relation for the stabilizer subgroup. (Contributed by Mario Carneiro, 15-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴} & ⊢ ∼ = (𝐺 ~QG 𝐻) ⇒ ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐵 ∼ 𝐶 ↔ (𝐵 ⊕ 𝐴) = (𝐶 ⊕ 𝐴))) | ||
Theorem | orbstafun 19341* | Existence and uniqueness for the function of orbsta 19343. (Contributed by Mario Carneiro, 15-Jan-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴} & ⊢ ∼ = (𝐺 ~QG 𝐻) & ⊢ 𝐹 = ran (𝑘 ∈ 𝑋 ↦ 〈[𝑘] ∼ , (𝑘 ⊕ 𝐴)〉) ⇒ ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → Fun 𝐹) | ||
Theorem | orbstaval 19342* | Value of the function at a given equivalence class element. (Contributed by Mario Carneiro, 15-Jan-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴} & ⊢ ∼ = (𝐺 ~QG 𝐻) & ⊢ 𝐹 = ran (𝑘 ∈ 𝑋 ↦ 〈[𝑘] ∼ , (𝑘 ⊕ 𝐴)〉) ⇒ ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝐵 ∈ 𝑋) → (𝐹‘[𝐵] ∼ ) = (𝐵 ⊕ 𝐴)) | ||
Theorem | orbsta 19343* | The Orbit-Stabilizer theorem. The mapping 𝐹 is a bijection from the cosets of the stabilizer subgroup of 𝐴 to the orbit of 𝐴. (Contributed by Mario Carneiro, 15-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴} & ⊢ ∼ = (𝐺 ~QG 𝐻) & ⊢ 𝐹 = ran (𝑘 ∈ 𝑋 ↦ 〈[𝑘] ∼ , (𝑘 ⊕ 𝐴)〉) & ⊢ 𝑂 = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} ⇒ ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐹:(𝑋 / ∼ )–1-1-onto→[𝐴]𝑂) | ||
Theorem | orbsta2 19344* | Relation between the size of the orbit and the size of the stabilizer of a point in a finite group action. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴} & ⊢ ∼ = (𝐺 ~QG 𝐻) & ⊢ 𝑂 = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} ⇒ ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑋 ∈ Fin) → (♯‘𝑋) = ((♯‘[𝐴]𝑂) · (♯‘𝐻))) | ||
Syntax | ccntz 19345 | Syntax for the centralizer of a set in a monoid. |
class Cntz | ||
Syntax | ccntr 19346 | Syntax for the centralizer of a monoid. |
class Cntr | ||
Definition | df-cntz 19347* | Define the centralizer of a subset of a magma, which is the set of elements each of which commutes with each element of the given subset. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ Cntz = (𝑚 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑚) ↦ {𝑥 ∈ (Base‘𝑚) ∣ ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝑚)𝑦) = (𝑦(+g‘𝑚)𝑥)})) | ||
Definition | df-cntr 19348 | Define the center of a magma, which is the elements that commute with all others. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ Cntr = (𝑚 ∈ V ↦ ((Cntz‘𝑚)‘(Base‘𝑚))) | ||
Theorem | cntrval 19349 | Substitute definition of the center. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ (𝑍‘𝐵) = (Cntr‘𝑀) | ||
Theorem | cntzfval 19350* | First level substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ (𝑀 ∈ 𝑉 → 𝑍 = (𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)})) | ||
Theorem | cntzval 19351* | Definition substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ (𝑆 ⊆ 𝐵 → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) | ||
Theorem | elcntz 19352* | Elementhood in the centralizer. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ (𝑆 ⊆ 𝐵 → (𝐴 ∈ (𝑍‘𝑆) ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝑆 (𝐴 + 𝑦) = (𝑦 + 𝐴)))) | ||
Theorem | cntzel 19353* | Membership in a centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑋 ∈ (𝑍‘𝑆) ↔ ∀𝑦 ∈ 𝑆 (𝑋 + 𝑦) = (𝑦 + 𝑋))) | ||
Theorem | cntzsnval 19354* | Special substitution for the centralizer of a singleton. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ (𝑌 ∈ 𝐵 → (𝑍‘{𝑌}) = {𝑥 ∈ 𝐵 ∣ (𝑥 + 𝑌) = (𝑌 + 𝑥)}) | ||
Theorem | elcntzsn 19355 | Value of the centralizer of a singleton. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ (𝑌 ∈ 𝐵 → (𝑋 ∈ (𝑍‘{𝑌}) ↔ (𝑋 ∈ 𝐵 ∧ (𝑋 + 𝑌) = (𝑌 + 𝑋)))) | ||
Theorem | sscntz 19356* | A centralizer expression for two sets elementwise commuting. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵) → (𝑆 ⊆ (𝑍‘𝑇) ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 (𝑥 + 𝑦) = (𝑦 + 𝑥))) | ||
Theorem | cntzrcl 19357 | Reverse closure for elements of the centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ (𝑋 ∈ (𝑍‘𝑆) → (𝑀 ∈ V ∧ 𝑆 ⊆ 𝐵)) | ||
Theorem | cntzssv 19358 | The centralizer is unconditionally a subset. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ (𝑍‘𝑆) ⊆ 𝐵 | ||
Theorem | cntzi 19359 | Membership in a centralizer (inference). (Contributed by Stefan O'Rear, 6-Sep-2015.) (Revised by Mario Carneiro, 22-Sep-2015.) |
⊢ + = (+g‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑋 ∈ (𝑍‘𝑆) ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
Theorem | elcntr 19360* | Elementhood in the center of a magma. (Contributed by SN, 21-Mar-2025.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝑍 = (Cntr‘𝑀) ⇒ ⊢ (𝐴 ∈ 𝑍 ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝐴 + 𝑦) = (𝑦 + 𝐴))) | ||
Theorem | cntrss 19361 | The center is a subset of the base field. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (Cntr‘𝑀) ⊆ 𝐵 | ||
Theorem | cntri 19362 | Defining property of the center of a group. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝑍 = (Cntr‘𝑀) ⇒ ⊢ ((𝑋 ∈ 𝑍 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
Theorem | resscntz 19363 | Centralizer in a substructure. (Contributed by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 𝑌 = (Cntz‘𝐻) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑌‘𝑆) = ((𝑍‘𝑆) ∩ 𝐴)) | ||
Theorem | cntzsgrpcl 19364* | Centralizers are closed under the semigroup operation. (Contributed by AV, 17-Feb-2025.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) & ⊢ 𝐶 = (𝑍‘𝑆) ⇒ ⊢ ((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) → ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐶 (𝑦(+g‘𝑀)𝑧) ∈ 𝐶) | ||
Theorem | cntz2ss 19365 | Centralizers reverse the subset relation. (Contributed by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝑆) → (𝑍‘𝑆) ⊆ (𝑍‘𝑇)) | ||
Theorem | cntzrec 19366 | Reciprocity relationship for centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵) → (𝑆 ⊆ (𝑍‘𝑇) ↔ 𝑇 ⊆ (𝑍‘𝑆))) | ||
Theorem | cntziinsn 19367* | Express any centralizer as an intersection of singleton centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ (𝑆 ⊆ 𝐵 → (𝑍‘𝑆) = (𝐵 ∩ ∩ 𝑥 ∈ 𝑆 (𝑍‘{𝑥}))) | ||
Theorem | cntzsubm 19368 | Centralizers in a monoid are submonoids. (Contributed by Stefan O'Rear, 6-Sep-2015.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubMnd‘𝑀)) | ||
Theorem | cntzsubg 19369 | Centralizers in a group are subgroups. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubGrp‘𝑀)) | ||
Theorem | cntzidss 19370 | If the elements of 𝑆 commute, the elements of a subset 𝑇 also commute. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ ((𝑆 ⊆ (𝑍‘𝑆) ∧ 𝑇 ⊆ 𝑆) → 𝑇 ⊆ (𝑍‘𝑇)) | ||
Theorem | cntzmhm 19371 | Centralizers in a monoid are preserved by monoid homomorphisms. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 𝑌 = (Cntz‘𝐻) ⇒ ⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) → (𝐹‘𝐴) ∈ (𝑌‘(𝐹 “ 𝑆))) | ||
Theorem | cntzmhm2 19372 | Centralizers in a monoid are preserved by monoid homomorphisms. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 𝑌 = (Cntz‘𝐻) ⇒ ⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑆 ⊆ (𝑍‘𝑇)) → (𝐹 “ 𝑆) ⊆ (𝑌‘(𝐹 “ 𝑇))) | ||
Theorem | cntrsubgnsg 19373 | A central subgroup is normal. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝑍 = (Cntr‘𝑀) ⇒ ⊢ ((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) → 𝑋 ∈ (NrmSGrp‘𝑀)) | ||
Theorem | cntrnsg 19374 | The center of a group is a normal subgroup. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝑍 = (Cntr‘𝑀) ⇒ ⊢ (𝑀 ∈ Grp → 𝑍 ∈ (NrmSGrp‘𝑀)) | ||
Syntax | coppg 19375 | The opposite group operation. |
class oppg | ||
Definition | df-oppg 19376 | Define an opposite group, which is the same as the original group but with addition written the other way around. df-oppr 20350 does the same thing for multiplication. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
⊢ oppg = (𝑤 ∈ V ↦ (𝑤 sSet 〈(+g‘ndx), tpos (+g‘𝑤)〉)) | ||
Theorem | oppgval 19377 | Value of the opposite group. (Contributed by Stefan O'Rear, 25-Aug-2015.) (Revised by Mario Carneiro, 16-Sep-2015.) (Revised by Fan Zheng, 26-Jun-2016.) |
⊢ + = (+g‘𝑅) & ⊢ 𝑂 = (oppg‘𝑅) ⇒ ⊢ 𝑂 = (𝑅 sSet 〈(+g‘ndx), tpos + 〉) | ||
Theorem | oppgplusfval 19378 | Value of the addition operation of an opposite group. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Fan Zheng, 26-Jun-2016.) |
⊢ + = (+g‘𝑅) & ⊢ 𝑂 = (oppg‘𝑅) & ⊢ ✚ = (+g‘𝑂) ⇒ ⊢ ✚ = tpos + | ||
Theorem | oppgplus 19379 | Value of the addition operation of an opposite ring. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Fan Zheng, 26-Jun-2016.) |
⊢ + = (+g‘𝑅) & ⊢ 𝑂 = (oppg‘𝑅) & ⊢ ✚ = (+g‘𝑂) ⇒ ⊢ (𝑋 ✚ 𝑌) = (𝑌 + 𝑋) | ||
Theorem | setsplusg 19380 | The other components of an extensible structure remain unchanged if the +g component is set/substituted. (Contributed by Stefan O'Rear, 26-Aug-2015.) Generalisation of the former oppglem and mgplem. (Revised by AV, 18-Oct-2024.) |
⊢ 𝑂 = (𝑅 sSet 〈(+g‘ndx), 𝑆〉) & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝐸‘ndx) ≠ (+g‘ndx) ⇒ ⊢ (𝐸‘𝑅) = (𝐸‘𝑂) | ||
Theorem | oppglemOLD 19381 | Obsolete version of setsplusg 19380 as of 18-Oct-2024. Lemma for oppgbas 19382. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 ≠ 2 ⇒ ⊢ (𝐸‘𝑅) = (𝐸‘𝑂) | ||
Theorem | oppgbas 19382 | Base set of an opposite group. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ 𝐵 = (Base‘𝑂) | ||
Theorem | oppgbasOLD 19383 | Obsolete version of oppgbas 19382 as of 18-Oct-2024. Base set of an opposite group. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ 𝐵 = (Base‘𝑂) | ||
Theorem | oppgtset 19384 | Topology of an opposite group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ 𝐽 = (TopSet‘𝑅) ⇒ ⊢ 𝐽 = (TopSet‘𝑂) | ||
Theorem | oppgtsetOLD 19385 | Obsolete version of oppgtset 19384 as of 18-Oct-2024. Topology of an opposite group. (Contributed by Mario Carneiro, 17-Sep-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ 𝐽 = (TopSet‘𝑅) ⇒ ⊢ 𝐽 = (TopSet‘𝑂) | ||
Theorem | oppgtopn 19386 | Topology of an opposite group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑅) ⇒ ⊢ 𝐽 = (TopOpen‘𝑂) | ||
Theorem | oppgmnd 19387 | The opposite of a monoid is a monoid. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Mario Carneiro, 16-Sep-2015.) |
⊢ 𝑂 = (oppg‘𝑅) ⇒ ⊢ (𝑅 ∈ Mnd → 𝑂 ∈ Mnd) | ||
Theorem | oppgmndb 19388 | Bidirectional form of oppgmnd 19387. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝑅) ⇒ ⊢ (𝑅 ∈ Mnd ↔ 𝑂 ∈ Mnd) | ||
Theorem | oppgid 19389 | Zero in a monoid is a symmetric notion. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Mario Carneiro, 16-Sep-2015.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ 0 = (0g‘𝑂) | ||
Theorem | oppggrp 19390 | The opposite of a group is a group. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝑅) ⇒ ⊢ (𝑅 ∈ Grp → 𝑂 ∈ Grp) | ||
Theorem | oppggrpb 19391 | Bidirectional form of oppggrp 19390. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝑅) ⇒ ⊢ (𝑅 ∈ Grp ↔ 𝑂 ∈ Grp) | ||
Theorem | oppginv 19392 | Inverses in a group are a symmetric notion. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) ⇒ ⊢ (𝑅 ∈ Grp → 𝐼 = (invg‘𝑂)) | ||
Theorem | invoppggim 19393 | The inverse is an antiautomorphism on any group. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝐼 ∈ (𝐺 GrpIso 𝑂)) | ||
Theorem | oppggic 19394 | Every group is (naturally) isomorphic to its opposite. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝐺 ≃𝑔 𝑂) | ||
Theorem | oppgsubm 19395 | Being a submonoid is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝑂 = (oppg‘𝐺) ⇒ ⊢ (SubMnd‘𝐺) = (SubMnd‘𝑂) | ||
Theorem | oppgsubg 19396 | Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝑂 = (oppg‘𝐺) ⇒ ⊢ (SubGrp‘𝐺) = (SubGrp‘𝑂) | ||
Theorem | oppgcntz 19397 | A centralizer in a group is the same as the centralizer in the opposite group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝑂 = (oppg‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝑍‘𝐴) = ((Cntz‘𝑂)‘𝐴) | ||
Theorem | oppgcntr 19398 | The center of a group is the same as the center of the opposite group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝑂 = (oppg‘𝐺) & ⊢ 𝑍 = (Cntr‘𝐺) ⇒ ⊢ 𝑍 = (Cntr‘𝑂) | ||
Theorem | gsumwrev 19399 | A sum in an opposite monoid is the regular sum of a reversed word. (Contributed by Stefan O'Rear, 27-Aug-2015.) (Proof shortened by Mario Carneiro, 28-Feb-2016.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑂 = (oppg‘𝑀) ⇒ ⊢ ((𝑀 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵) → (𝑂 Σg 𝑊) = (𝑀 Σg (reverse‘𝑊))) | ||
According to Wikipedia ("Symmetric group", 09-Mar-2019,
https://en.wikipedia.org/wiki/symmetric_group) "In abstract algebra, the
symmetric group defined over any set is the group whose elements are all the
bijections from the set to itself, and whose group operation is the composition
of functions." and according to Encyclopedia of Mathematics ("Symmetric group",
09-Mar-2019, https://www.encyclopediaofmath.org/index.php/Symmetric_group)
"The group of all permutations (self-bijections) of a set with the operation of
composition (see Permutation group).". In [Rotman] p. 27 "If X is a nonempty
set, a permutation of X is a function a : X -> X that is a one-to-one
correspondence." and "If X is a nonempty set, the symmetric group on X, denoted
SX, is the group whose elements are the permutations of X and whose
binary operation is composition of functions.". Therefore, we define the
symmetric group on a set 𝐴 as the set of one-to-one onto functions
from 𝐴 to itself under function composition, see df-symg 19401. However, the
set is allowed to be empty, see symgbas0 19420. Hint: The symmetric groups
should not be confused with "symmetry groups" which is a different topic in
group theory.
| ||
Syntax | csymg 19400 | Extend class notation to include the class of symmetric groups. |
class SymGrp |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |