P. 190 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18901-19000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	gicer 18901	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 18902	Isomorphic groups have equinumerous base sets. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝑅 ≃𝑔 𝑆 → 𝐵 ≈ 𝐶)
Theorem	gicsubgen 18903	A less trivial example of a group invariant: cardinality of the subgroup lattice. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝑅 ≃𝑔 𝑆 → (SubGrp‘𝑅) ≈ (SubGrp‘𝑆))
10.2.7  Group actions
Syntax	cga 18904	Extend class definition to include the class of group actions.
class GrpAct
Definition	df-ga 18905*	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 18906*	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 18921). 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 18907	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 18908	The right argument of a group action is a set. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → 𝑌 ∈ V)
Theorem	gagrpid 18909	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 18910	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 18911	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 18912	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 18913	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 18914	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 18915*	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 18916*	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 18917	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 18918*	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 18919	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 18920	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 18921*	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 18922*	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 18923*	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 18924*	The stabilizer subgroup in a group action. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴}    ⇒   ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐻 ∈ (SubGrp‘𝐺))
Theorem	gastacos 18925*	Write the coset relation for the stabilizer subgroup. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴}    &   ⊢ ∼ = (𝐺 ~QG 𝐻)    ⇒   ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐵 ∼ 𝐶 ↔ (𝐵 ⊕ 𝐴) = (𝐶 ⊕ 𝐴)))
Theorem	orbstafun 18926*	Existence and uniqueness for the function of orbsta 18928. (Contributed by Mario Carneiro, 15-Jan-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴}    &   ⊢ ∼ = (𝐺 ~QG 𝐻)    &   ⊢ 𝐹 = ran (𝑘 ∈ 𝑋 ↦ ⟨[𝑘] ∼ , (𝑘 ⊕ 𝐴)⟩)    ⇒   ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → Fun 𝐹)
Theorem	orbstaval 18927*	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 18928*	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 18929*	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) → (♯‘𝑋) = ((♯‘[𝐴]𝑂) · (♯‘𝐻)))
10.2.8  Centralizers and centers
Syntax	ccntz 18930	Syntax for the centralizer of a set in a monoid.
class Cntz
Syntax	ccntr 18931	Syntax for the centralizer of a monoid.
class Cntr
Definition	df-cntz 18932*	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 18933	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 18934	Substitute definition of the center. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑍‘𝐵) = (Cntr‘𝑀)
Theorem	cntzfval 18935*	First level substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑀 ∈ 𝑉 → 𝑍 = (𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)}))
Theorem	cntzval 18936*	Definition substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑆 ⊆ 𝐵 → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)})
Theorem	elcntz 18937*	Elementhood in the centralizer. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑆 ⊆ 𝐵 → (𝐴 ∈ (𝑍‘𝑆) ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝑆 (𝐴 + 𝑦) = (𝑦 + 𝐴))))
Theorem	cntzel 18938*	Membership in a centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑋 ∈ (𝑍‘𝑆) ↔ ∀𝑦 ∈ 𝑆 (𝑋 + 𝑦) = (𝑦 + 𝑋)))
Theorem	cntzsnval 18939*	Special substitution for the centralizer of a singleton. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑌 ∈ 𝐵 → (𝑍‘{𝑌}) = {𝑥 ∈ 𝐵 ∣ (𝑥 + 𝑌) = (𝑌 + 𝑥)})
Theorem	elcntzsn 18940	Value of the centralizer of a singleton. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑌 ∈ 𝐵 → (𝑋 ∈ (𝑍‘{𝑌}) ↔ (𝑋 ∈ 𝐵 ∧ (𝑋 + 𝑌) = (𝑌 + 𝑋))))
Theorem	sscntz 18941*	A centralizer expression for two sets elementwise commuting. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵) → (𝑆 ⊆ (𝑍‘𝑇) ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 (𝑥 + 𝑦) = (𝑦 + 𝑥)))
Theorem	cntzrcl 18942	Reverse closure for elements of the centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑋 ∈ (𝑍‘𝑆) → (𝑀 ∈ V ∧ 𝑆 ⊆ 𝐵))
Theorem	cntzssv 18943	The centralizer is unconditionally a subset. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑍‘𝑆) ⊆ 𝐵
Theorem	cntzi 18944	Membership in a centralizer (inference). (Contributed by Stefan O'Rear, 6-Sep-2015.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑋 ∈ (𝑍‘𝑆) ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	cntrss 18945	The center is a subset of the base field. (Contributed by Thierry Arnoux, 21-Aug-2023.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (Cntr‘𝑀) ⊆ 𝐵
Theorem	cntri 18946	Defining property of the center of a group. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntr‘𝑀)    ⇒   ⊢ ((𝑋 ∈ 𝑍 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	resscntz 18947	Centralizer in a substructure. (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 𝑌 = (Cntz‘𝐻)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑌‘𝑆) = ((𝑍‘𝑆) ∩ 𝐴))
Theorem	cntz2ss 18948	Centralizers reverse the subset relation. (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝑆) → (𝑍‘𝑆) ⊆ (𝑍‘𝑇))
Theorem	cntzrec 18949	Reciprocity relationship for centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵) → (𝑆 ⊆ (𝑍‘𝑇) ↔ 𝑇 ⊆ (𝑍‘𝑆)))
Theorem	cntziinsn 18950*	Express any centralizer as an intersection of singleton centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑆 ⊆ 𝐵 → (𝑍‘𝑆) = (𝐵 ∩ ∩ 𝑥 ∈ 𝑆 (𝑍‘{𝑥})))
Theorem	cntzsubm 18951	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 18952	Centralizers in a group are subgroups. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubGrp‘𝑀))
Theorem	cntzidss 18953	If the elements of 𝑆 commute, the elements of a subset 𝑇 also commute. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ 𝑍 = (Cntz‘𝐺)    ⇒   ⊢ ((𝑆 ⊆ (𝑍‘𝑆) ∧ 𝑇 ⊆ 𝑆) → 𝑇 ⊆ (𝑍‘𝑇))
Theorem	cntzmhm 18954	Centralizers in a monoid are preserved by monoid homomorphisms. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 𝑌 = (Cntz‘𝐻)    ⇒   ⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) → (𝐹‘𝐴) ∈ (𝑌‘(𝐹 “ 𝑆)))
Theorem	cntzmhm2 18955	Centralizers in a monoid are preserved by monoid homomorphisms. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 𝑌 = (Cntz‘𝐻)    ⇒   ⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑆 ⊆ (𝑍‘𝑇)) → (𝐹 “ 𝑆) ⊆ (𝑌‘(𝐹 “ 𝑇)))
Theorem	cntrsubgnsg 18956	A central subgroup is normal. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝑍 = (Cntr‘𝑀)    ⇒   ⊢ ((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) → 𝑋 ∈ (NrmSGrp‘𝑀))
Theorem	cntrnsg 18957	The center of a group is a normal subgroup. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝑍 = (Cntr‘𝑀)    ⇒   ⊢ (𝑀 ∈ Grp → 𝑍 ∈ (NrmSGrp‘𝑀))
10.2.9  The opposite group
Syntax	coppg 18958	The opposite group operation.
class oppg
Definition	df-oppg 18959	Define an opposite group, which is the same as the original group but with addition written the other way around. df-oppr 19871 does the same thing for multiplication. (Contributed by Stefan O'Rear, 25-Aug-2015.)
⊢ oppg = (𝑤 ∈ V ↦ (𝑤 sSet ⟨(+g‘ndx), tpos (+g‘𝑤)⟩))
Theorem	oppgval 18960	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 18961	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 18962	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 18963	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 18964	Obsolete version of setsplusg 18963 as of 18-Oct-2024. Lemma for oppgbas 18965. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑂 = (oppg‘𝑅)    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑁 ≠ 2    ⇒   ⊢ (𝐸‘𝑅) = (𝐸‘𝑂)
Theorem	oppgbas 18965	Base set of an opposite group. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ 𝐵 = (Base‘𝑂)
Theorem	oppgbasOLD 18966	Obsolete version of oppgbas 18965 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 18967	Topology of an opposite group. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝑂 = (oppg‘𝑅)    &   ⊢ 𝐽 = (TopSet‘𝑅)    ⇒   ⊢ 𝐽 = (TopSet‘𝑂)
Theorem	oppgtsetOLD 18968	Obsolete version of oppgtset 18967 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 18969	Topology of an opposite group. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝑂 = (oppg‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑅)    ⇒   ⊢ 𝐽 = (TopOpen‘𝑂)
Theorem	oppgmnd 18970	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 18971	Bidirectional form of oppgmnd 18970. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝑅)    ⇒   ⊢ (𝑅 ∈ Mnd ↔ 𝑂 ∈ Mnd)
Theorem	oppgid 18972	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 18973	The opposite of a group is a group. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝑅)    ⇒   ⊢ (𝑅 ∈ Grp → 𝑂 ∈ Grp)
Theorem	oppggrpb 18974	Bidirectional form of oppggrp 18973. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝑅)    ⇒   ⊢ (𝑅 ∈ Grp ↔ 𝑂 ∈ Grp)
Theorem	oppginv 18975	Inverses in a group are a symmetric notion. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝑅)    &   ⊢ 𝐼 = (invg‘𝑅)    ⇒   ⊢ (𝑅 ∈ Grp → 𝐼 = (invg‘𝑂))
Theorem	invoppggim 18976	The inverse is an antiautomorphism on any group. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝐼 ∈ (𝐺 GrpIso 𝑂))
Theorem	oppggic 18977	Every group is (naturally) isomorphic to its opposite. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝐺 ≃𝑔 𝑂)
Theorem	oppgsubm 18978	Being a submonoid is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝑂 = (oppg‘𝐺)    ⇒   ⊢ (SubMnd‘𝐺) = (SubMnd‘𝑂)
Theorem	oppgsubg 18979	Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝑂 = (oppg‘𝐺)    ⇒   ⊢ (SubGrp‘𝐺) = (SubGrp‘𝑂)
Theorem	oppgcntz 18980	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 18981	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 18982	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‘𝑊)))
10.2.10  Symmetric groups
10.2.10.1  Definition and basic properties 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 18984. However, the set is allowed to be empty, see symgbas0 19005. Hint: The symmetric groups should not be confused with "symmetry groups" which is a different topic in group theory. In this context, the one-to-one onto functions are called permutations for short. Since the base set of symmetric groups on a set 𝐴 is the set of all permutations of 𝐴 (see symgbas 18987), we can formally say 𝑃 ∈ (SymGrp‘𝐴) expressing "𝑃 is a permutation of 𝐴" if we are not interested in the group (or topology) structure. In general, a permutation group "... is a group G whose elements are permutations of a given set M and whose group operation is the composition of permutations in G (which are thought of as bijective functions from the set M to itself)." (see Wikipedia "Permutation group", 17-Mar-2019, https://en.wikipedia.org/wiki/Permutation_group 18987). This means that a symmetric group is a permutation group, and each permutation group is a subgroup of a symmetric group (see pgrpsubgsymgbi 19025 and pgrpsubgsymg 19026). For example, the structure with the singleton containing only the identity function restricted to a set as base set and the function composition as group operation is a permutation group (group consisting of permutations), see idrespermg 19028, which is a (proper) subgroup of a symmetric group, see idressubgsymg 19027. As in [Rotman] p. 28 "Let 𝑥 ∈ 𝑋 and 𝑝 ∈ SymGrp(𝑋); we say 𝑝 fixes 𝑥 if (𝑝‘𝑥) = 𝑥; otherwise 𝑝 moves 𝑥.". The theorems starting with symgfix2 19033 are about fixed/moved elements.
Syntax	csymg 18983	Extend class notation to include the class of symmetric groups.
class SymGrp
Definition	df-symg 18984*	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 18985*	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	permsetexOLD 18986*	Obsolete version of f1osetex 8656 as of 8-Aug-2024. (Contributed by AV, 30-Mar-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐴} ∈ V)
Theorem	symgbas 18987*	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	symgbasexOLD 18988	Obsolete as of 8-Aug-2024. 𝐵 ∈ V follows immediatly from fvex 6796. (Contributed by AV, 30-Mar-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐵 ∈ V)
Theorem	elsymgbas2 18989	Two ways of saying a function is a 1-1-onto mapping of A to itself. (Contributed by Mario Carneiro, 28-Jan-2015.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝐵 ↔ 𝐹:𝐴–1-1-onto→𝐴))
Theorem	elsymgbas 18990	Two ways of saying a function is a 1-1-onto mapping of A to itself. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 28-Jan-2015.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐹 ∈ 𝐵 ↔ 𝐹:𝐴–1-1-onto→𝐴))
Theorem	symgbasf1o 18991	Elements in the symmetric group are 1-1 onto functions. (Contributed by SO, 9-Jul-2018.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐴–1-1-onto→𝐴)
Theorem	symgbasf 18992	A permutation (element of the symmetric group) is a function from a set into itself. (Contributed by AV, 1-Jan-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐴⟶𝐴)
Theorem	symgbasmap 18993	A permutation (element of the symmetric group) is a mapping (or set exponentiation) from a set into itself. (Contributed by AV, 30-Mar-2024.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹 ∈ (𝐴 ↑m 𝐴))
Theorem	symghash 18994	The symmetric group on 𝑛 objects has cardinality 𝑛!. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ Fin → (♯‘𝐵) = (!‘(♯‘𝐴)))
Theorem	symgbasfi 18995	The symmetric group on a finite index set is finite. (Contributed by SO, 9-Jul-2018.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ Fin → 𝐵 ∈ Fin)
Theorem	symgfv 18996	The function value of a permutation. (Contributed by AV, 1-Jan-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) ∈ 𝐴)
Theorem	symgfvne 18997	The function values of a permutation for different arguments are different. (Contributed by AV, 8-Jan-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹‘𝑋) = 𝑍 → (𝑌 ≠ 𝑋 → (𝐹‘𝑌) ≠ 𝑍)))
Theorem	symgressbas 18998	The symmetric group on 𝐴 characterized as structure restriction of the monoid of endofunctions on 𝐴 to its base set. (Contributed by AV, 30-Mar-2024.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑀 = (EndoFMnd‘𝐴)    ⇒   ⊢ 𝐺 = (𝑀 ↾s 𝐵)
Theorem	symgplusg 18999*	The group operation of a symmetric group is the function composition. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 28-Jan-2015.) (Proof shortened by AV, 19-Feb-2024.) (Revised by AV, 29-Mar-2024.) (Proof shortened by AV, 14-Aug-2024.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (𝐴 ↑m 𝐴)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔))
Theorem	symgov 19000	The value of the group operation of the symmetric group on 𝐴. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 28-Jan-2015.) (Revised by AV, 30-Mar-2024.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌))