P. 197 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19601-19700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pj1ghm2 19601	The left projection function is a group homomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    &   ⊢ 𝑃 = (proj1‘𝐺)    ⇒   ⊢ (𝜑 → (𝑇𝑃𝑈) ∈ ((𝐺 ↾s (𝑇 ⊕ 𝑈)) GrpHom (𝐺 ↾s 𝑇)))
Theorem	lsmhash 19602	The order of the direct product of groups. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    &   ⊢ (𝜑 → 𝑇 ∈ Fin)    &   ⊢ (𝜑 → 𝑈 ∈ Fin)    ⇒   ⊢ (𝜑 → (♯‘(𝑇 ⊕ 𝑈)) = ((♯‘𝑇) · (♯‘𝑈)))
10.2.13  Free groups
Syntax	cefg 19603	Extend class notation with the free group equivalence relation.
class ~FG
Syntax	cfrgp 19604	Extend class notation with the free group construction.
class freeGrp
Syntax	cvrgp 19605	Extend class notation with free group injection.
class varFGrp
Definition	df-efg 19606*	Define the free group equivalence relation, which is the smallest equivalence relation ≈ such that for any words 𝐴, 𝐵 and formal symbol 𝑥 with inverse invg𝑥, 𝐴𝐵 ≈ 𝐴𝑥(invg𝑥)𝐵. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ ~FG = (𝑖 ∈ V ↦ ∩ {𝑟 ∣ (𝑟 Er Word (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩))})
Definition	df-frgp 19607	Define the free group on a set 𝐼 of generators, defined as the quotient of the free monoid on 𝐼 × 2o (representing the generator elements and their formal inverses) by the free group equivalence relation df-efg 19606. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ freeGrp = (𝑖 ∈ V ↦ ((freeMnd‘(𝑖 × 2o)) /s ( ~FG ‘𝑖)))
Definition	df-vrgp 19608*	Define the canonical injection from the generating set 𝐼 into the base set of the free group. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ varFGrp = (𝑖 ∈ V ↦ (𝑗 ∈ 𝑖 ↦ [⟨“⟨𝑗, ∅⟩”⟩]( ~FG ‘𝑖)))
Theorem	efgmval 19609*	Value of the formal inverse operation for the generating set of a free group. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    ⇒   ⊢ ((𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 2o) → (𝐴𝑀𝐵) = ⟨𝐴, (1o ∖ 𝐵)⟩)
Theorem	efgmf 19610*	The formal inverse operation is an endofunction on the generating set. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    ⇒   ⊢ 𝑀:(𝐼 × 2o)⟶(𝐼 × 2o)
Theorem	efgmnvl 19611*	The inversion function on the generators is an involution. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    ⇒   ⊢ (𝐴 ∈ (𝐼 × 2o) → (𝑀‘(𝑀‘𝐴)) = 𝐴)
Theorem	efgrcl 19612	Lemma for efgval 19614. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    ⇒   ⊢ (𝐴 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o)))
Theorem	efglem 19613*	Lemma for efgval 19614. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    ⇒   ⊢ ∃𝑟(𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩))
Theorem	efgval 19614*	Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    ⇒   ⊢ ∼ = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩))}
Theorem	efger 19615	Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    ⇒   ⊢ ∼ Er 𝑊
Theorem	efgi 19616	Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    ⇒   ⊢ (((𝐴 ∈ 𝑊 ∧ 𝑁 ∈ (0...(♯‘𝐴))) ∧ (𝐽 ∈ 𝐼 ∧ 𝐾 ∈ 2o)) → 𝐴 ∼ (𝐴 splice ⟨𝑁, 𝑁, ⟨“⟨𝐽, 𝐾⟩⟨𝐽, (1o ∖ 𝐾)⟩”⟩⟩))
Theorem	efgi0 19617	Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    ⇒   ⊢ ((𝐴 ∈ 𝑊 ∧ 𝑁 ∈ (0...(♯‘𝐴)) ∧ 𝐽 ∈ 𝐼) → 𝐴 ∼ (𝐴 splice ⟨𝑁, 𝑁, ⟨“⟨𝐽, ∅⟩⟨𝐽, 1o⟩”⟩⟩))
Theorem	efgi1 19618	Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    ⇒   ⊢ ((𝐴 ∈ 𝑊 ∧ 𝑁 ∈ (0...(♯‘𝐴)) ∧ 𝐽 ∈ 𝐼) → 𝐴 ∼ (𝐴 splice ⟨𝑁, 𝑁, ⟨“⟨𝐽, 1o⟩⟨𝐽, ∅⟩”⟩⟩))
Theorem	efgtf 19619*	Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    ⇒   ⊢ (𝑋 ∈ 𝑊 → ((𝑇‘𝑋) = (𝑎 ∈ (0...(♯‘𝑋)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑋 splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀‘𝑏)”⟩⟩)) ∧ (𝑇‘𝑋):((0...(♯‘𝑋)) × (𝐼 × 2o))⟶𝑊))
Theorem	efgtval 19620*	Value of the extension function, which maps a word (a representation of the group element as a sequence of elements and their inverses) to its direct extensions, defined as the original representation with an element and its inverse inserted somewhere in the string. (Contributed by Mario Carneiro, 29-Sep-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    ⇒   ⊢ ((𝑋 ∈ 𝑊 ∧ 𝑁 ∈ (0...(♯‘𝑋)) ∧ 𝐴 ∈ (𝐼 × 2o)) → (𝑁(𝑇‘𝑋)𝐴) = (𝑋 splice ⟨𝑁, 𝑁, ⟨“𝐴(𝑀‘𝐴)”⟩⟩))
Theorem	efgval2 19621*	Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    ⇒   ⊢ ∼ = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ran (𝑇‘𝑥) ⊆ [𝑥]𝑟)}
Theorem	efgi2 19622*	Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    ⇒   ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ ran (𝑇‘𝐴)) → 𝐴 ∼ 𝐵)
Theorem	efgtlen 19623*	Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    ⇒   ⊢ ((𝑋 ∈ 𝑊 ∧ 𝐴 ∈ ran (𝑇‘𝑋)) → (♯‘𝐴) = ((♯‘𝑋) + 2))
Theorem	efginvrel2 19624*	The inverse of the reverse of a word composed with the word relates to the identity. (This provides an explicit expression for the representation of the group inverse, given a representative of the free group equivalence class.) (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    ⇒   ⊢ (𝐴 ∈ 𝑊 → (𝐴 ++ (𝑀 ∘ (reverse‘𝐴))) ∼ ∅)
Theorem	efginvrel1 19625*	The inverse of the reverse of a word composed with the word relates to the identity. (This provides an explicit expression for the representation of the group inverse, given a representative of the free group equivalence class.) (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    ⇒   ⊢ (𝐴 ∈ 𝑊 → ((𝑀 ∘ (reverse‘𝐴)) ++ 𝐴) ∼ ∅)
Theorem	efgsf 19626*	Value of the auxiliary function 𝑆 defining a sequence of extensions starting at some irreducible word. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    ⇒   ⊢ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊
Theorem	efgsdm 19627*	Elementhood in the domain of 𝑆, the set of sequences of extensions starting at an irreducible word. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    ⇒   ⊢ (𝐹 ∈ dom 𝑆 ↔ (𝐹 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐹‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘𝐹))(𝐹‘𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))))
Theorem	efgsval 19628*	Value of the auxiliary function 𝑆 defining a sequence of extensions. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    ⇒   ⊢ (𝐹 ∈ dom 𝑆 → (𝑆‘𝐹) = (𝐹‘((♯‘𝐹) − 1)))
Theorem	efgsdmi 19629*	Property of the last link in the chain of extensions. (Contributed by Mario Carneiro, 29-Sep-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    ⇒   ⊢ ((𝐹 ∈ dom 𝑆 ∧ ((♯‘𝐹) − 1) ∈ ℕ) → (𝑆‘𝐹) ∈ ran (𝑇‘(𝐹‘(((♯‘𝐹) − 1) − 1))))
Theorem	efgsval2 19630*	Value of the auxiliary function 𝑆 defining a sequence of extensions. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    ⇒   ⊢ ((𝐴 ∈ Word 𝑊 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ++ ⟨“𝐵”⟩) ∈ dom 𝑆) → (𝑆‘(𝐴 ++ ⟨“𝐵”⟩)) = 𝐵)
Theorem	efgsrel 19631*	The start and end of any extension sequence are related (i.e. evaluate to the same element of the quotient group to be created). (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    ⇒   ⊢ (𝐹 ∈ dom 𝑆 → (𝐹‘0) ∼ (𝑆‘𝐹))
Theorem	efgs1 19632*	A singleton of an irreducible word is an extension sequence. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    ⇒   ⊢ (𝐴 ∈ 𝐷 → ⟨“𝐴”⟩ ∈ dom 𝑆)
Theorem	efgs1b 19633*	Every extension sequence ending in an irreducible word is trivial. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    ⇒   ⊢ (𝐴 ∈ dom 𝑆 → ((𝑆‘𝐴) ∈ 𝐷 ↔ (♯‘𝐴) = 1))
Theorem	efgsp1 19634*	If 𝐹 is an extension sequence and 𝐴 is an extension of the last element of 𝐹, then 𝐹 + ⟨“𝐴”⟩ is an extension sequence. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    ⇒   ⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (𝐹 ++ ⟨“𝐴”⟩) ∈ dom 𝑆)
Theorem	efgsres 19635*	An initial segment of an extension sequence is an extension sequence. (Contributed by Mario Carneiro, 1-Oct-2015.) (Proof shortened by AV, 3-Nov-2022.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    ⇒   ⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → (𝐹 ↾ (0..^𝑁)) ∈ dom 𝑆)
Theorem	efgsfo 19636*	For any word, there is a sequence of extensions starting at a reduced word and ending at the target word, such that each word in the chain is an extension of the previous (inserting an element and its inverse at adjacent indices somewhere in the sequence). (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    ⇒   ⊢ 𝑆:dom 𝑆–onto→𝑊
Theorem	efgredlema 19637*	The reduced word that forms the base of the sequence in efgsval 19628 is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    &   ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑆)    &   ⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵))    &   ⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0))    ⇒   ⊢ (𝜑 → (((♯‘𝐴) − 1) ∈ ℕ ∧ ((♯‘𝐵) − 1) ∈ ℕ))
Theorem	efgredlemf 19638*	Lemma for efgredleme 19640. (Contributed by Mario Carneiro, 4-Jun-2016.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    &   ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑆)    &   ⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵))    &   ⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0))    &   ⊢ 𝐾 = (((♯‘𝐴) − 1) − 1)    &   ⊢ 𝐿 = (((♯‘𝐵) − 1) − 1)    ⇒   ⊢ (𝜑 → ((𝐴‘𝐾) ∈ 𝑊 ∧ (𝐵‘𝐿) ∈ 𝑊))
Theorem	efgredlemg 19639*	Lemma for efgred 19645. (Contributed by Mario Carneiro, 4-Jun-2016.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    &   ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑆)    &   ⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵))    &   ⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0))    &   ⊢ 𝐾 = (((♯‘𝐴) − 1) − 1)    &   ⊢ 𝐿 = (((♯‘𝐵) − 1) − 1)    &   ⊢ (𝜑 → 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))))    &   ⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))))    &   ⊢ (𝜑 → 𝑈 ∈ (𝐼 × 2o))    &   ⊢ (𝜑 → 𝑉 ∈ (𝐼 × 2o))    &   ⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈))    &   ⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉))    ⇒   ⊢ (𝜑 → (♯‘(𝐴‘𝐾)) = (♯‘(𝐵‘𝐿)))
Theorem	efgredleme 19640*	Lemma for efgred 19645. (Contributed by Mario Carneiro, 1-Oct-2015.) (Proof shortened by AV, 15-Oct-2022.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    &   ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑆)    &   ⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵))    &   ⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0))    &   ⊢ 𝐾 = (((♯‘𝐴) − 1) − 1)    &   ⊢ 𝐿 = (((♯‘𝐵) − 1) − 1)    &   ⊢ (𝜑 → 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))))    &   ⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))))    &   ⊢ (𝜑 → 𝑈 ∈ (𝐼 × 2o))    &   ⊢ (𝜑 → 𝑉 ∈ (𝐼 × 2o))    &   ⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈))    &   ⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉))    &   ⊢ (𝜑 → ¬ (𝐴‘𝐾) = (𝐵‘𝐿))    &   ⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(𝑄 + 2)))    &   ⊢ (𝜑 → 𝐶 ∈ dom 𝑆)    &   ⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))    ⇒   ⊢ (𝜑 → ((𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶)) ∧ (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶))))
Theorem	efgredlemd 19641*	The reduced word that forms the base of the sequence in efgsval 19628 is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 1-Oct-2015.) (Proof shortened by AV, 15-Oct-2022.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    &   ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑆)    &   ⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵))    &   ⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0))    &   ⊢ 𝐾 = (((♯‘𝐴) − 1) − 1)    &   ⊢ 𝐿 = (((♯‘𝐵) − 1) − 1)    &   ⊢ (𝜑 → 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))))    &   ⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))))    &   ⊢ (𝜑 → 𝑈 ∈ (𝐼 × 2o))    &   ⊢ (𝜑 → 𝑉 ∈ (𝐼 × 2o))    &   ⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈))    &   ⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉))    &   ⊢ (𝜑 → ¬ (𝐴‘𝐾) = (𝐵‘𝐿))    &   ⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(𝑄 + 2)))    &   ⊢ (𝜑 → 𝐶 ∈ dom 𝑆)    &   ⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴‘𝐾))⟩)))    ⇒   ⊢ (𝜑 → (𝐴‘0) = (𝐵‘0))
Theorem	efgredlemc 19642*	The reduced word that forms the base of the sequence in efgsval 19628 is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 1-Oct-2015.) (Proof shortened by AV, 15-Oct-2022.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    &   ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑆)    &   ⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵))    &   ⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0))    &   ⊢ 𝐾 = (((♯‘𝐴) − 1) − 1)    &   ⊢ 𝐿 = (((♯‘𝐵) − 1) − 1)    &   ⊢ (𝜑 → 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))))    &   ⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))))    &   ⊢ (𝜑 → 𝑈 ∈ (𝐼 × 2o))    &   ⊢ (𝜑 → 𝑉 ∈ (𝐼 × 2o))    &   ⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈))    &   ⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉))    &   ⊢ (𝜑 → ¬ (𝐴‘𝐾) = (𝐵‘𝐿))    ⇒   ⊢ (𝜑 → (𝑃 ∈ (ℤ≥‘𝑄) → (𝐴‘0) = (𝐵‘0)))
Theorem	efgredlemb 19643*	The reduced word that forms the base of the sequence in efgsval 19628 is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 30-Sep-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    &   ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑆)    &   ⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵))    &   ⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0))    &   ⊢ 𝐾 = (((♯‘𝐴) − 1) − 1)    &   ⊢ 𝐿 = (((♯‘𝐵) − 1) − 1)    &   ⊢ (𝜑 → 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))))    &   ⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))))    &   ⊢ (𝜑 → 𝑈 ∈ (𝐼 × 2o))    &   ⊢ (𝜑 → 𝑉 ∈ (𝐼 × 2o))    &   ⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈))    &   ⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉))    &   ⊢ (𝜑 → ¬ (𝐴‘𝐾) = (𝐵‘𝐿))    ⇒   ⊢ ¬ 𝜑
Theorem	efgredlem 19644*	The reduced word that forms the base of the sequence in efgsval 19628 is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 30-Sep-2015.) (Proof shortened by AV, 3-Nov-2022.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    &   ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑆)    &   ⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵))    &   ⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0))    ⇒   ⊢ ¬ 𝜑
Theorem	efgred 19645*	The reduced word that forms the base of the sequence in efgsval 19628 is uniquely determined, given the terminal point. (Contributed by Mario Carneiro, 28-Sep-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    ⇒   ⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆 ∧ (𝑆‘𝐴) = (𝑆‘𝐵)) → (𝐴‘0) = (𝐵‘0))
Theorem	efgrelexlema 19646*	If two words 𝐴, 𝐵 are related under the free group equivalence, then there exist two extension sequences 𝑎, 𝑏 such that 𝑎 ends at 𝐴, 𝑏 ends at 𝐵, and 𝑎 and 𝐵 have the same starting point. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    &   ⊢ 𝐿 = {⟨𝑖, 𝑗⟩ ∣ ∃𝑐 ∈ (◡𝑆 “ {𝑖})∃𝑑 ∈ (◡𝑆 “ {𝑗})(𝑐‘0) = (𝑑‘0)}    ⇒   ⊢ (𝐴𝐿𝐵 ↔ ∃𝑎 ∈ (◡𝑆 “ {𝐴})∃𝑏 ∈ (◡𝑆 “ {𝐵})(𝑎‘0) = (𝑏‘0))
Theorem	efgrelexlemb 19647*	If two words 𝐴, 𝐵 are related under the free group equivalence, then there exist two extension sequences 𝑎, 𝑏 such that 𝑎 ends at 𝐴, 𝑏 ends at 𝐵, and 𝑎 and 𝐵 have the same starting point. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    &   ⊢ 𝐿 = {⟨𝑖, 𝑗⟩ ∣ ∃𝑐 ∈ (◡𝑆 “ {𝑖})∃𝑑 ∈ (◡𝑆 “ {𝑗})(𝑐‘0) = (𝑑‘0)}    ⇒   ⊢ ∼ ⊆ 𝐿
Theorem	efgrelex 19648*	If two words 𝐴, 𝐵 are related under the free group equivalence, then there exist two extension sequences 𝑎, 𝑏 such that 𝑎 ends at 𝐴, 𝑏 ends at 𝐵, and 𝑎 and 𝐵 have the same starting point. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    ⇒   ⊢ (𝐴 ∼ 𝐵 → ∃𝑎 ∈ (◡𝑆 “ {𝐴})∃𝑏 ∈ (◡𝑆 “ {𝐵})(𝑎‘0) = (𝑏‘0))
Theorem	efgredeu 19649*	There is a unique reduced word equivalent to a given word. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    ⇒   ⊢ (𝐴 ∈ 𝑊 → ∃!𝑑 ∈ 𝐷 𝑑 ∼ 𝐴)
Theorem	efgred2 19650*	Two extension sequences have related endpoints iff they have the same base. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    ⇒   ⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆) → ((𝑆‘𝐴) ∼ (𝑆‘𝐵) ↔ (𝐴‘0) = (𝐵‘0)))
Theorem	efgcpbllema 19651*	Lemma for efgrelex 19648. Define an auxiliary equivalence relation 𝐿 such that 𝐴𝐿𝐵 if there are sequences from 𝐴 to 𝐵 passing through the same reduced word. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    &   ⊢ 𝐿 = {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑊 ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ∼ ((𝐴 ++ 𝑗) ++ 𝐵))}    ⇒   ⊢ (𝑋𝐿𝑌 ↔ (𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑊 ∧ ((𝐴 ++ 𝑋) ++ 𝐵) ∼ ((𝐴 ++ 𝑌) ++ 𝐵)))
Theorem	efgcpbllemb 19652*	Lemma for efgrelex 19648. Show that 𝐿 is an equivalence relation containing all direct extensions of a word, so is closed under ∼. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    &   ⊢ 𝐿 = {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝑊 ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ∼ ((𝐴 ++ 𝑗) ++ 𝐵))}    ⇒   ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∼ ⊆ 𝐿)
Theorem	efgcpbl 19653*	Two extension sequences have related endpoints iff they have the same base. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    ⇒   ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ∧ 𝑋 ∼ 𝑌) → ((𝐴 ++ 𝑋) ++ 𝐵) ∼ ((𝐴 ++ 𝑌) ++ 𝐵))
Theorem	efgcpbl2 19654*	Two extension sequences have related endpoints iff they have the same base. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    ⇒   ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → (𝐴 ++ 𝐵) ∼ (𝑋 ++ 𝑌))
Theorem	frgpval 19655	Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ 𝑀 = (freeMnd‘(𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐺 = (𝑀 /s ∼ ))
Theorem	frgpcpbl 19656	Compatibility of the group operation with the free group equivalence relation. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ 𝑀 = (freeMnd‘(𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷) → (𝐴 + 𝐵) ∼ (𝐶 + 𝐷))
Theorem	frgp0 19657	The free group is a group. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ ∼ = ( ~FG ‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → (𝐺 ∈ Grp ∧ [∅] ∼ = (0g‘𝐺)))
Theorem	frgpeccl 19658	Closure of the quotient map in a free group. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑊 → [𝑋] ∼ ∈ 𝐵)
Theorem	frgpgrp 19659	The free group is a group. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝐺 = (freeGrp‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐺 ∈ Grp)
Theorem	frgpadd 19660	Addition in the free group is given by concatenation. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ([𝐴] ∼ + [𝐵] ∼ ) = [(𝐴 ++ 𝐵)] ∼ )
Theorem	frgpinv 19661*	The inverse of an element of the free group. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    ⇒   ⊢ (𝐴 ∈ 𝑊 → (𝑁‘[𝐴] ∼ ) = [(𝑀 ∘ (reverse‘𝐴))] ∼ )
Theorem	frgpmhm 19662*	The "natural map" from words of the free monoid to their cosets in the free group is a surjective monoid homomorphism. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑀 = (freeMnd‘(𝐼 × 2o))    &   ⊢ 𝑊 = (Base‘𝑀)    &   ⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑊 ↦ [𝑥] ∼ )    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐹 ∈ (𝑀 MndHom 𝐺))
Theorem	vrgpfval 19663*	The canonical injection from the generating set 𝐼 to the base set of the free group. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑈 = (varFGrp‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑈 = (𝑗 ∈ 𝐼 ↦ [⟨“⟨𝑗, ∅⟩”⟩] ∼ ))
Theorem	vrgpval 19664	The value of the generating elements of a free group. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑈 = (varFGrp‘𝐼)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) → (𝑈‘𝐴) = [⟨“⟨𝐴, ∅⟩”⟩] ∼ )
Theorem	vrgpf 19665	The mapping from the index set to the generators is a function into the free group. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑈 = (varFGrp‘𝐼)    &   ⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑈:𝐼⟶𝑋)
Theorem	vrgpinv 19666	The inverse of a generating element is represented by ⟨𝐴, 1⟩ instead of ⟨𝐴, 0⟩. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑈 = (varFGrp‘𝐼)    &   ⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) → (𝑁‘(𝑈‘𝐴)) = [⟨“⟨𝐴, 1o⟩”⟩] ∼ )
Theorem	frgpuptf 19667*	Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝐵 = (Base‘𝐻)    &   ⊢ 𝑁 = (invg‘𝐻)    &   ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))))    &   ⊢ (𝜑 → 𝐻 ∈ Grp)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐼⟶𝐵)    ⇒   ⊢ (𝜑 → 𝑇:(𝐼 × 2o)⟶𝐵)
Theorem	frgpuptinv 19668*	Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝐵 = (Base‘𝐻)    &   ⊢ 𝑁 = (invg‘𝐻)    &   ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))))    &   ⊢ (𝜑 → 𝐻 ∈ Grp)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐼⟶𝐵)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐼 × 2o)) → (𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴)))
Theorem	frgpuplem 19669*	Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝐵 = (Base‘𝐻)    &   ⊢ 𝑁 = (invg‘𝐻)    &   ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))))    &   ⊢ (𝜑 → 𝐻 ∈ Grp)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐼⟶𝐵)    &   ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∼ 𝐶) → (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶)))
Theorem	frgpupf 19670*	Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝐵 = (Base‘𝐻)    &   ⊢ 𝑁 = (invg‘𝐻)    &   ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))))    &   ⊢ (𝜑 → 𝐻 ∈ Grp)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐼⟶𝐵)    &   ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ ⟨[𝑔] ∼ , (𝐻 Σg (𝑇 ∘ 𝑔))⟩)    ⇒   ⊢ (𝜑 → 𝐸:𝑋⟶𝐵)
Theorem	frgpupval 19671*	Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝐵 = (Base‘𝐻)    &   ⊢ 𝑁 = (invg‘𝐻)    &   ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))))    &   ⊢ (𝜑 → 𝐻 ∈ Grp)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐼⟶𝐵)    &   ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ ⟨[𝑔] ∼ , (𝐻 Σg (𝑇 ∘ 𝑔))⟩)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑊) → (𝐸‘[𝐴] ∼ ) = (𝐻 Σg (𝑇 ∘ 𝐴)))
Theorem	frgpup1 19672*	Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)
⊢ 𝐵 = (Base‘𝐻)    &   ⊢ 𝑁 = (invg‘𝐻)    &   ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))))    &   ⊢ (𝜑 → 𝐻 ∈ Grp)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐼⟶𝐵)    &   ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ ⟨[𝑔] ∼ , (𝐻 Σg (𝑇 ∘ 𝑔))⟩)    ⇒   ⊢ (𝜑 → 𝐸 ∈ (𝐺 GrpHom 𝐻))
Theorem	frgpup2 19673*	The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)
⊢ 𝐵 = (Base‘𝐻)    &   ⊢ 𝑁 = (invg‘𝐻)    &   ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))))    &   ⊢ (𝜑 → 𝐻 ∈ Grp)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐼⟶𝐵)    &   ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ ⟨[𝑔] ∼ , (𝐻 Σg (𝑇 ∘ 𝑔))⟩)    &   ⊢ 𝑈 = (varFGrp‘𝐼)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝐸‘(𝑈‘𝐴)) = (𝐹‘𝐴))
Theorem	frgpup3lem 19674*	The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)
⊢ 𝐵 = (Base‘𝐻)    &   ⊢ 𝑁 = (invg‘𝐻)    &   ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))))    &   ⊢ (𝜑 → 𝐻 ∈ Grp)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐼⟶𝐵)    &   ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ ⟨[𝑔] ∼ , (𝐻 Σg (𝑇 ∘ 𝑔))⟩)    &   ⊢ 𝑈 = (varFGrp‘𝐼)    &   ⊢ (𝜑 → 𝐾 ∈ (𝐺 GrpHom 𝐻))    &   ⊢ (𝜑 → (𝐾 ∘ 𝑈) = 𝐹)    ⇒   ⊢ (𝜑 → 𝐾 = 𝐸)
Theorem	frgpup3 19675*	Universal property of the free monoid by existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)
⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐻)    &   ⊢ 𝑈 = (varFGrp‘𝐼)    ⇒   ⊢ ((𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝐵) → ∃!𝑚 ∈ (𝐺 GrpHom 𝐻)(𝑚 ∘ 𝑈) = 𝐹)
Theorem	0frgp 19676	The free group on zero generators is trivial. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐺 = (freeGrp‘∅)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ 𝐵 ≈ 1o
10.2.14  Abelian groups
10.2.14.1  Definition and basic properties
Syntax	ccmn 19677	Extend class notation with class of all commutative monoids.
class CMnd
Syntax	cabl 19678	Extend class notation with class of all Abelian groups.
class Abel
Definition	df-cmn 19679*	Define class of all commutative monoids. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ CMnd = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g‘𝑔)𝑏) = (𝑏(+g‘𝑔)𝑎)}
Definition	df-abl 19680	Define class of all Abelian groups. (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ Abel = (Grp ∩ CMnd)
Theorem	isabl 19681	The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.)
⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
Theorem	ablgrp 19682	An Abelian group is a group. (Contributed by NM, 26-Aug-2011.)
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)
Theorem	ablgrpd 19683	An Abelian group is a group, deduction form of ablgrp 19682. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Abel)    ⇒   ⊢ (𝜑 → 𝐺 ∈ Grp)
Theorem	ablcmn 19684	An Abelian group is a commutative monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ (𝐺 ∈ Abel → 𝐺 ∈ CMnd)
Theorem	ablcmnd 19685	An Abelian group is a commutative monoid. (Contributed by SN, 1-Jun-2024.)
⊢ (𝜑 → 𝐺 ∈ Abel)    ⇒   ⊢ (𝜑 → 𝐺 ∈ CMnd)
Theorem	iscmn 19686*	The predicate "is a commutative monoid". (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥)))
Theorem	isabl2 19687*	The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥)))
Theorem	cmnpropd 19688*	If two structures have the same group components (properties), one is a commutative monoid iff the other one is. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ CMnd ↔ 𝐿 ∈ CMnd))
Theorem	ablpropd 19689*	If two structures have the same group components (properties), one is an Abelian group iff the other one is. (Contributed by NM, 6-Dec-2014.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ Abel ↔ 𝐿 ∈ Abel))
Theorem	ablprop 19690	If two structures have the same group components (properties), one is an Abelian group iff the other one is. (Contributed by NM, 11-Oct-2013.)
⊢ (Base‘𝐾) = (Base‘𝐿)    &   ⊢ (+g‘𝐾) = (+g‘𝐿)    ⇒   ⊢ (𝐾 ∈ Abel ↔ 𝐿 ∈ Abel)
Theorem	iscmnd 19691*	Properties that determine a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥))    ⇒   ⊢ (𝜑 → 𝐺 ∈ CMnd)
Theorem	isabld 19692*	Properties that determine an Abelian group. (Contributed by NM, 6-Aug-2013.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥))    ⇒   ⊢ (𝜑 → 𝐺 ∈ Abel)
Theorem	isabli 19693*	Properties that determine an Abelian group. (Contributed by NM, 4-Sep-2011.)
⊢ 𝐺 ∈ Grp    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥))    ⇒   ⊢ 𝐺 ∈ Abel
Theorem	cmnmnd 19694	A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
Theorem	cmncom 19695	A commutative monoid is commutative. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ CMnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	ablcom 19696	An Abelian group operation is commutative. (Contributed by NM, 26-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	cmn32 19697	Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌))
Theorem	cmn4 19698	Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊)))
Theorem	cmn12 19699	Commutative/associative law for commutative monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 + (𝑌 + 𝑍)) = (𝑌 + (𝑋 + 𝑍)))
Theorem	abl32 19700	Commutative/associative law for Abelian groups. (Contributed by Stefan O'Rear, 10-Apr-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌))