Home | Metamath
Proof Explorer Theorem List (p. 182 of 426) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lsmdisj2b 18101 | Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝜑 → ((((𝑆 ⊕ 𝑈) ∩ 𝑇) = { 0 } ∧ (𝑆 ∩ 𝑈) = { 0 }) ↔ ((𝑆 ∩ (𝑇 ⊕ 𝑈)) = { 0 } ∧ (𝑇 ∩ 𝑈) = { 0 }))) | ||
Theorem | lsmdisj3a 18102 | Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝑆 ⊆ (𝑍‘𝑇)) ⇒ ⊢ (𝜑 → ((((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 } ∧ (𝑆 ∩ 𝑇) = { 0 }) ↔ ((𝑆 ∩ (𝑇 ⊕ 𝑈)) = { 0 } ∧ (𝑇 ∩ 𝑈) = { 0 }))) | ||
Theorem | lsmdisj3b 18103 | Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈)) ⇒ ⊢ (𝜑 → ((((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 } ∧ (𝑆 ∩ 𝑇) = { 0 }) ↔ ((𝑆 ∩ (𝑇 ⊕ 𝑈)) = { 0 } ∧ (𝑇 ∩ 𝑈) = { 0 }))) | ||
Theorem | subgdisj1 18104 | Vectors belonging to disjoint commuting subgroups are uniquely determined by their sum. (Contributed by NM, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 }) & ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈)) & ⊢ (𝜑 → 𝐴 ∈ 𝑇) & ⊢ (𝜑 → 𝐶 ∈ 𝑇) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) & ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐶 + 𝐷)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐶) | ||
Theorem | subgdisj2 18105 | Vectors belonging to disjoint commuting subgroups are uniquely determined by their sum. (Contributed by NM, 12-Jul-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 }) & ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈)) & ⊢ (𝜑 → 𝐴 ∈ 𝑇) & ⊢ (𝜑 → 𝐶 ∈ 𝑇) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑈) & ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐶 + 𝐷)) ⇒ ⊢ (𝜑 → 𝐵 = 𝐷) | ||
Theorem | subgdisjb 18106 | Vectors belonging to disjoint commuting subgroups are uniquely determined by their sum. Analogous to opth 4945, 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 18107* | 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 18108* | 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 18109* | Uniqueness of a left projection. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 }) & ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) → ∃!𝑥 ∈ 𝑇 ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦)) | ||
Theorem | pj1f 18110 | 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 18111 | 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 18112 | 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 18113 | 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 18114 | 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 18115 | 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 18116 | 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 18117 | 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 18118 | The order of the direct product of groups. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 }) & ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈)) & ⊢ (𝜑 → 𝑇 ∈ Fin) & ⊢ (𝜑 → 𝑈 ∈ Fin) ⇒ ⊢ (𝜑 → (#‘(𝑇 ⊕ 𝑈)) = ((#‘𝑇) · (#‘𝑈))) | ||
Syntax | cefg 18119 | Extend class notation with the free group equivalence relation. |
class ~FG | ||
Syntax | cfrgp 18120 | Extend class notation with the free group construction. |
class freeGrp | ||
Syntax | cvrgp 18121 | Extend class notation with free group injection. |
class varFGrp | ||
Definition | df-efg 18122* | 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 (𝑖 × 2𝑜) ∧ ∀𝑥 ∈ Word (𝑖 × 2𝑜)∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))}) | ||
Definition | df-frgp 18123 | Define the free group on a set 𝐼 of generators, defined as the quotient of the free monoid on 𝐼 × 2𝑜 (representing the generator elements and their formal inverses) by the free group equivalence relation df-efg 18122. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ freeGrp = (𝑖 ∈ V ↦ ((freeMnd‘(𝑖 × 2𝑜)) /s ( ~FG ‘𝑖))) | ||
Definition | df-vrgp 18124* | 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 18125* | Value of the formal inverse operation for the generating set of a free group. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) ⇒ ⊢ ((𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 2𝑜) → (𝐴𝑀𝐵) = 〈𝐴, (1𝑜 ∖ 𝐵)〉) | ||
Theorem | efgmf 18126* | The formal inverse operation is an endofunction on the generating set. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) ⇒ ⊢ 𝑀:(𝐼 × 2𝑜)⟶(𝐼 × 2𝑜) | ||
Theorem | efgmnvl 18127* | The inversion function on the generators is an involution. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) ⇒ ⊢ (𝐴 ∈ (𝐼 × 2𝑜) → (𝑀‘(𝑀‘𝐴)) = 𝐴) | ||
Theorem | efgrcl 18128 | Lemma for efgval 18130. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) ⇒ ⊢ (𝐴 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2𝑜))) | ||
Theorem | efglem 18129* | Lemma for efgval 18130. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) ⇒ ⊢ ∃𝑟(𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉)) | ||
Theorem | efgval 18130* | Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) ⇒ ⊢ ∼ = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(#‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2𝑜 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1𝑜 ∖ 𝑧)〉”〉〉))} | ||
Theorem | efger 18131 | Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) ⇒ ⊢ ∼ Er 𝑊 | ||
Theorem | efgi 18132 | Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) ⇒ ⊢ (((𝐴 ∈ 𝑊 ∧ 𝑁 ∈ (0...(#‘𝐴))) ∧ (𝐽 ∈ 𝐼 ∧ 𝐾 ∈ 2𝑜)) → 𝐴 ∼ (𝐴 splice 〈𝑁, 𝑁, 〈“〈𝐽, 𝐾〉〈𝐽, (1𝑜 ∖ 𝐾)〉”〉〉)) | ||
Theorem | efgi0 18133 | Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) ⇒ ⊢ ((𝐴 ∈ 𝑊 ∧ 𝑁 ∈ (0...(#‘𝐴)) ∧ 𝐽 ∈ 𝐼) → 𝐴 ∼ (𝐴 splice 〈𝑁, 𝑁, 〈“〈𝐽, ∅〉〈𝐽, 1𝑜〉”〉〉)) | ||
Theorem | efgi1 18134 | Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) ⇒ ⊢ ((𝐴 ∈ 𝑊 ∧ 𝑁 ∈ (0...(#‘𝐴)) ∧ 𝐽 ∈ 𝐼) → 𝐴 ∼ (𝐴 splice 〈𝑁, 𝑁, 〈“〈𝐽, 1𝑜〉〈𝐽, ∅〉”〉〉)) | ||
Theorem | efgtf 18135* | Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) ⇒ ⊢ (𝑋 ∈ 𝑊 → ((𝑇‘𝑋) = (𝑎 ∈ (0...(#‘𝑋)), 𝑏 ∈ (𝐼 × 2𝑜) ↦ (𝑋 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) ∧ (𝑇‘𝑋):((0...(#‘𝑋)) × (𝐼 × 2𝑜))⟶𝑊)) | ||
Theorem | efgtval 18136* | 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 (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) ⇒ ⊢ ((𝑋 ∈ 𝑊 ∧ 𝑁 ∈ (0...(#‘𝑋)) ∧ 𝐴 ∈ (𝐼 × 2𝑜)) → (𝑁(𝑇‘𝑋)𝐴) = (𝑋 splice 〈𝑁, 𝑁, 〈“𝐴(𝑀‘𝐴)”〉〉)) | ||
Theorem | efgval2 18137* | Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) ⇒ ⊢ ∼ = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ran (𝑇‘𝑥) ⊆ [𝑥]𝑟)} | ||
Theorem | efgi2 18138* | Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) ⇒ ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ ran (𝑇‘𝐴)) → 𝐴 ∼ 𝐵) | ||
Theorem | efgtlen 18139* | Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) ⇒ ⊢ ((𝑋 ∈ 𝑊 ∧ 𝐴 ∈ ran (𝑇‘𝑋)) → (#‘𝐴) = ((#‘𝑋) + 2)) | ||
Theorem | efginvrel2 18140* | 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 (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) ⇒ ⊢ (𝐴 ∈ 𝑊 → (𝐴 ++ (𝑀 ∘ (reverse‘𝐴))) ∼ ∅) | ||
Theorem | efginvrel1 18141* | 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 (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) ⇒ ⊢ (𝐴 ∈ 𝑊 → ((𝑀 ∘ (reverse‘𝐴)) ++ 𝐴) ∼ ∅) | ||
Theorem | efgsf 18142* | Value of the auxiliary function 𝑆 defining a sequence of extensions starting at some irreducible word. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) ⇒ ⊢ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊 | ||
Theorem | efgsdm 18143* | 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 (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) ⇒ ⊢ (𝐹 ∈ dom 𝑆 ↔ (𝐹 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐹‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(#‘𝐹))(𝐹‘𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1))))) | ||
Theorem | efgsval 18144* | Value of the auxiliary function 𝑆 defining a sequence of extensions. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) ⇒ ⊢ (𝐹 ∈ dom 𝑆 → (𝑆‘𝐹) = (𝐹‘((#‘𝐹) − 1))) | ||
Theorem | efgsdmi 18145* | Property of the last link in the chain of extensions. (Contributed by Mario Carneiro, 29-Sep-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) ⇒ ⊢ ((𝐹 ∈ dom 𝑆 ∧ ((#‘𝐹) − 1) ∈ ℕ) → (𝑆‘𝐹) ∈ ran (𝑇‘(𝐹‘(((#‘𝐹) − 1) − 1)))) | ||
Theorem | efgsval2 18146* | Value of the auxiliary function 𝑆 defining a sequence of extensions. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) ⇒ ⊢ ((𝐴 ∈ Word 𝑊 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ++ 〈“𝐵”〉) ∈ dom 𝑆) → (𝑆‘(𝐴 ++ 〈“𝐵”〉)) = 𝐵) | ||
Theorem | efgsrel 18147* | 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 (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) ⇒ ⊢ (𝐹 ∈ dom 𝑆 → (𝐹‘0) ∼ (𝑆‘𝐹)) | ||
Theorem | efgs1 18148* | A singleton of an irreducible word is an extension sequence. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) ⇒ ⊢ (𝐴 ∈ 𝐷 → 〈“𝐴”〉 ∈ dom 𝑆) | ||
Theorem | efgs1b 18149* | Every extension sequence ending in an irreducible word is trivial. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) ⇒ ⊢ (𝐴 ∈ dom 𝑆 → ((𝑆‘𝐴) ∈ 𝐷 ↔ (#‘𝐴) = 1)) | ||
Theorem | efgsp1 18150* | 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 (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) ⇒ ⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (𝐹 ++ 〈“𝐴”〉) ∈ dom 𝑆) | ||
Theorem | efgsres 18151* | An initial segment of an extension sequence is an extension sequence. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) ⇒ ⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(#‘𝐹))) → (𝐹 ↾ (0..^𝑁)) ∈ dom 𝑆) | ||
Theorem | efgsfo 18152* | 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 indexes somewhere in the sequence). (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) ⇒ ⊢ 𝑆:dom 𝑆–onto→𝑊 | ||
Theorem | efgredlema 18153* | The reduced word that forms the base of the sequence in efgsval 18144 is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) & ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑆) & ⊢ (𝜑 → 𝐵 ∈ dom 𝑆) & ⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵)) & ⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0)) ⇒ ⊢ (𝜑 → (((#‘𝐴) − 1) ∈ ℕ ∧ ((#‘𝐵) − 1) ∈ ℕ)) | ||
Theorem | efgredlemf 18154* | Lemma for efgredleme 18156. (Contributed by Mario Carneiro, 4-Jun-2016.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) & ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑆) & ⊢ (𝜑 → 𝐵 ∈ dom 𝑆) & ⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵)) & ⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0)) & ⊢ 𝐾 = (((#‘𝐴) − 1) − 1) & ⊢ 𝐿 = (((#‘𝐵) − 1) − 1) ⇒ ⊢ (𝜑 → ((𝐴‘𝐾) ∈ 𝑊 ∧ (𝐵‘𝐿) ∈ 𝑊)) | ||
Theorem | efgredlemg 18155* | Lemma for efgred 18161. (Contributed by Mario Carneiro, 4-Jun-2016.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) & ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑆) & ⊢ (𝜑 → 𝐵 ∈ dom 𝑆) & ⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵)) & ⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0)) & ⊢ 𝐾 = (((#‘𝐴) − 1) − 1) & ⊢ 𝐿 = (((#‘𝐵) − 1) − 1) & ⊢ (𝜑 → 𝑃 ∈ (0...(#‘(𝐴‘𝐾)))) & ⊢ (𝜑 → 𝑄 ∈ (0...(#‘(𝐵‘𝐿)))) & ⊢ (𝜑 → 𝑈 ∈ (𝐼 × 2𝑜)) & ⊢ (𝜑 → 𝑉 ∈ (𝐼 × 2𝑜)) & ⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈)) & ⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉)) ⇒ ⊢ (𝜑 → (#‘(𝐴‘𝐾)) = (#‘(𝐵‘𝐿))) | ||
Theorem | efgredleme 18156* | Lemma for efgred 18161. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) & ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑆) & ⊢ (𝜑 → 𝐵 ∈ dom 𝑆) & ⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵)) & ⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0)) & ⊢ 𝐾 = (((#‘𝐴) − 1) − 1) & ⊢ 𝐿 = (((#‘𝐵) − 1) − 1) & ⊢ (𝜑 → 𝑃 ∈ (0...(#‘(𝐴‘𝐾)))) & ⊢ (𝜑 → 𝑄 ∈ (0...(#‘(𝐵‘𝐿)))) & ⊢ (𝜑 → 𝑈 ∈ (𝐼 × 2𝑜)) & ⊢ (𝜑 → 𝑉 ∈ (𝐼 × 2𝑜)) & ⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈)) & ⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉)) & ⊢ (𝜑 → ¬ (𝐴‘𝐾) = (𝐵‘𝐿)) & ⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) & ⊢ (𝜑 → 𝐶 ∈ dom 𝑆) & ⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉))) ⇒ ⊢ (𝜑 → ((𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶)) ∧ (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶)))) | ||
Theorem | efgredlemd 18157* | The reduced word that forms the base of the sequence in efgsval 18144 is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) & ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑆) & ⊢ (𝜑 → 𝐵 ∈ dom 𝑆) & ⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵)) & ⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0)) & ⊢ 𝐾 = (((#‘𝐴) − 1) − 1) & ⊢ 𝐿 = (((#‘𝐵) − 1) − 1) & ⊢ (𝜑 → 𝑃 ∈ (0...(#‘(𝐴‘𝐾)))) & ⊢ (𝜑 → 𝑄 ∈ (0...(#‘(𝐵‘𝐿)))) & ⊢ (𝜑 → 𝑈 ∈ (𝐼 × 2𝑜)) & ⊢ (𝜑 → 𝑉 ∈ (𝐼 × 2𝑜)) & ⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈)) & ⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉)) & ⊢ (𝜑 → ¬ (𝐴‘𝐾) = (𝐵‘𝐿)) & ⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) & ⊢ (𝜑 → 𝐶 ∈ dom 𝑆) & ⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉))) ⇒ ⊢ (𝜑 → (𝐴‘0) = (𝐵‘0)) | ||
Theorem | efgredlemc 18158* | The reduced word that forms the base of the sequence in efgsval 18144 is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) & ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑆) & ⊢ (𝜑 → 𝐵 ∈ dom 𝑆) & ⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵)) & ⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0)) & ⊢ 𝐾 = (((#‘𝐴) − 1) − 1) & ⊢ 𝐿 = (((#‘𝐵) − 1) − 1) & ⊢ (𝜑 → 𝑃 ∈ (0...(#‘(𝐴‘𝐾)))) & ⊢ (𝜑 → 𝑄 ∈ (0...(#‘(𝐵‘𝐿)))) & ⊢ (𝜑 → 𝑈 ∈ (𝐼 × 2𝑜)) & ⊢ (𝜑 → 𝑉 ∈ (𝐼 × 2𝑜)) & ⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈)) & ⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉)) & ⊢ (𝜑 → ¬ (𝐴‘𝐾) = (𝐵‘𝐿)) ⇒ ⊢ (𝜑 → (𝑃 ∈ (ℤ≥‘𝑄) → (𝐴‘0) = (𝐵‘0))) | ||
Theorem | efgredlemb 18159* | The reduced word that forms the base of the sequence in efgsval 18144 is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 30-Sep-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) & ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑆) & ⊢ (𝜑 → 𝐵 ∈ dom 𝑆) & ⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵)) & ⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0)) & ⊢ 𝐾 = (((#‘𝐴) − 1) − 1) & ⊢ 𝐿 = (((#‘𝐵) − 1) − 1) & ⊢ (𝜑 → 𝑃 ∈ (0...(#‘(𝐴‘𝐾)))) & ⊢ (𝜑 → 𝑄 ∈ (0...(#‘(𝐵‘𝐿)))) & ⊢ (𝜑 → 𝑈 ∈ (𝐼 × 2𝑜)) & ⊢ (𝜑 → 𝑉 ∈ (𝐼 × 2𝑜)) & ⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈)) & ⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉)) & ⊢ (𝜑 → ¬ (𝐴‘𝐾) = (𝐵‘𝐿)) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | efgredlem 18160* | The reduced word that forms the base of the sequence in efgsval 18144 is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 30-Sep-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) & ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑆) & ⊢ (𝜑 → 𝐵 ∈ dom 𝑆) & ⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵)) & ⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0)) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | efgred 18161* | The reduced word that forms the base of the sequence in efgsval 18144 is uniquely determined, given the terminal point. (Contributed by Mario Carneiro, 28-Sep-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) ⇒ ⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆 ∧ (𝑆‘𝐴) = (𝑆‘𝐵)) → (𝐴‘0) = (𝐵‘0)) | ||
Theorem | efgrelexlema 18162* | 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 (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) & ⊢ 𝐿 = {〈𝑖, 𝑗〉 ∣ ∃𝑐 ∈ (◡𝑆 “ {𝑖})∃𝑑 ∈ (◡𝑆 “ {𝑗})(𝑐‘0) = (𝑑‘0)} ⇒ ⊢ (𝐴𝐿𝐵 ↔ ∃𝑎 ∈ (◡𝑆 “ {𝐴})∃𝑏 ∈ (◡𝑆 “ {𝐵})(𝑎‘0) = (𝑏‘0)) | ||
Theorem | efgrelexlemb 18163* | 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 (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) & ⊢ 𝐿 = {〈𝑖, 𝑗〉 ∣ ∃𝑐 ∈ (◡𝑆 “ {𝑖})∃𝑑 ∈ (◡𝑆 “ {𝑗})(𝑐‘0) = (𝑑‘0)} ⇒ ⊢ ∼ ⊆ 𝐿 | ||
Theorem | efgrelex 18164* | 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 (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) ⇒ ⊢ (𝐴 ∼ 𝐵 → ∃𝑎 ∈ (◡𝑆 “ {𝐴})∃𝑏 ∈ (◡𝑆 “ {𝐵})(𝑎‘0) = (𝑏‘0)) | ||
Theorem | efgredeu 18165* | There is a unique reduced word equivalent to a given word. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) ⇒ ⊢ (𝐴 ∈ 𝑊 → ∃!𝑑 ∈ 𝐷 𝑑 ∼ 𝐴) | ||
Theorem | efgred2 18166* | Two extension sequences have related endpoints iff they have the same base. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) ⇒ ⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆) → ((𝑆‘𝐴) ∼ (𝑆‘𝐵) ↔ (𝐴‘0) = (𝐵‘0))) | ||
Theorem | efgcpbllema 18167* | Lemma for efgrelex 18164. 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 (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) & ⊢ 𝐿 = {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝑊 ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ∼ ((𝐴 ++ 𝑗) ++ 𝐵))} ⇒ ⊢ (𝑋𝐿𝑌 ↔ (𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑊 ∧ ((𝐴 ++ 𝑋) ++ 𝐵) ∼ ((𝐴 ++ 𝑌) ++ 𝐵))) | ||
Theorem | efgcpbllemb 18168* | Lemma for efgrelex 18164. 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 (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) & ⊢ 𝐿 = {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝑊 ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ∼ ((𝐴 ++ 𝑗) ++ 𝐵))} ⇒ ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∼ ⊆ 𝐿) | ||
Theorem | efgcpbl 18169* | Two extension sequences have related endpoints iff they have the same base. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) ⇒ ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ∧ 𝑋 ∼ 𝑌) → ((𝐴 ++ 𝑋) ++ 𝐵) ∼ ((𝐴 ++ 𝑌) ++ 𝐵)) | ||
Theorem | efgcpbl2 18170* | Two extension sequences have related endpoints iff they have the same base. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) ⇒ ⊢ ((𝐴 ∼ 𝑋 ∧ 𝐵 ∼ 𝑌) → (𝐴 ++ 𝐵) ∼ (𝑋 ++ 𝑌)) | ||
Theorem | frgpval 18171 | Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑀 = (freeMnd‘(𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐺 = (𝑀 /s ∼ )) | ||
Theorem | frgpcpbl 18172 | 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‘(𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ + = (+g‘𝑀) ⇒ ⊢ ((𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷) → (𝐴 + 𝐵) ∼ (𝐶 + 𝐷)) | ||
Theorem | frgp0 18173 | 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 18174 | Closure of the quotient map in a free group. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝑊 → [𝑋] ∼ ∈ 𝐵) | ||
Theorem | frgpgrp 18175 | The free group is a group. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝐺 = (freeGrp‘𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐺 ∈ Grp) | ||
Theorem | frgpadd 18176 | Addition in the free group is given by concatenation. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ([𝐴] ∼ + [𝐵] ∼ ) = [(𝐴 ++ 𝐵)] ∼ ) | ||
Theorem | frgpinv 18177* | The inverse of an element of the free group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) ⇒ ⊢ (𝐴 ∈ 𝑊 → (𝑁‘[𝐴] ∼ ) = [(𝑀 ∘ (reverse‘𝐴))] ∼ ) | ||
Theorem | frgpmhm 18178* | 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‘(𝐼 × 2𝑜)) & ⊢ 𝑊 = (Base‘𝑀) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝐹 = (𝑥 ∈ 𝑊 ↦ [𝑥] ∼ ) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐹 ∈ (𝑀 MndHom 𝐺)) | ||
Theorem | vrgpfval 18179* | 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 18180 | The value of the generating elements of a free group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑈 = (varFGrp‘𝐼) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) → (𝑈‘𝐴) = [〈“〈𝐴, ∅〉”〉] ∼ ) | ||
Theorem | vrgpf 18181 | 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 18182 | The inverse of a generating element is represented by 〈𝐴, 1〉 instead of 〈𝐴, 0〉. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑈 = (varFGrp‘𝐼) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) → (𝑁‘(𝑈‘𝐴)) = [〈“〈𝐴, 1𝑜〉”〉] ∼ ) | ||
Theorem | frgpuptf 18183* | 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‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) ⇒ ⊢ (𝜑 → 𝑇:(𝐼 × 2𝑜)⟶𝐵) | ||
Theorem | frgpuptinv 18184* | 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‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ 〈𝑦, (1𝑜 ∖ 𝑧)〉) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐼 × 2𝑜)) → (𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴))) | ||
Theorem | frgpuplem 18185* | 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‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∼ 𝐶) → (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶))) | ||
Theorem | frgpupf 18186* | 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‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ 〈[𝑔] ∼ , (𝐻 Σg (𝑇 ∘ 𝑔))〉) ⇒ ⊢ (𝜑 → 𝐸:𝑋⟶𝐵) | ||
Theorem | frgpupval 18187* | 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‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ 〈[𝑔] ∼ , (𝐻 Σg (𝑇 ∘ 𝑔))〉) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑊) → (𝐸‘[𝐴] ∼ ) = (𝐻 Σg (𝑇 ∘ 𝐴))) | ||
Theorem | frgpup1 18188* | 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‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ 〈[𝑔] ∼ , (𝐻 Σg (𝑇 ∘ 𝑔))〉) ⇒ ⊢ (𝜑 → 𝐸 ∈ (𝐺 GrpHom 𝐻)) | ||
Theorem | frgpup2 18189* | 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‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ 〈[𝑔] ∼ , (𝐻 Σg (𝑇 ∘ 𝑔))〉) & ⊢ 𝑈 = (varFGrp‘𝐼) & ⊢ (𝜑 → 𝐴 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝐸‘(𝑈‘𝐴)) = (𝐹‘𝐴)) | ||
Theorem | frgpup3lem 18190* | 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‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2𝑜)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ 〈[𝑔] ∼ , (𝐻 Σg (𝑇 ∘ 𝑔))〉) & ⊢ 𝑈 = (varFGrp‘𝐼) & ⊢ (𝜑 → 𝐾 ∈ (𝐺 GrpHom 𝐻)) & ⊢ (𝜑 → (𝐾 ∘ 𝑈) = 𝐹) ⇒ ⊢ (𝜑 → 𝐾 = 𝐸) | ||
Theorem | frgpup3 18191* | 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 18192 | The free group on zero generators is trivial. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐺 = (freeGrp‘∅) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ 𝐵 ≈ 1𝑜 | ||
Syntax | ccmn 18193 | Extend class notation with class of all commutative monoids. |
class CMnd | ||
Syntax | cabl 18194 | Extend class notation with class of all Abelian groups. |
class Abel | ||
Definition | df-cmn 18195* | Define class of all commutative monoids. (Contributed by Mario Carneiro, 6-Jan-2015.) |
⊢ CMnd = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g‘𝑔)𝑏) = (𝑏(+g‘𝑔)𝑎)} | ||
Definition | df-abl 18196 | Define class of all Abelian groups. (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ Abel = (Grp ∩ CMnd) | ||
Theorem | isabl 18197 | The predicate "is an Abelian (commutative) group." (Contributed by NM, 17-Oct-2011.) |
⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) | ||
Theorem | ablgrp 18198 | An Abelian group is a group. (Contributed by NM, 26-Aug-2011.) |
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) | ||
Theorem | ablcmn 18199 | An Abelian group is a commutative monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
⊢ (𝐺 ∈ Abel → 𝐺 ∈ CMnd) | ||
Theorem | iscmn 18200* | The predicate "is a commutative monoid." (Contributed by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |