P. 186 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18501-18600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	subgdisjb 18501	Vectors belonging to disjoint commuting subgroups are uniquely determined by their sum. Analogous to opth 5178, this theorem shows a way of representing a pair of vectors. (Contributed by NM, 5-Jul-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	pj1fval 18502*	The left projection function (for a direct product of group subspaces). (Contributed by Mario Carneiro, 15-Oct-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝑃 = (proj1‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) → (𝑇𝑃𝑈) = (𝑧 ∈ (𝑇 ⊕ 𝑈) ↦ (℩𝑥 ∈ 𝑇 ∃𝑦 ∈ 𝑈 𝑧 = (𝑥 + 𝑦))))
Theorem	pj1val 18503*	The left projection function (for a direct product of group subspaces). (Contributed by Mario Carneiro, 15-Oct-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝑃 = (proj1‘𝐺)    ⇒   ⊢ (((𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) → ((𝑇𝑃𝑈)‘𝑋) = (℩𝑥 ∈ 𝑇 ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦)))
Theorem	pj1eu 18504*	Uniqueness of a left projection. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) → ∃!𝑥 ∈ 𝑇 ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦))
Theorem	pj1f 18505	The left projection function maps a direct subspace sum onto the left factor. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    &   ⊢ 𝑃 = (proj1‘𝐺)    ⇒   ⊢ (𝜑 → (𝑇𝑃𝑈):(𝑇 ⊕ 𝑈)⟶𝑇)
Theorem	pj2f 18506	The right projection function maps a direct subspace sum onto the right factor. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    &   ⊢ 𝑃 = (proj1‘𝐺)    ⇒   ⊢ (𝜑 → (𝑈𝑃𝑇):(𝑇 ⊕ 𝑈)⟶𝑈)
Theorem	pj1id 18507	Any element of a direct subspace sum can be decomposed into projections onto the left and right factors. (Contributed by Mario Carneiro, 15-Oct-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    &   ⊢ 𝑃 = (proj1‘𝐺)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) → 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + ((𝑈𝑃𝑇)‘𝑋)))
Theorem	pj1eq 18508	Any element of a direct subspace sum can be decomposed uniquely into projections onto the left and right factors. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    &   ⊢ 𝑃 = (proj1‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑇 ⊕ 𝑈))    &   ⊢ (𝜑 → 𝐵 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑋 = (𝐵 + 𝐶) ↔ (((𝑇𝑃𝑈)‘𝑋) = 𝐵 ∧ ((𝑈𝑃𝑇)‘𝑋) = 𝐶)))
Theorem	pj1lid 18509	The left projection function is the identity on the left subspace. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    &   ⊢ 𝑃 = (proj1‘𝐺)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑇) → ((𝑇𝑃𝑈)‘𝑋) = 𝑋)
Theorem	pj1rid 18510	The left projection function is the zero operator on the right subspace. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    &   ⊢ 𝑃 = (proj1‘𝐺)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → ((𝑇𝑃𝑈)‘𝑋) = 0 )
Theorem	pj1ghm 18511	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 𝐺))
Theorem	pj1ghm2 18512	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 18513	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.12  Free groups
Syntax	cefg 18514	Extend class notation with the free group equivalence relation.
class ~FG
Syntax	cfrgp 18515	Extend class notation with the free group construction.
class freeGrp
Syntax	cvrgp 18516	Extend class notation with free group injection.
class varFGrp
Definition	df-efg 18517*	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 18518	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 18517. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ freeGrp = (𝑖 ∈ V ↦ ((freeMnd‘(𝑖 × 2o)) /s ( ~FG ‘𝑖)))
Definition	df-vrgp 18519*	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 18520*	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 18521*	The formal inverse operation is an endofunction on the generating set. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    ⇒   ⊢ 𝑀:(𝐼 × 2o)⟶(𝐼 × 2o)
Theorem	efgmnvl 18522*	The inversion function on the generators is an involution. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    ⇒   ⊢ (𝐴 ∈ (𝐼 × 2o) → (𝑀‘(𝑀‘𝐴)) = 𝐴)
Theorem	efgrcl 18523	Lemma for efgval 18525. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    ⇒   ⊢ (𝐴 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o)))
Theorem	efglem 18524*	Lemma for efgval 18525. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    ⇒   ⊢ ∃𝑟(𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩))
Theorem	efgval 18525*	Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    ⇒   ⊢ ∼ = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩))}
Theorem	efger 18526	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 18527	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 18528	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 18529	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 18530*	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 18531*	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 18532*	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 18533*	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 18534*	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 18535*	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 18536*	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 18537*	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 18538*	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 18539*	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 18540*	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 18541*	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 18542*	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 18543*	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 18544*	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 18545*	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 18546*	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	efgsresOLD 18547*	Obsolete proof of efgsres 18546 as of 12-Oct-2022. (Contributed by Mario Carneiro, 1-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    &   ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))    &   ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))    ⇒   ⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → (𝐹 ↾ (0..^𝑁)) ∈ dom 𝑆)
Theorem	efgsfo 18548*	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 18549*	The reduced word that forms the base of the sequence in efgsval 18539 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 18550*	Lemma for efgredleme 18552. (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 18551*	Lemma for efgred 18558. (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 18552*	Lemma for efgred 18558. (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 18553*	The reduced word that forms the base of the sequence in efgsval 18539 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 18554*	The reduced word that forms the base of the sequence in efgsval 18539 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 18555*	The reduced word that forms the base of the sequence in efgsval 18539 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 18556*	The reduced word that forms the base of the sequence in efgsval 18539 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	efgredlemOLD 18557*	Obsolete proof of efgredlem 18556 as of 12-Oct-2022. (Contributed by Mario Carneiro, 30-Sep-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑊 = ( 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 18558*	The reduced word that forms the base of the sequence in efgsval 18539 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 18559*	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 18560*	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 18561*	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 18562*	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 18563*	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 18564*	Lemma for efgrelex 18561. 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 18565*	Lemma for efgrelex 18561. 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 18566*	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 18567*	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 18568	Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ 𝑀 = (freeMnd‘(𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐺 = (𝑀 /s ∼ ))
Theorem	frgpcpbl 18569	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 18570	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 18571	Closure of the quotient map in a free group. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑊 → [𝑋] ∼ ∈ 𝐵)
Theorem	frgpgrp 18572	The free group is a group. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝐺 = (freeGrp‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐺 ∈ Grp)
Theorem	frgpadd 18573	Addition in the free group is given by concatenation. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ([𝐴] ∼ + [𝐵] ∼ ) = [(𝐴 ++ 𝐵)] ∼ )
Theorem	frgpinv 18574*	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 18575*	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 18576*	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 18577	The value of the generating elements of a free group. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑈 = (varFGrp‘𝐼)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) → (𝑈‘𝐴) = [⟨“⟨𝐴, ∅⟩”⟩] ∼ )
Theorem	vrgpf 18578	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 18579	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 18580*	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 18581*	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 18582*	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 18583*	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 18584*	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 18585*	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 18586*	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 18587*	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 18588*	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 18589	The free group on zero generators is trivial. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐺 = (freeGrp‘∅)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ 𝐵 ≈ 1o
10.3  Abelian groups
10.3.1  Definition and basic properties
Syntax	ccmn 18590	Extend class notation with class of all commutative monoids.
class CMnd
Syntax	cabl 18591	Extend class notation with class of all Abelian groups.
class Abel
Definition	df-cmn 18592*	Define class of all commutative monoids. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ CMnd = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g‘𝑔)𝑏) = (𝑏(+g‘𝑔)𝑎)}
Definition	df-abl 18593	Define class of all Abelian groups. (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ Abel = (Grp ∩ CMnd)
Theorem	isabl 18594	The predicate "is an Abelian (commutative) group." (Contributed by NM, 17-Oct-2011.)
⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
Theorem	ablgrp 18595	An Abelian group is a group. (Contributed by NM, 26-Aug-2011.)
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)
Theorem	ablcmn 18596	An Abelian group is a commutative monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ (𝐺 ∈ Abel → 𝐺 ∈ CMnd)
Theorem	iscmn 18597*	The predicate "is a commutative monoid." (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥)))
Theorem	isabl2 18598*	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 18599*	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 18600*	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))