P. 199 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19801-19900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	efgsdm 19801*	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 19802*	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 19803*	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 19804*	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 19805*	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 19806*	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 19807*	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 19808*	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 19809*	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 19810*	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 19811*	The reduced word that forms the base of the sequence in efgsval 19802 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 19812*	Lemma for efgredleme 19814. (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 19813*	Lemma for efgred 19819. (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 19814*	Lemma for efgred 19819. (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 19815*	The reduced word that forms the base of the sequence in efgsval 19802 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 19816*	The reduced word that forms the base of the sequence in efgsval 19802 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 19817*	The reduced word that forms the base of the sequence in efgsval 19802 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 19818*	The reduced word that forms the base of the sequence in efgsval 19802 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 19819*	The reduced word that forms the base of the sequence in efgsval 19802 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 19820*	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 19821*	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 19822*	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 19823*	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 19824*	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 19825*	Lemma for efgrelex 19822. 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 19826*	Lemma for efgrelex 19822. 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 19827*	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 19828*	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 19829	Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ 𝑀 = (freeMnd‘(𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐺 = (𝑀 /s ∼ ))
Theorem	frgpcpbl 19830	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 19831	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 19832	Closure of the quotient map in a free group. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑊 → [𝑋] ∼ ∈ 𝐵)
Theorem	frgpgrp 19833	The free group is a group. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝐺 = (freeGrp‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐺 ∈ Grp)
Theorem	frgpadd 19834	Addition in the free group is given by concatenation. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ 𝐺 = (freeGrp‘𝐼)    &   ⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ([𝐴] ∼ + [𝐵] ∼ ) = [(𝐴 ++ 𝐵)] ∼ )
Theorem	frgpinv 19835*	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 19836*	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 19837*	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 19838	The value of the generating elements of a free group. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ ∼ = ( ~FG ‘𝐼)    &   ⊢ 𝑈 = (varFGrp‘𝐼)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) → (𝑈‘𝐴) = [⟨“⟨𝐴, ∅⟩”⟩] ∼ )
Theorem	vrgpf 19839	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 19840	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 19841*	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 19842*	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 19843*	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 19844*	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 19845*	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 19846*	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 19847*	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 19848*	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 19849*	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 19850	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 19851	Extend class notation with class of all commutative monoids.
class CMnd
Syntax	cabl 19852	Extend class notation with class of all Abelian groups.
class Abel
Definition	df-cmn 19853*	Define class of all commutative monoids. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ CMnd = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g‘𝑔)𝑏) = (𝑏(+g‘𝑔)𝑎)}
Definition	df-abl 19854	Define class of all Abelian groups. (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ Abel = (Grp ∩ CMnd)
Theorem	isabl 19855	The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.)
⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
Theorem	ablgrp 19856	An Abelian group is a group. (Contributed by NM, 26-Aug-2011.)
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)
Theorem	ablgrpd 19857	An Abelian group is a group, deduction form of ablgrp 19856. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Abel)    ⇒   ⊢ (𝜑 → 𝐺 ∈ Grp)
Theorem	ablcmn 19858	An Abelian group is a commutative monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ (𝐺 ∈ Abel → 𝐺 ∈ CMnd)
Theorem	ablcmnd 19859	An Abelian group is a commutative monoid. (Contributed by SN, 1-Jun-2024.)
⊢ (𝜑 → 𝐺 ∈ Abel)    ⇒   ⊢ (𝜑 → 𝐺 ∈ CMnd)
Theorem	iscmn 19860*	The predicate "is a commutative monoid". (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥)))
Theorem	isabl2 19861*	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 19862*	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 19863*	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 19864	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 19865*	Properties that determine a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥))    ⇒   ⊢ (𝜑 → 𝐺 ∈ CMnd)
Theorem	isabld 19866*	Properties that determine an Abelian group. (Contributed by NM, 6-Aug-2013.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥))    ⇒   ⊢ (𝜑 → 𝐺 ∈ Abel)
Theorem	isabli 19867*	Properties that determine an Abelian group. (Contributed by NM, 4-Sep-2011.)
⊢ 𝐺 ∈ Grp    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥))    ⇒   ⊢ 𝐺 ∈ Abel
Theorem	cmnmnd 19868	A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
Theorem	cmncom 19869	A commutative monoid is commutative. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ CMnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	ablcom 19870	An Abelian group operation is commutative. (Contributed by NM, 26-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	cmn32 19871	Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌))
Theorem	cmn4 19872	Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊)))
Theorem	cmn12 19873	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 19874	Commutative/associative law for Abelian groups. (Contributed by Stefan O'Rear, 10-Apr-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌))
Theorem	cmnmndd 19875	A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024.)
⊢ (𝜑 → 𝐺 ∈ CMnd)    ⇒   ⊢ (𝜑 → 𝐺 ∈ Mnd)
Theorem	cmnbascntr 19876	The base set of a commutative monoid is its center. (Contributed by SN, 21-Mar-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑍 = (Cntr‘𝐺)    ⇒   ⊢ (𝐺 ∈ CMnd → 𝐵 = 𝑍)
Theorem	rinvmod 19877*	Uniqueness of a right inverse element in a commutative monoid, if it exists. Corresponds to caovmo 7649. (Contributed by AV, 31-Dec-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ CMnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃*𝑤 ∈ 𝐵 (𝐴 + 𝑤) = 0 )
Theorem	ablinvadd 19878	The inverse of an Abelian group operation. (Contributed by NM, 31-Mar-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑁‘(𝑋 + 𝑌)) = ((𝑁‘𝑋) + (𝑁‘𝑌)))
Theorem	ablsub2inv 19879	Abelian group subtraction of two inverses. (Contributed by Stefan O'Rear, 24-May-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑁‘𝑋) − (𝑁‘𝑌)) = (𝑌 − 𝑋))
Theorem	ablsubadd 19880	Relationship between Abelian group subtraction and addition. (Contributed by NM, 31-Mar-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) = 𝑍 ↔ (𝑌 + 𝑍) = 𝑋))
Theorem	ablsub4 19881	Commutative/associative subtraction law for Abelian groups. (Contributed by NM, 31-Mar-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 + 𝑌) − (𝑍 + 𝑊)) = ((𝑋 − 𝑍) + (𝑌 − 𝑊)))
Theorem	abladdsub4 19882	Abelian group addition/subtraction law. (Contributed by NM, 31-Mar-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 + 𝑌) = (𝑍 + 𝑊) ↔ (𝑋 − 𝑍) = (𝑊 − 𝑌)))
Theorem	abladdsub 19883	Associative-type law for group subtraction and addition. (Contributed by NM, 19-Apr-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) − 𝑍) = ((𝑋 − 𝑍) + 𝑌))
Theorem	ablsubadd23 19884	Commutative/associative law for addition and subtraction in abelian groups. (subadd23d 11592 analog.) (Contributed by AV, 2-Mar-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) + 𝑍) = (𝑋 + (𝑍 − 𝑌)))
Theorem	ablsubaddsub 19885	Double subtraction and addition in abelian groups. (cnambpcma 48014 analog.) (Contributed by AV, 3-Mar-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((𝑋 − 𝑌) + 𝑍) − 𝑋) = (𝑍 − 𝑌))
Theorem	ablpncan2 19886	Cancellation law for subtraction in an Abelian group. (Contributed by NM, 2-Oct-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 + 𝑌) − 𝑋) = 𝑌)
Theorem	ablpncan3 19887	A cancellation law for Abelian groups. (Contributed by NM, 23-Mar-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 + (𝑌 − 𝑋)) = 𝑌)
Theorem	ablsubsub 19888	Law for double subtraction. (Contributed by NM, 7-Apr-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 − (𝑌 − 𝑍)) = ((𝑋 − 𝑌) + 𝑍))
Theorem	ablsubsub4 19889	Law for double subtraction. (Contributed by NM, 7-Apr-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 − 𝑌) − 𝑍) = (𝑋 − (𝑌 + 𝑍)))
Theorem	ablpnpcan 19890	Cancellation law for mixed addition and subtraction. (pnpcan 11498 analog.) (Contributed by NM, 29-May-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) − (𝑋 + 𝑍)) = (𝑌 − 𝑍))
Theorem	ablnncan 19891	Cancellation law for group subtraction. (nncan 11488 analog.) (Contributed by NM, 7-Apr-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 − (𝑋 − 𝑌)) = 𝑌)
Theorem	ablsub32 19892	Swap the second and third terms in a double group subtraction. (Contributed by NM, 7-Apr-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 − 𝑌) − 𝑍) = ((𝑋 − 𝑍) − 𝑌))
Theorem	ablnnncan 19893	Cancellation law for group subtraction. (nnncan 11494 analog.) (Contributed by NM, 29-Feb-2008.) (Revised by AV, 27-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 − (𝑌 − 𝑍)) − 𝑍) = (𝑋 − 𝑌))
Theorem	ablnnncan1 19894	Cancellation law for group subtraction. (nnncan1 11495 analog.) (Contributed by NM, 7-Apr-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Abel)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 − 𝑌) − (𝑋 − 𝑍)) = (𝑍 − 𝑌))
Theorem	ablsubsub23 19895	Swap subtrahend and result of group subtraction. (Contributed by NM, 14-Dec-2007.) (Revised by AV, 7-Oct-2021.)
⊢ 𝑉 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Abel ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵))
Theorem	mulgnn0di 19896	Group multiple of a sum, for nonnegative multiples. (Contributed by Mario Carneiro, 13-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑀 · (𝑋 + 𝑌)) = ((𝑀 · 𝑋) + (𝑀 · 𝑌)))
Theorem	mulgdi 19897	Group multiple of a sum. (Contributed by Mario Carneiro, 13-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Abel ∧ (𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑀 · (𝑋 + 𝑌)) = ((𝑀 · 𝑋) + (𝑀 · 𝑌)))
Theorem	mulgmhm 19898*	The map from 𝑥 to 𝑛𝑥 for a fixed positive integer 𝑛 is a monoid homomorphism if the monoid is commutative. (Contributed by Mario Carneiro, 4-May-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0) → (𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥)) ∈ (𝐺 MndHom 𝐺))
Theorem	mulgghm 19899*	The map from 𝑥 to 𝑛𝑥 for a fixed integer 𝑛 is a group homomorphism if the group is commutative. (Contributed by Mario Carneiro, 4-May-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Abel ∧ 𝑀 ∈ ℤ) → (𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥)) ∈ (𝐺 GrpHom 𝐺))
Theorem	mulgsubdi 19900	Group multiple of a difference. (Contributed by Mario Carneiro, 13-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Abel ∧ (𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑀 · (𝑋 − 𝑌)) = ((𝑀 · 𝑋) − (𝑀 · 𝑌)))