Home | Metamath
Proof Explorer Theorem List (p. 185 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | gimfn 18401 | The group isomorphism function is a well-defined function. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ GrpIso Fn (Grp × Grp) | ||
Theorem | isgim 18402 | An isomorphism of groups is a bijective homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 GrpIso 𝑆) ↔ (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶)) | ||
Theorem | gimf1o 18403 | An isomorphism of groups is a bijection. (Contributed by Stefan O'Rear, 21-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 GrpIso 𝑆) → 𝐹:𝐵–1-1-onto→𝐶) | ||
Theorem | gimghm 18404 | An isomorphism of groups is a homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ (𝐹 ∈ (𝑅 GrpIso 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) | ||
Theorem | isgim2 18405 | A group isomorphism is a homomorphism whose converse is also a homomorphism. Characterization of isomorphisms similar to ishmeo 22367. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ (𝐹 ∈ (𝑅 GrpIso 𝑆) ↔ (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 GrpHom 𝑅))) | ||
Theorem | subggim 18406 | Behavior of subgroups under isomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝐹 ∈ (𝑅 GrpIso 𝑆) ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝐹 “ 𝐴) ∈ (SubGrp‘𝑆))) | ||
Theorem | gimcnv 18407 | The converse of a bijective group homomorphism is a bijective group homomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ (𝐹 ∈ (𝑆 GrpIso 𝑇) → ◡𝐹 ∈ (𝑇 GrpIso 𝑆)) | ||
Theorem | gimco 18408 | The composition of group isomorphisms is a group isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ ((𝐹 ∈ (𝑇 GrpIso 𝑈) ∧ 𝐺 ∈ (𝑆 GrpIso 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 GrpIso 𝑈)) | ||
Theorem | brgic 18409 | The relation "is isomorphic to" for groups. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝑅 ≃𝑔 𝑆 ↔ (𝑅 GrpIso 𝑆) ≠ ∅) | ||
Theorem | brgici 18410 | Prove isomorphic by an explicit isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝐹 ∈ (𝑅 GrpIso 𝑆) → 𝑅 ≃𝑔 𝑆) | ||
Theorem | gicref 18411 | Isomorphism is reflexive. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ (𝑅 ∈ Grp → 𝑅 ≃𝑔 𝑅) | ||
Theorem | giclcl 18412 | Isomorphism implies the left side is a group. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝑅 ≃𝑔 𝑆 → 𝑅 ∈ Grp) | ||
Theorem | gicrcl 18413 | Isomorphism implies the right side is a group. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ (𝑅 ≃𝑔 𝑆 → 𝑆 ∈ Grp) | ||
Theorem | gicsym 18414 | Isomorphism is symmetric. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ (𝑅 ≃𝑔 𝑆 → 𝑆 ≃𝑔 𝑅) | ||
Theorem | gictr 18415 | Isomorphism is transitive. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ ((𝑅 ≃𝑔 𝑆 ∧ 𝑆 ≃𝑔 𝑇) → 𝑅 ≃𝑔 𝑇) | ||
Theorem | gicer 18416 | 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 18417 | Isomorphic groups have equinumerous base sets. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝑅 ≃𝑔 𝑆 → 𝐵 ≈ 𝐶) | ||
Theorem | gicsubgen 18418 | A less trivial example of a group invariant: cardinality of the subgroup lattice. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝑅 ≃𝑔 𝑆 → (SubGrp‘𝑅) ≈ (SubGrp‘𝑆)) | ||
Syntax | cga 18419 | Extend class definition to include the class of group actions. |
class GrpAct | ||
Definition | df-ga 18420* | 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 18421* | 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 18436). 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 18422 | 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 18423 | The right argument of a group action is a set. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → 𝑌 ∈ V) | ||
Theorem | gagrpid 18424 | 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 18425 | 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 18426 | 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 18427 | 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 18428 | 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 18429 | 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 18430* | 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 18431* | 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 18432 | 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 18433* | 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 18434 | 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 18435 | 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 18436* | 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 18437* | 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 18438* | 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 18439* | The stabilizer subgroup in a group action. (Contributed by Mario Carneiro, 15-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴} ⇒ ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐻 ∈ (SubGrp‘𝐺)) | ||
Theorem | gastacos 18440* | Write the coset relation for the stabilizer subgroup. (Contributed by Mario Carneiro, 15-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴} & ⊢ ∼ = (𝐺 ~QG 𝐻) ⇒ ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐵 ∼ 𝐶 ↔ (𝐵 ⊕ 𝐴) = (𝐶 ⊕ 𝐴))) | ||
Theorem | orbstafun 18441* | Existence and uniqueness for the function of orbsta 18443. (Contributed by Mario Carneiro, 15-Jan-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴} & ⊢ ∼ = (𝐺 ~QG 𝐻) & ⊢ 𝐹 = ran (𝑘 ∈ 𝑋 ↦ 〈[𝑘] ∼ , (𝑘 ⊕ 𝐴)〉) ⇒ ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → Fun 𝐹) | ||
Theorem | orbstaval 18442* | 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 18443* | 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 18444* | 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 18445 | Syntax for the centralizer of a set in a monoid. |
class Cntz | ||
Syntax | ccntr 18446 | Syntax for the centralizer of a monoid. |
class Cntr | ||
Definition | df-cntz 18447* | 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 18448 | 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 18449 | Substitute definition of the center. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ (𝑍‘𝐵) = (Cntr‘𝑀) | ||
Theorem | cntzfval 18450* | First level substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ (𝑀 ∈ 𝑉 → 𝑍 = (𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)})) | ||
Theorem | cntzval 18451* | Definition substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ (𝑆 ⊆ 𝐵 → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)}) | ||
Theorem | elcntz 18452* | Elementhood in the centralizer. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ (𝑆 ⊆ 𝐵 → (𝐴 ∈ (𝑍‘𝑆) ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝑆 (𝐴 + 𝑦) = (𝑦 + 𝐴)))) | ||
Theorem | cntzel 18453* | Membership in a centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑋 ∈ (𝑍‘𝑆) ↔ ∀𝑦 ∈ 𝑆 (𝑋 + 𝑦) = (𝑦 + 𝑋))) | ||
Theorem | cntzsnval 18454* | Special substitution for the centralizer of a singleton. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ (𝑌 ∈ 𝐵 → (𝑍‘{𝑌}) = {𝑥 ∈ 𝐵 ∣ (𝑥 + 𝑌) = (𝑌 + 𝑥)}) | ||
Theorem | elcntzsn 18455 | Value of the centralizer of a singleton. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ (𝑌 ∈ 𝐵 → (𝑋 ∈ (𝑍‘{𝑌}) ↔ (𝑋 ∈ 𝐵 ∧ (𝑋 + 𝑌) = (𝑌 + 𝑋)))) | ||
Theorem | sscntz 18456* | A centralizer expression for two sets elementwise commuting. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵) → (𝑆 ⊆ (𝑍‘𝑇) ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 (𝑥 + 𝑦) = (𝑦 + 𝑥))) | ||
Theorem | cntzrcl 18457 | Reverse closure for elements of the centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ (𝑋 ∈ (𝑍‘𝑆) → (𝑀 ∈ V ∧ 𝑆 ⊆ 𝐵)) | ||
Theorem | cntzssv 18458 | The centralizer is unconditionally a subset. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ (𝑍‘𝑆) ⊆ 𝐵 | ||
Theorem | cntzi 18459 | Membership in a centralizer (inference). (Contributed by Stefan O'Rear, 6-Sep-2015.) (Revised by Mario Carneiro, 22-Sep-2015.) |
⊢ + = (+g‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑋 ∈ (𝑍‘𝑆) ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
Theorem | cntrss 18460 | The center is a subset of the base field. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (Cntr‘𝑀) ⊆ 𝐵 | ||
Theorem | cntri 18461 | Defining property of the center of a group. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝑍 = (Cntr‘𝑀) ⇒ ⊢ ((𝑋 ∈ 𝑍 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
Theorem | resscntz 18462 | Centralizer in a substructure. (Contributed by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 𝑌 = (Cntz‘𝐻) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑌‘𝑆) = ((𝑍‘𝑆) ∩ 𝐴)) | ||
Theorem | cntz2ss 18463 | Centralizers reverse the subset relation. (Contributed by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝑆) → (𝑍‘𝑆) ⊆ (𝑍‘𝑇)) | ||
Theorem | cntzrec 18464 | Reciprocity relationship for centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵) → (𝑆 ⊆ (𝑍‘𝑇) ↔ 𝑇 ⊆ (𝑍‘𝑆))) | ||
Theorem | cntziinsn 18465* | Express any centralizer as an intersection of singleton centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ (𝑆 ⊆ 𝐵 → (𝑍‘𝑆) = (𝐵 ∩ ∩ 𝑥 ∈ 𝑆 (𝑍‘{𝑥}))) | ||
Theorem | cntzsubm 18466 | 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 18467 | Centralizers in a group are subgroups. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubGrp‘𝑀)) | ||
Theorem | cntzidss 18468 | If the elements of 𝑆 commute, the elements of a subset 𝑇 also commute. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ ((𝑆 ⊆ (𝑍‘𝑆) ∧ 𝑇 ⊆ 𝑆) → 𝑇 ⊆ (𝑍‘𝑇)) | ||
Theorem | cntzmhm 18469 | Centralizers in a monoid are preserved by monoid homomorphisms. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 𝑌 = (Cntz‘𝐻) ⇒ ⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) → (𝐹‘𝐴) ∈ (𝑌‘(𝐹 “ 𝑆))) | ||
Theorem | cntzmhm2 18470 | Centralizers in a monoid are preserved by monoid homomorphisms. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 𝑌 = (Cntz‘𝐻) ⇒ ⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑆 ⊆ (𝑍‘𝑇)) → (𝐹 “ 𝑆) ⊆ (𝑌‘(𝐹 “ 𝑇))) | ||
Theorem | cntrsubgnsg 18471 | A central subgroup is normal. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝑍 = (Cntr‘𝑀) ⇒ ⊢ ((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) → 𝑋 ∈ (NrmSGrp‘𝑀)) | ||
Theorem | cntrnsg 18472 | The center of a group is a normal subgroup. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝑍 = (Cntr‘𝑀) ⇒ ⊢ (𝑀 ∈ Grp → 𝑍 ∈ (NrmSGrp‘𝑀)) | ||
Syntax | coppg 18473 | The opposite group operation. |
class oppg | ||
Definition | df-oppg 18474 | Define an opposite group, which is the same as the original group but with addition written the other way around. df-oppr 19373 does the same thing for multiplication. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
⊢ oppg = (𝑤 ∈ V ↦ (𝑤 sSet 〈(+g‘ndx), tpos (+g‘𝑤)〉)) | ||
Theorem | oppgval 18475 | 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 18476 | 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 18477 | 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 | oppglem 18478 | Lemma for oppgbas 18479. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 ≠ 2 ⇒ ⊢ (𝐸‘𝑅) = (𝐸‘𝑂) | ||
Theorem | oppgbas 18479 | Base set of an opposite group. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ 𝐵 = (Base‘𝑂) | ||
Theorem | oppgtset 18480 | Topology of an opposite group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ 𝐽 = (TopSet‘𝑅) ⇒ ⊢ 𝐽 = (TopSet‘𝑂) | ||
Theorem | oppgtopn 18481 | Topology of an opposite group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑅) ⇒ ⊢ 𝐽 = (TopOpen‘𝑂) | ||
Theorem | oppgmnd 18482 | 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 18483 | Bidirectional form of oppgmnd 18482. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝑅) ⇒ ⊢ (𝑅 ∈ Mnd ↔ 𝑂 ∈ Mnd) | ||
Theorem | oppgid 18484 | 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 18485 | The opposite of a group is a group. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝑅) ⇒ ⊢ (𝑅 ∈ Grp → 𝑂 ∈ Grp) | ||
Theorem | oppggrpb 18486 | Bidirectional form of oppggrp 18485. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝑅) ⇒ ⊢ (𝑅 ∈ Grp ↔ 𝑂 ∈ Grp) | ||
Theorem | oppginv 18487 | Inverses in a group are a symmetric notion. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) ⇒ ⊢ (𝑅 ∈ Grp → 𝐼 = (invg‘𝑂)) | ||
Theorem | invoppggim 18488 | The inverse is an antiautomorphism on any group. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝐼 ∈ (𝐺 GrpIso 𝑂)) | ||
Theorem | oppggic 18489 | Every group is (naturally) isomorphic to its opposite. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝐺 ≃𝑔 𝑂) | ||
Theorem | oppgsubm 18490 | Being a submonoid is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝑂 = (oppg‘𝐺) ⇒ ⊢ (SubMnd‘𝐺) = (SubMnd‘𝑂) | ||
Theorem | oppgsubg 18491 | Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝑂 = (oppg‘𝐺) ⇒ ⊢ (SubGrp‘𝐺) = (SubGrp‘𝑂) | ||
Theorem | oppgcntz 18492 | 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 18493 | 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 18494 | 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 18496. However, the
set is allowed to be empty, see symgbas0 18517. Hint: The symmetric groups
should not be confused with "symmetry groups" which is a different topic in
group theory.
| ||
Syntax | csymg 18495 | Extend class notation to include the class of symmetric groups. |
class SymGrp | ||
Definition | df-symg 18496* | Define the symmetric group on set 𝑥. We represent the group as the set of one-to-one onto functions from 𝑥 to itself under function composition, and topologize it as a function space assuming the set is discrete. This definition is based on the fact that a symmetric group is a restriction of the monoid of endofunctions. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by AV, 28-Mar-2024.) |
⊢ SymGrp = (𝑥 ∈ V ↦ ((EndoFMnd‘𝑥) ↾s {ℎ ∣ ℎ:𝑥–1-1-onto→𝑥})) | ||
Theorem | symgval 18497* | The value of the symmetric group function at 𝐴. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 12-Jan-2015.) (Revised by AV, 28-Mar-2024.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} ⇒ ⊢ 𝐺 = ((EndoFMnd‘𝐴) ↾s 𝐵) | ||
Theorem | permsetex 18498* | The set of permutations of a set 𝐴 exists. (Contributed by AV, 30-Mar-2024.) |
⊢ (𝐴 ∈ 𝑉 → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐴} ∈ V) | ||
Theorem | symgbas 18499* | The base set of the symmetric group. (Contributed by Mario Carneiro, 12-Jan-2015.) (Proof shortened by AV, 29-Mar-2024.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ 𝐵 = {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} | ||
Theorem | symgbasex 18500 | The base set of the symmetric group over a set 𝐴 exists. (Contributed by AV, 30-Mar-2024.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐵 ∈ V) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |