Home | Metamath
Proof Explorer Theorem List (p. 189 of 450) | < 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | subglsm 18801 | The subgroup sum evaluated within a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐴 = (LSSum‘𝐻) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆) → (𝑇 ⊕ 𝑈) = (𝑇𝐴𝑈)) | ||
Theorem | lssnle 18802 | Equivalent expressions for "not less than". (chnlei 29264 analog.) (Contributed by NM, 10-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) ⇒ ⊢ (𝜑 → (¬ 𝑈 ⊆ 𝑇 ↔ 𝑇 ⊊ (𝑇 ⊕ 𝑈))) | ||
Theorem | lsmmod 18803 | The modular law holds for subgroup sum. Similar to part of Theorem 16.9 of [MaedaMaeda] p. 70. (Contributed by NM, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ 𝑆 ⊆ 𝑈) → (𝑆 ⊕ (𝑇 ∩ 𝑈)) = ((𝑆 ⊕ 𝑇) ∩ 𝑈)) | ||
Theorem | lsmmod2 18804 | Modular law dual for subgroup sum. Similar to part of Theorem 16.9 of [MaedaMaeda] p. 70. (Contributed by NM, 8-Jan-2015.) (Revised by Mario Carneiro, 21-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ 𝑈 ⊆ 𝑆) → (𝑆 ∩ (𝑇 ⊕ 𝑈)) = ((𝑆 ∩ 𝑇) ⊕ 𝑈)) | ||
Theorem | lsmpropd 18805* | If two structures have the same components (properties), they have the same subspace structure. (Contributed by Mario Carneiro, 29-Jun-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ (𝜑 → 𝐾 ∈ V) & ⊢ (𝜑 → 𝐿 ∈ V) ⇒ ⊢ (𝜑 → (LSSum‘𝐾) = (LSSum‘𝐿)) | ||
Theorem | cntzrecd 18806 | Commute the "subgroups commute" predicate. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈)) ⇒ ⊢ (𝜑 → 𝑈 ⊆ (𝑍‘𝑇)) | ||
Theorem | lsmcntz 18807 | The "subgroups commute" predicate applied to a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝜑 → ((𝑆 ⊕ 𝑇) ⊆ (𝑍‘𝑈) ↔ (𝑆 ⊆ (𝑍‘𝑈) ∧ 𝑇 ⊆ (𝑍‘𝑈)))) | ||
Theorem | lsmcntzr 18808 | The "subgroups commute" predicate applied to a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝜑 → (𝑆 ⊆ (𝑍‘(𝑇 ⊕ 𝑈)) ↔ (𝑆 ⊆ (𝑍‘𝑇) ∧ 𝑆 ⊆ (𝑍‘𝑈)))) | ||
Theorem | lsmdisj 18809 | Disjointness from a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → ((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 }) ⇒ ⊢ (𝜑 → ((𝑆 ∩ 𝑈) = { 0 } ∧ (𝑇 ∩ 𝑈) = { 0 })) | ||
Theorem | lsmdisj2 18810 | Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 22-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → ((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 }) & ⊢ (𝜑 → (𝑆 ∩ 𝑇) = { 0 }) ⇒ ⊢ (𝜑 → (𝑇 ∩ (𝑆 ⊕ 𝑈)) = { 0 }) | ||
Theorem | lsmdisj3 18811 | Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → ((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 }) & ⊢ (𝜑 → (𝑆 ∩ 𝑇) = { 0 }) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝑆 ⊆ (𝑍‘𝑇)) ⇒ ⊢ (𝜑 → (𝑆 ∩ (𝑇 ⊕ 𝑈)) = { 0 }) | ||
Theorem | lsmdisjr 18812 | Disjointness from a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → (𝑆 ∩ (𝑇 ⊕ 𝑈)) = { 0 }) ⇒ ⊢ (𝜑 → ((𝑆 ∩ 𝑇) = { 0 } ∧ (𝑆 ∩ 𝑈) = { 0 })) | ||
Theorem | lsmdisj2r 18813 | Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 22-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → (𝑆 ∩ (𝑇 ⊕ 𝑈)) = { 0 }) & ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 }) ⇒ ⊢ (𝜑 → ((𝑆 ⊕ 𝑈) ∩ 𝑇) = { 0 }) | ||
Theorem | lsmdisj3r 18814 | Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 22-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → (𝑆 ∩ (𝑇 ⊕ 𝑈)) = { 0 }) & ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 }) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈)) ⇒ ⊢ (𝜑 → ((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 }) | ||
Theorem | lsmdisj2a 18815 | 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 | lsmdisj2b 18816 | 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 18817 | 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 18818 | 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 18819 | 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 18820 | 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 18821 | Vectors belonging to disjoint commuting subgroups are uniquely determined by their sum. Analogous to opth 5370, 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 18822* | 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 18823* | 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 18824* | Uniqueness of a left projection. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 }) & ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) → ∃!𝑥 ∈ 𝑇 ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦)) | ||
Theorem | pj1f 18825 | 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 18826 | 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 18827 | 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 18828 | 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 18829 | 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 18830 | 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 18831 | 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 18832 | 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 18833 | 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 18834 | Extend class notation with the free group equivalence relation. |
class ~FG | ||
Syntax | cfrgp 18835 | Extend class notation with the free group construction. |
class freeGrp | ||
Syntax | cvrgp 18836 | Extend class notation with free group injection. |
class varFGrp | ||
Definition | df-efg 18837* | 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 18838 | 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 18837. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ freeGrp = (𝑖 ∈ V ↦ ((freeMnd‘(𝑖 × 2o)) /s ( ~FG ‘𝑖))) | ||
Definition | df-vrgp 18839* | 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 18840* | 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 18841* | The formal inverse operation is an endofunction on the generating set. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) ⇒ ⊢ 𝑀:(𝐼 × 2o)⟶(𝐼 × 2o) | ||
Theorem | efgmnvl 18842* | The inversion function on the generators is an involution. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) ⇒ ⊢ (𝐴 ∈ (𝐼 × 2o) → (𝑀‘(𝑀‘𝐴)) = 𝐴) | ||
Theorem | efgrcl 18843 | Lemma for efgval 18845. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) ⇒ ⊢ (𝐴 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o))) | ||
Theorem | efglem 18844* | Lemma for efgval 18845. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) ⇒ ⊢ ∃𝑟(𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉)) | ||
Theorem | efgval 18845* | Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) & ⊢ ∼ = ( ~FG ‘𝐼) ⇒ ⊢ ∼ = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} | ||
Theorem | efger 18846 | 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 18847 | 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 18848 | 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 18849 | 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 18850* | 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 18851* | 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 18852* | 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 18853* | 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 18854* | 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 18855* | 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 18856* | 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 18857* | 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 18858* | 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 18859* | 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 18860* | 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 18861* | 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 18862* | 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 18863* | 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 18864* | 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 18865* | 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 18866* | 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 18867* | 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 18868* | The reduced word that forms the base of the sequence in efgsval 18859 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 18869* | Lemma for efgredleme 18871. (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 18870* | Lemma for efgred 18876. (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 18871* | Lemma for efgred 18876. (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 18872* | The reduced word that forms the base of the sequence in efgsval 18859 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 18873* | The reduced word that forms the base of the sequence in efgsval 18859 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 18874* | The reduced word that forms the base of the sequence in efgsval 18859 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 18875* | The reduced word that forms the base of the sequence in efgsval 18859 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 18876* | The reduced word that forms the base of the sequence in efgsval 18859 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 18877* | 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 18878* | 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 18879* | 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 18880* | 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 18881* | 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 18882* | Lemma for efgrelex 18879. 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 18883* | Lemma for efgrelex 18879. 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 18884* | 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 18885* | 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 18886 | Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑀 = (freeMnd‘(𝐼 × 2o)) & ⊢ ∼ = ( ~FG ‘𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐺 = (𝑀 /s ∼ )) | ||
Theorem | frgpcpbl 18887 | 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 18888 | 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 18889 | Closure of the quotient map in a free group. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝑊 → [𝑋] ∼ ∈ 𝐵) | ||
Theorem | frgpgrp 18890 | The free group is a group. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝐺 = (freeGrp‘𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐺 ∈ Grp) | ||
Theorem | frgpadd 18891 | Addition in the free group is given by concatenation. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ([𝐴] ∼ + [𝐵] ∼ ) = [(𝐴 ++ 𝐵)] ∼ ) | ||
Theorem | frgpinv 18892* | 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 18893* | 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 18894* | 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 18895 | The value of the generating elements of a free group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝑈 = (varFGrp‘𝐼) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) → (𝑈‘𝐴) = [〈“〈𝐴, ∅〉”〉] ∼ ) | ||
Theorem | vrgpf 18896 | 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 18897 | 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 18898* | 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 18899* | 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 18900* | 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 (𝑇 ∘ 𝐶))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |