Home | Metamath
Proof Explorer Theorem List (p. 188 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lsmless2x 18701 | Subset implies subgroup sum subset (extended domain version). (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (((𝐺 ∈ 𝑉 ∧ 𝑅 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) ∧ 𝑇 ⊆ 𝑈) → (𝑅 ⊕ 𝑇) ⊆ (𝑅 ⊕ 𝑈)) | ||
Theorem | lsmub1x 18702 | Subgroup sum is an upper bound of its arguments. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ⊆ 𝐵 ∧ 𝑈 ∈ (SubMnd‘𝐺)) → 𝑇 ⊆ (𝑇 ⊕ 𝑈)) | ||
Theorem | lsmub2x 18703 | Subgroup sum is an upper bound of its arguments. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubMnd‘𝐺) ∧ 𝑈 ⊆ 𝐵) → 𝑈 ⊆ (𝑇 ⊕ 𝑈)) | ||
Theorem | lsmval 18704* | Subgroup sum value (for a left module or left vector space). (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑇 ⊕ 𝑈) = ran (𝑥 ∈ 𝑇, 𝑦 ∈ 𝑈 ↦ (𝑥 + 𝑦))) | ||
Theorem | lsmelval 18705* | Subgroup sum membership (for a left module or left vector space). (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑋 ∈ (𝑇 ⊕ 𝑈) ↔ ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 𝑋 = (𝑦 + 𝑧))) | ||
Theorem | lsmelvali 18706 | Subgroup sum membership (for a left module or left vector space). (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ (𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑈)) → (𝑋 + 𝑌) ∈ (𝑇 ⊕ 𝑈)) | ||
Theorem | lsmelvalm 18707* | Subgroup sum membership analogue of lsmelval 18705 using vector subtraction. TODO: any way to shorten proof? (Contributed by NM, 16-Mar-2015.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ − = (-g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑇 ⊕ 𝑈) ↔ ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 𝑋 = (𝑦 − 𝑧))) | ||
Theorem | lsmelvalmi 18708 | Membership of vector subtraction in subgroup sum. (Contributed by NM, 27-Apr-2015.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ − = (-g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑋 ∈ 𝑇) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) ∈ (𝑇 ⊕ 𝑈)) | ||
Theorem | lsmsubm 18709 | The sum of two commuting submonoids is a submonoid. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubMnd‘𝐺) ∧ 𝑈 ∈ (SubMnd‘𝐺) ∧ 𝑇 ⊆ (𝑍‘𝑈)) → (𝑇 ⊕ 𝑈) ∈ (SubMnd‘𝐺)) | ||
Theorem | lsmsubg 18710 | The sum of two commuting subgroups is a subgroup. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ (𝑍‘𝑈)) → (𝑇 ⊕ 𝑈) ∈ (SubGrp‘𝐺)) | ||
Theorem | lsmcom2 18711 | Subgroup sum commutes. (Contributed by Mario Carneiro, 22-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ (𝑍‘𝑈)) → (𝑇 ⊕ 𝑈) = (𝑈 ⊕ 𝑇)) | ||
Theorem | smndlsmidm 18712 | The direct product is idempotent for submonoids. (Contributed by AV, 27-Dec-2023.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (𝑈 ∈ (SubMnd‘𝐺) → (𝑈 ⊕ 𝑈) = 𝑈) | ||
Theorem | lsmub1 18713 | Subgroup sum is an upper bound of its arguments. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝑇 ⊆ (𝑇 ⊕ 𝑈)) | ||
Theorem | lsmub2 18714 | Subgroup sum is an upper bound of its arguments. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝑈 ⊆ (𝑇 ⊕ 𝑈)) | ||
Theorem | lsmunss 18715 | Union of subgroups is a subset of subgroup sum. (Contributed by NM, 6-Feb-2014.) (Proof shortened by Mario Carneiro, 21-Jun-2014.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑇 ∪ 𝑈) ⊆ (𝑇 ⊕ 𝑈)) | ||
Theorem | lsmless1 18716 | Subset implies subgroup sum subset. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑆 ⊆ 𝑇) → (𝑆 ⊕ 𝑈) ⊆ (𝑇 ⊕ 𝑈)) | ||
Theorem | lsmless2 18717 | Subset implies subgroup sum subset. (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ 𝑈) → (𝑆 ⊕ 𝑇) ⊆ (𝑆 ⊕ 𝑈)) | ||
Theorem | lsmless12 18718 | Subset implies subgroup sum subset. (Contributed by NM, 14-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ (𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈)) → (𝑅 ⊕ 𝑇) ⊆ (𝑆 ⊕ 𝑈)) | ||
Theorem | lsmidm 18719 | Subgroup sum is idempotent. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) (Proof shortened by AV, 27-Dec-2023.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (𝑈 ∈ (SubGrp‘𝐺) → (𝑈 ⊕ 𝑈) = 𝑈) | ||
Theorem | lsmidmOLD 18720 | Obsolete proof of lsmidm 18719 as of 13-Jan-2024. Subgroup sum is idempotent. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (𝑈 ∈ (SubGrp‘𝐺) → (𝑈 ⊕ 𝑈) = 𝑈) | ||
Theorem | lsmlub 18721 | The least upper bound property of subgroup sum. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → ((𝑆 ⊆ 𝑈 ∧ 𝑇 ⊆ 𝑈) ↔ (𝑆 ⊕ 𝑇) ⊆ 𝑈)) | ||
Theorem | lsmss1 18722 | Subgroup sum with a subset. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ 𝑈) → (𝑇 ⊕ 𝑈) = 𝑈) | ||
Theorem | lsmss1b 18723 | Subgroup sum with a subset. (Contributed by NM, 10-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑇 ⊆ 𝑈 ↔ (𝑇 ⊕ 𝑈) = 𝑈)) | ||
Theorem | lsmss2 18724 | Subgroup sum with a subset. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑈 ⊆ 𝑇) → (𝑇 ⊕ 𝑈) = 𝑇) | ||
Theorem | lsmss2b 18725 | Subgroup sum with a subset. (Contributed by NM, 10-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑈 ⊆ 𝑇 ↔ (𝑇 ⊕ 𝑈) = 𝑇)) | ||
Theorem | lsmass 18726 | Subgroup sum is associative. (Contributed by NM, 2-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → ((𝑅 ⊕ 𝑇) ⊕ 𝑈) = (𝑅 ⊕ (𝑇 ⊕ 𝑈))) | ||
Theorem | mndlsmidm 18727 | Subgroup sum is idempotent for monoids. This corresponds to the observation in [Lang] p. 6. (Contributed by AV, 27-Dec-2023.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Mnd → (𝐵 ⊕ 𝐵) = 𝐵) | ||
Theorem | lsm01 18728 | Subgroup sum with the zero subgroup. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (𝑋 ∈ (SubGrp‘𝐺) → (𝑋 ⊕ { 0 }) = 𝑋) | ||
Theorem | lsm02 18729 | Subgroup sum with the zero subgroup. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (𝑋 ∈ (SubGrp‘𝐺) → ({ 0 } ⊕ 𝑋) = 𝑋) | ||
Theorem | subglsm 18730 | The subgroup sum evaluated within a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐴 = (LSSum‘𝐻) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆) → (𝑇 ⊕ 𝑈) = (𝑇𝐴𝑈)) | ||
Theorem | lssnle 18731 | Equivalent expressions for "not less than". (chnlei 29190 analog.) (Contributed by NM, 10-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) ⇒ ⊢ (𝜑 → (¬ 𝑈 ⊆ 𝑇 ↔ 𝑇 ⊊ (𝑇 ⊕ 𝑈))) | ||
Theorem | lsmmod 18732 | 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 18733 | 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 18734* | 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 18735 | Commute the "subgroups commute" predicate. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈)) ⇒ ⊢ (𝜑 → 𝑈 ⊆ (𝑍‘𝑇)) | ||
Theorem | lsmcntz 18736 | The "subgroups commute" predicate applied to a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝜑 → ((𝑆 ⊕ 𝑇) ⊆ (𝑍‘𝑈) ↔ (𝑆 ⊆ (𝑍‘𝑈) ∧ 𝑇 ⊆ (𝑍‘𝑈)))) | ||
Theorem | lsmcntzr 18737 | The "subgroups commute" predicate applied to a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝜑 → (𝑆 ⊆ (𝑍‘(𝑇 ⊕ 𝑈)) ↔ (𝑆 ⊆ (𝑍‘𝑇) ∧ 𝑆 ⊆ (𝑍‘𝑈)))) | ||
Theorem | lsmdisj 18738 | Disjointness from a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → ((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 }) ⇒ ⊢ (𝜑 → ((𝑆 ∩ 𝑈) = { 0 } ∧ (𝑇 ∩ 𝑈) = { 0 })) | ||
Theorem | lsmdisj2 18739 | 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 18740 | 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 18741 | Disjointness from a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → (𝑆 ∩ (𝑇 ⊕ 𝑈)) = { 0 }) ⇒ ⊢ (𝜑 → ((𝑆 ∩ 𝑇) = { 0 } ∧ (𝑆 ∩ 𝑈) = { 0 })) | ||
Theorem | lsmdisj2r 18742 | 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 18743 | 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 18744 | 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 18745 | 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 18746 | 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 18747 | 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 18748 | 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 18749 | 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 18750 | Vectors belonging to disjoint commuting subgroups are uniquely determined by their sum. Analogous to opth 5360, 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 18751* | 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 18752* | 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 18753* | Uniqueness of a left projection. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 }) & ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) → ∃!𝑥 ∈ 𝑇 ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦)) | ||
Theorem | pj1f 18754 | 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 18755 | 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 18756 | 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 18757 | 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 18758 | 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 18759 | 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 18760 | 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 18761 | 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 18762 | 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 18763 | Extend class notation with the free group equivalence relation. |
class ~FG | ||
Syntax | cfrgp 18764 | Extend class notation with the free group construction. |
class freeGrp | ||
Syntax | cvrgp 18765 | Extend class notation with free group injection. |
class varFGrp | ||
Definition | df-efg 18766* | 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 18767 | 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 18766. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ freeGrp = (𝑖 ∈ V ↦ ((freeMnd‘(𝑖 × 2o)) /s ( ~FG ‘𝑖))) | ||
Definition | df-vrgp 18768* | 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 18769* | 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 18770* | The formal inverse operation is an endofunction on the generating set. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) ⇒ ⊢ 𝑀:(𝐼 × 2o)⟶(𝐼 × 2o) | ||
Theorem | efgmnvl 18771* | The inversion function on the generators is an involution. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) ⇒ ⊢ (𝐴 ∈ (𝐼 × 2o) → (𝑀‘(𝑀‘𝐴)) = 𝐴) | ||
Theorem | efgrcl 18772 | Lemma for efgval 18774. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) ⇒ ⊢ (𝐴 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o))) | ||
Theorem | efglem 18773* | Lemma for efgval 18774. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) ⇒ ⊢ ∃𝑟(𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉)) | ||
Theorem | efgval 18774* | Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) & ⊢ ∼ = ( ~FG ‘𝐼) ⇒ ⊢ ∼ = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice 〈𝑛, 𝑛, 〈“〈𝑦, 𝑧〉〈𝑦, (1o ∖ 𝑧)〉”〉〉))} | ||
Theorem | efger 18775 | 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 18776 | 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 18777 | 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 18778 | 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 18779* | 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 18780* | 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 18781* | 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 18782* | 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 18783* | 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 18784* | 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 18785* | 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 18786* | 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 18787* | 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 18788* | 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 18789* | 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 18790* | 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 18791* | 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 18792* | 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 18793* | 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 18794* | 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 18795* | 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 18796* | 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 18797* | The reduced word that forms the base of the sequence in efgsval 18788 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 18798* | Lemma for efgredleme 18800. (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 18799* | Lemma for efgred 18805. (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 18800* | Lemma for efgred 18805. (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 (𝑇‘(𝑆‘𝐶)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |