P. 182 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18101-18200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	gictr 18101	Isomorphism is transitive. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ ((𝑅 ≃𝑔 𝑆 ∧ 𝑆 ≃𝑔 𝑇) → 𝑅 ≃𝑔 𝑇)
Theorem	gicer 18102	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 18103	Isomorphic groups have equinumerous base sets. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝑅 ≃𝑔 𝑆 → 𝐵 ≈ 𝐶)
Theorem	gicsubgen 18104	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.6  Group actions
Syntax	cga 18105	Extend class definition to include the class of group actions.
class GrpAct
Definition	df-ga 18106*	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‘𝑔) / 𝑏⦌{𝑚 ∈ (𝑠 ↑𝑚 (𝑏 × 𝑠)) ∣ ∀𝑥 ∈ 𝑠 (((0g‘𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
Theorem	isga 18107*	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 18122). 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 18108	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 18109	The right argument of a group action is a set. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → 𝑌 ∈ V)
Theorem	gagrpid 18110	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 18111	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 18112	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 18113	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 18114	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 18115	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 18116*	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 18117*	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 18118	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 18119*	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 18120	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 18121	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 18122*	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 18123*	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 18124*	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 18125*	The stabilizer subgroup in a group action. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴}    ⇒   ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐻 ∈ (SubGrp‘𝐺))
Theorem	gastacos 18126*	Write the coset relation for the stabilizer subgroup. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴}    &   ⊢ ∼ = (𝐺 ~QG 𝐻)    ⇒   ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐵 ∼ 𝐶 ↔ (𝐵 ⊕ 𝐴) = (𝐶 ⊕ 𝐴)))
Theorem	orbstafun 18127*	Existence and uniqueness for the function of orbsta 18129. (Contributed by Mario Carneiro, 15-Jan-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴}    &   ⊢ ∼ = (𝐺 ~QG 𝐻)    &   ⊢ 𝐹 = ran (𝑘 ∈ 𝑋 ↦ ⟨[𝑘] ∼ , (𝑘 ⊕ 𝐴)⟩)    ⇒   ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → Fun 𝐹)
Theorem	orbstaval 18128*	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 18129*	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 18130*	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.7  Centralizers and centers
Syntax	ccntz 18131	Syntax for the centralizer of a set in a monoid.
class Cntz
Syntax	ccntr 18132	Syntax for the centralizer of a monoid.
class Cntr
Definition	df-cntz 18133*	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 18134	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 18135	Substitute definition of the center. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑍‘𝐵) = (Cntr‘𝑀)
Theorem	cntzfval 18136*	First level substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑀 ∈ 𝑉 → 𝑍 = (𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)}))
Theorem	cntzval 18137*	Definition substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑆 ⊆ 𝐵 → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)})
Theorem	elcntz 18138*	Elementhood in the centralizer. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑆 ⊆ 𝐵 → (𝐴 ∈ (𝑍‘𝑆) ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝑆 (𝐴 + 𝑦) = (𝑦 + 𝐴))))
Theorem	cntzel 18139*	Membership in a centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑋 ∈ (𝑍‘𝑆) ↔ ∀𝑦 ∈ 𝑆 (𝑋 + 𝑦) = (𝑦 + 𝑋)))
Theorem	cntzsnval 18140*	Special substitution for the centralizer of a singleton. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑌 ∈ 𝐵 → (𝑍‘{𝑌}) = {𝑥 ∈ 𝐵 ∣ (𝑥 + 𝑌) = (𝑌 + 𝑥)})
Theorem	elcntzsn 18141	Value of the centralizer of a singleton. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑌 ∈ 𝐵 → (𝑋 ∈ (𝑍‘{𝑌}) ↔ (𝑋 ∈ 𝐵 ∧ (𝑋 + 𝑌) = (𝑌 + 𝑋))))
Theorem	sscntz 18142*	A centralizer expression for two sets elementwise commuting. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵) → (𝑆 ⊆ (𝑍‘𝑇) ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 (𝑥 + 𝑦) = (𝑦 + 𝑥)))
Theorem	cntzrcl 18143	Reverse closure for elements of the centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑋 ∈ (𝑍‘𝑆) → (𝑀 ∈ V ∧ 𝑆 ⊆ 𝐵))
Theorem	cntzssv 18144	The centralizer is unconditionally a subset. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑍‘𝑆) ⊆ 𝐵
Theorem	cntzi 18145	Membership in a centralizer (inference). (Contributed by Stefan O'Rear, 6-Sep-2015.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑋 ∈ (𝑍‘𝑆) ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	cntri 18146	Defining property of the center of a group. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntr‘𝑀)    ⇒   ⊢ ((𝑋 ∈ 𝑍 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	resscntz 18147	Centralizer in a substructure. (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 𝑌 = (Cntz‘𝐻)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑌‘𝑆) = ((𝑍‘𝑆) ∩ 𝐴))
Theorem	cntz2ss 18148	Centralizers reverse the subset relation. (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝑆) → (𝑍‘𝑆) ⊆ (𝑍‘𝑇))
Theorem	cntzrec 18149	Reciprocity relationship for centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵) → (𝑆 ⊆ (𝑍‘𝑇) ↔ 𝑇 ⊆ (𝑍‘𝑆)))
Theorem	cntziinsn 18150*	Express any centralizer as an intersection of singleton centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑆 ⊆ 𝐵 → (𝑍‘𝑆) = (𝐵 ∩ ∩ 𝑥 ∈ 𝑆 (𝑍‘{𝑥})))
Theorem	cntzsubm 18151	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 18152	Centralizers in a group are subgroups. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubGrp‘𝑀))
Theorem	cntzidss 18153	If the elements of 𝑆 commute, the elements of a subset 𝑇 also commute. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ 𝑍 = (Cntz‘𝐺)    ⇒   ⊢ ((𝑆 ⊆ (𝑍‘𝑆) ∧ 𝑇 ⊆ 𝑆) → 𝑇 ⊆ (𝑍‘𝑇))
Theorem	cntzmhm 18154	Centralizers in a monoid are preserved by monoid homomorphisms. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 𝑌 = (Cntz‘𝐻)    ⇒   ⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) → (𝐹‘𝐴) ∈ (𝑌‘(𝐹 “ 𝑆)))
Theorem	cntzmhm2 18155	Centralizers in a monoid are preserved by monoid homomorphisms. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 𝑌 = (Cntz‘𝐻)    ⇒   ⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑆 ⊆ (𝑍‘𝑇)) → (𝐹 “ 𝑆) ⊆ (𝑌‘(𝐹 “ 𝑇)))
Theorem	cntrsubgnsg 18156	A central subgroup is normal. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝑍 = (Cntr‘𝑀)    ⇒   ⊢ ((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) → 𝑋 ∈ (NrmSGrp‘𝑀))
Theorem	cntrnsg 18157	The center of a group is a normal subgroup. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝑍 = (Cntr‘𝑀)    ⇒   ⊢ (𝑀 ∈ Grp → 𝑍 ∈ (NrmSGrp‘𝑀))
10.2.8  The opposite group
Syntax	coppg 18158	The opposite group operation.
class oppg
Definition	df-oppg 18159	Define an opposite group, which is the same as the original group but with addition written the other way around. df-oppr 19010 does the same thing for multiplication. (Contributed by Stefan O'Rear, 25-Aug-2015.)
⊢ oppg = (𝑤 ∈ V ↦ (𝑤 sSet ⟨(+g‘ndx), tpos (+g‘𝑤)⟩))
Theorem	oppgval 18160	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 18161	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 18162	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 18163	Lemma for oppgbas 18164. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝑅)    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑁 ≠ 2    ⇒   ⊢ (𝐸‘𝑅) = (𝐸‘𝑂)
Theorem	oppgbas 18164	Base set of an opposite group. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ 𝐵 = (Base‘𝑂)
Theorem	oppgtset 18165	Topology of an opposite group. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝑂 = (oppg‘𝑅)    &   ⊢ 𝐽 = (TopSet‘𝑅)    ⇒   ⊢ 𝐽 = (TopSet‘𝑂)
Theorem	oppgtopn 18166	Topology of an opposite group. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝑂 = (oppg‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑅)    ⇒   ⊢ 𝐽 = (TopOpen‘𝑂)
Theorem	oppgmnd 18167	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 18168	Bidirectional form of oppgmnd 18167. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝑅)    ⇒   ⊢ (𝑅 ∈ Mnd ↔ 𝑂 ∈ Mnd)
Theorem	oppgid 18169	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 18170	The opposite of a group is a group. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝑅)    ⇒   ⊢ (𝑅 ∈ Grp → 𝑂 ∈ Grp)
Theorem	oppggrpb 18171	Bidirectional form of oppggrp 18170. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝑅)    ⇒   ⊢ (𝑅 ∈ Grp ↔ 𝑂 ∈ Grp)
Theorem	oppginv 18172	Inverses in a group are a symmetric notion. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝑅)    &   ⊢ 𝐼 = (invg‘𝑅)    ⇒   ⊢ (𝑅 ∈ Grp → 𝐼 = (invg‘𝑂))
Theorem	invoppggim 18173	The inverse is an antiautomorphism on any group. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝐼 ∈ (𝐺 GrpIso 𝑂))
Theorem	oppggic 18174	Every group is (naturally) isomorphic to its opposite. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝐺 ≃𝑔 𝑂)
Theorem	oppgsubm 18175	Being a submonoid is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝑂 = (oppg‘𝐺)    ⇒   ⊢ (SubMnd‘𝐺) = (SubMnd‘𝑂)
Theorem	oppgsubg 18176	Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝑂 = (oppg‘𝐺)    ⇒   ⊢ (SubGrp‘𝐺) = (SubGrp‘𝑂)
Theorem	oppgcntz 18177	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 18178	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 18179	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.9  Symmetric groups
10.2.9.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 18181. However, the set is allowed to be empty, see symgbas0 18197. 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 18183), 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). This means that a symmetric group is a permutation group, and each permutation group is a subgroup of a symmetric group (see pgrpsubgsymgbi 18210 and pgrpsubgsymg 18211). 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 18214, which is a (proper) subgroup of a symmetric group, see idressubgsymg 18213. As in [Rotman] p. 28 "Let 𝑥 ∈ 𝑋 and 𝑝 ∈ SymGrp(𝑋); we say 𝑝 fixes 𝑥 if (𝑝‘𝑥) = 𝑥; otherwise 𝑝 moves 𝑥.". The theorems starting with symgfix2 18219 are about fixed/moved elements.
Syntax	csymg 18180	Extend class notation to include the class of symmetric groups.
class SymGrp
Definition	df-symg 18181*	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. (Contributed by Paul Chapman, 25-Feb-2008.)
⊢ SymGrp = (𝑥 ∈ V ↦ ⦋{ℎ ∣ ℎ:𝑥–1-1-onto→𝑥} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})
Theorem	symgval 18182*	The value of the symmetric group function at 𝐴. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 12-Jan-2015.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴}    &   ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔))    &   ⊢ 𝐽 = (∏t‘(𝐴 × {𝒫 𝐴}))    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩})
Theorem	symgbas 18183*	The base set of the symmetric group. (Contributed by Mario Carneiro, 12-Jan-2015.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ 𝐵 = {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴}
Theorem	elsymgbas2 18184	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 18185	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 18186	Elements in the symmetric group are 1-1 onto functions. (Contributed by SO, 9-Jul-2018.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐴–1-1-onto→𝐴)
Theorem	symgbasf 18187	A permutation (element of the symmetric group) is a function from a set into itself. (Contributed by AV, 1-Jan-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐴⟶𝐴)
Theorem	symghash 18188	The symmetric group on 𝑛 objects has cardinality 𝑛!. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ Fin → (♯‘𝐵) = (!‘(♯‘𝐴)))
Theorem	symgbasfi 18189	The symmetric group on a finite index set is finite. (Contributed by SO, 9-Jul-2018.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ Fin → 𝐵 ∈ Fin)
Theorem	symgfv 18190	The function value of a permutation. (Contributed by AV, 1-Jan-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) ∈ 𝐴)
Theorem	symgfvne 18191	The function values of a permutation for different arguments are different. (Contributed by AV, 8-Jan-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹‘𝑋) = 𝑍 → (𝑌 ≠ 𝑋 → (𝐹‘𝑌) ≠ 𝑍)))
Theorem	symgplusg 18192*	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.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔))
Theorem	symgov 18193	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.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌))
Theorem	symgcl 18194	The group operation of the symmetric group on 𝐴 is closed, i.e. a magma. (Contributed by Mario Carneiro, 12-Jan-2015.) (Revised by Mario Carneiro, 28-Jan-2015.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	symgmov1 18195*	For a permutation of a set, each element of the set replaces an(other) element of the set. (Contributed by AV, 2-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    ⇒   ⊢ (𝑄 ∈ 𝑃 → ∀𝑛 ∈ 𝑁 ∃𝑘 ∈ 𝑁 (𝑄‘𝑛) = 𝑘)
Theorem	symgmov2 18196*	For a permutation of a set, each element of the set is replaced by an(other) element of the set. (Contributed by AV, 2-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    ⇒   ⊢ (𝑄 ∈ 𝑃 → ∀𝑛 ∈ 𝑁 ∃𝑘 ∈ 𝑁 (𝑄‘𝑘) = 𝑛)
Theorem	symgbas0 18197	The base set of the symmetric group on the empty set is the singleton containing the empty set. (Contributed by AV, 27-Feb-2019.)
⊢ (Base‘(SymGrp‘∅)) = {∅}
Theorem	symg1hash 18198	The symmetric group on a singleton has cardinality 1. (Contributed by AV, 9-Dec-2018.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼}    ⇒   ⊢ (𝐼 ∈ 𝑉 → (♯‘𝐵) = 1)
Theorem	symg1bas 18199	The symmetric group on a singleton is the symmetric group S1 consisting of the identity only. (Contributed by AV, 9-Dec-2018.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼}    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐵 = {{⟨𝐼, 𝐼⟩}})
Theorem	symg2hash 18200	The symmetric group on a (proper) pair has cardinality 2. (Contributed by AV, 9-Dec-2018.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼, 𝐽}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) → (♯‘𝐵) = 2)