![]() |
Metamath
Proof Explorer Theorem List (p. 197 of 480) | < 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: | ![]() (1-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | subgdisj1 19601 | 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 19602 | 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 19603 | Vectors belonging to disjoint commuting subgroups are uniquely determined by their sum. Analogous to opth 5477, 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 19604* | 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 19605* | 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 19606* | Uniqueness of a left projection. (Contributed by Mario Carneiro, 15-Oct-2015.) |
โข + = (+gโ๐บ) & โข โ = (LSSumโ๐บ) & โข 0 = (0gโ๐บ) & โข ๐ = (Cntzโ๐บ) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ (๐ โฉ ๐) = { 0 }) & โข (๐ โ ๐ โ (๐โ๐)) โ โข ((๐ โง ๐ โ (๐ โ ๐)) โ โ!๐ฅ โ ๐ โ๐ฆ โ ๐ ๐ = (๐ฅ + ๐ฆ)) | ||
Theorem | pj1f 19607 | 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 19608 | 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 19609 | 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 19610 | 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 19611 | 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 19612 | 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 19613 | 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 19614 | 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 19615 | 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 19616 | Extend class notation with the free group equivalence relation. |
class ~FG | ||
Syntax | cfrgp 19617 | Extend class notation with the free group construction. |
class freeGrp | ||
Syntax | cvrgp 19618 | Extend class notation with free group injection. |
class varFGrp | ||
Definition | df-efg 19619* | 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 19620 | 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 19619. (Contributed by Mario Carneiro, 1-Oct-2015.) |
โข freeGrp = (๐ โ V โฆ ((freeMndโ(๐ ร 2o)) /s ( ~FG โ๐))) | ||
Definition | df-vrgp 19621* | 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 19622* | 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 19623* | The formal inverse operation is an endofunction on the generating set. (Contributed by Mario Carneiro, 27-Sep-2015.) |
โข ๐ = (๐ฆ โ ๐ผ, ๐ง โ 2o โฆ โจ๐ฆ, (1o โ ๐ง)โฉ) โ โข ๐:(๐ผ ร 2o)โถ(๐ผ ร 2o) | ||
Theorem | efgmnvl 19624* | The inversion function on the generators is an involution. (Contributed by Mario Carneiro, 1-Oct-2015.) |
โข ๐ = (๐ฆ โ ๐ผ, ๐ง โ 2o โฆ โจ๐ฆ, (1o โ ๐ง)โฉ) โ โข (๐ด โ (๐ผ ร 2o) โ (๐โ(๐โ๐ด)) = ๐ด) | ||
Theorem | efgrcl 19625 | Lemma for efgval 19627. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
โข ๐ = ( I โWord (๐ผ ร 2o)) โ โข (๐ด โ ๐ โ (๐ผ โ V โง ๐ = Word (๐ผ ร 2o))) | ||
Theorem | efglem 19626* | Lemma for efgval 19627. (Contributed by Mario Carneiro, 27-Sep-2015.) |
โข ๐ = ( I โWord (๐ผ ร 2o)) โ โข โ๐(๐ Er ๐ โง โ๐ฅ โ ๐ โ๐ โ (0...(โฏโ๐ฅ))โ๐ฆ โ ๐ผ โ๐ง โ 2o ๐ฅ๐(๐ฅ splice โจ๐, ๐, โจโโจ๐ฆ, ๐งโฉโจ๐ฆ, (1o โ ๐ง)โฉโโฉโฉ)) | ||
Theorem | efgval 19627* | Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015.) |
โข ๐ = ( I โWord (๐ผ ร 2o)) & โข โผ = ( ~FG โ๐ผ) โ โข โผ = โฉ {๐ โฃ (๐ Er ๐ โง โ๐ฅ โ ๐ โ๐ โ (0...(โฏโ๐ฅ))โ๐ฆ โ ๐ผ โ๐ง โ 2o ๐ฅ๐(๐ฅ splice โจ๐, ๐, โจโโจ๐ฆ, ๐งโฉโจ๐ฆ, (1o โ ๐ง)โฉโโฉโฉ))} | ||
Theorem | efger 19628 | 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 19629 | 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 19630 | 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 19631 | 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 19632* | 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 19633* | 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 19634* | 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 19635* | 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 19636* | 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 19637* | 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 19638* | 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 19639* | 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 19640* | 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 19641* | 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 19642* | 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 19643* | 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 19644* | 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 19645* | 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 19646* | 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 19647* | 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 19648* | 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 19649* | 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 19650* | The reduced word that forms the base of the sequence in efgsval 19641 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 19651* | Lemma for efgredleme 19653. (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 19652* | Lemma for efgred 19658. (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 19653* | Lemma for efgred 19658. (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 19654* | The reduced word that forms the base of the sequence in efgsval 19641 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 19655* | The reduced word that forms the base of the sequence in efgsval 19641 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 19656* | The reduced word that forms the base of the sequence in efgsval 19641 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 19657* | The reduced word that forms the base of the sequence in efgsval 19641 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 19658* | The reduced word that forms the base of the sequence in efgsval 19641 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 19659* | 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 19660* | 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 19661* | 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 19662* | 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 19663* | 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 19664* | Lemma for efgrelex 19661. 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 19665* | Lemma for efgrelex 19661. 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 19666* | 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 19667* | 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 19668 | Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015.) |
โข ๐บ = (freeGrpโ๐ผ) & โข ๐ = (freeMndโ(๐ผ ร 2o)) & โข โผ = ( ~FG โ๐ผ) โ โข (๐ผ โ ๐ โ ๐บ = (๐ /s โผ )) | ||
Theorem | frgpcpbl 19669 | 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 19670 | 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 19671 | Closure of the quotient map in a free group. (Contributed by Mario Carneiro, 1-Oct-2015.) |
โข ๐บ = (freeGrpโ๐ผ) & โข โผ = ( ~FG โ๐ผ) & โข ๐ = ( I โWord (๐ผ ร 2o)) & โข ๐ต = (Baseโ๐บ) โ โข (๐ โ ๐ โ [๐] โผ โ ๐ต) | ||
Theorem | frgpgrp 19672 | The free group is a group. (Contributed by Mario Carneiro, 1-Oct-2015.) |
โข ๐บ = (freeGrpโ๐ผ) โ โข (๐ผ โ ๐ โ ๐บ โ Grp) | ||
Theorem | frgpadd 19673 | Addition in the free group is given by concatenation. (Contributed by Mario Carneiro, 1-Oct-2015.) |
โข ๐ = ( I โWord (๐ผ ร 2o)) & โข ๐บ = (freeGrpโ๐ผ) & โข โผ = ( ~FG โ๐ผ) & โข + = (+gโ๐บ) โ โข ((๐ด โ ๐ โง ๐ต โ ๐) โ ([๐ด] โผ + [๐ต] โผ ) = [(๐ด ++ ๐ต)] โผ ) | ||
Theorem | frgpinv 19674* | 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 19675* | 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 19676* | 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 19677 | The value of the generating elements of a free group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
โข โผ = ( ~FG โ๐ผ) & โข ๐ = (varFGrpโ๐ผ) โ โข ((๐ผ โ ๐ โง ๐ด โ ๐ผ) โ (๐โ๐ด) = [โจโโจ๐ด, โ โฉโโฉ] โผ ) | ||
Theorem | vrgpf 19678 | 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 19679 | 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 19680* | 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 19681* | 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 19682* | Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.) |
โข ๐ต = (Baseโ๐ป) & โข ๐ = (invgโ๐ป) & โข ๐ = (๐ฆ โ ๐ผ, ๐ง โ 2o โฆ if(๐ง = โ , (๐นโ๐ฆ), (๐โ(๐นโ๐ฆ)))) & โข (๐ โ ๐ป โ Grp) & โข (๐ โ ๐ผ โ ๐) & โข (๐ โ ๐น:๐ผโถ๐ต) & โข ๐ = ( I โWord (๐ผ ร 2o)) & โข โผ = ( ~FG โ๐ผ) โ โข ((๐ โง ๐ด โผ ๐ถ) โ (๐ป ฮฃg (๐ โ ๐ด)) = (๐ป ฮฃg (๐ โ ๐ถ))) | ||
Theorem | frgpupf 19683* | Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.) |
โข ๐ต = (Baseโ๐ป) & โข ๐ = (invgโ๐ป) & โข ๐ = (๐ฆ โ ๐ผ, ๐ง โ 2o โฆ if(๐ง = โ , (๐นโ๐ฆ), (๐โ(๐นโ๐ฆ)))) & โข (๐ โ ๐ป โ Grp) & โข (๐ โ ๐ผ โ ๐) & โข (๐ โ ๐น:๐ผโถ๐ต) & โข ๐ = ( I โWord (๐ผ ร 2o)) & โข โผ = ( ~FG โ๐ผ) & โข ๐บ = (freeGrpโ๐ผ) & โข ๐ = (Baseโ๐บ) & โข ๐ธ = ran (๐ โ ๐ โฆ โจ[๐] โผ , (๐ป ฮฃg (๐ โ ๐))โฉ) โ โข (๐ โ ๐ธ:๐โถ๐ต) | ||
Theorem | frgpupval 19684* | Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.) |
โข ๐ต = (Baseโ๐ป) & โข ๐ = (invgโ๐ป) & โข ๐ = (๐ฆ โ ๐ผ, ๐ง โ 2o โฆ if(๐ง = โ , (๐นโ๐ฆ), (๐โ(๐นโ๐ฆ)))) & โข (๐ โ ๐ป โ Grp) & โข (๐ โ ๐ผ โ ๐) & โข (๐ โ ๐น:๐ผโถ๐ต) & โข ๐ = ( I โWord (๐ผ ร 2o)) & โข โผ = ( ~FG โ๐ผ) & โข ๐บ = (freeGrpโ๐ผ) & โข ๐ = (Baseโ๐บ) & โข ๐ธ = ran (๐ โ ๐ โฆ โจ[๐] โผ , (๐ป ฮฃg (๐ โ ๐))โฉ) โ โข ((๐ โง ๐ด โ ๐) โ (๐ธโ[๐ด] โผ ) = (๐ป ฮฃg (๐ โ ๐ด))) | ||
Theorem | frgpup1 19685* | Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) |
โข ๐ต = (Baseโ๐ป) & โข ๐ = (invgโ๐ป) & โข ๐ = (๐ฆ โ ๐ผ, ๐ง โ 2o โฆ if(๐ง = โ , (๐นโ๐ฆ), (๐โ(๐นโ๐ฆ)))) & โข (๐ โ ๐ป โ Grp) & โข (๐ โ ๐ผ โ ๐) & โข (๐ โ ๐น:๐ผโถ๐ต) & โข ๐ = ( I โWord (๐ผ ร 2o)) & โข โผ = ( ~FG โ๐ผ) & โข ๐บ = (freeGrpโ๐ผ) & โข ๐ = (Baseโ๐บ) & โข ๐ธ = ran (๐ โ ๐ โฆ โจ[๐] โผ , (๐ป ฮฃg (๐ โ ๐))โฉ) โ โข (๐ โ ๐ธ โ (๐บ GrpHom ๐ป)) | ||
Theorem | frgpup2 19686* | The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) |
โข ๐ต = (Baseโ๐ป) & โข ๐ = (invgโ๐ป) & โข ๐ = (๐ฆ โ ๐ผ, ๐ง โ 2o โฆ if(๐ง = โ , (๐นโ๐ฆ), (๐โ(๐นโ๐ฆ)))) & โข (๐ โ ๐ป โ Grp) & โข (๐ โ ๐ผ โ ๐) & โข (๐ โ ๐น:๐ผโถ๐ต) & โข ๐ = ( I โWord (๐ผ ร 2o)) & โข โผ = ( ~FG โ๐ผ) & โข ๐บ = (freeGrpโ๐ผ) & โข ๐ = (Baseโ๐บ) & โข ๐ธ = ran (๐ โ ๐ โฆ โจ[๐] โผ , (๐ป ฮฃg (๐ โ ๐))โฉ) & โข ๐ = (varFGrpโ๐ผ) & โข (๐ โ ๐ด โ ๐ผ) โ โข (๐ โ (๐ธโ(๐โ๐ด)) = (๐นโ๐ด)) | ||
Theorem | frgpup3lem 19687* | The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) |
โข ๐ต = (Baseโ๐ป) & โข ๐ = (invgโ๐ป) & โข ๐ = (๐ฆ โ ๐ผ, ๐ง โ 2o โฆ if(๐ง = โ , (๐นโ๐ฆ), (๐โ(๐นโ๐ฆ)))) & โข (๐ โ ๐ป โ Grp) & โข (๐ โ ๐ผ โ ๐) & โข (๐ โ ๐น:๐ผโถ๐ต) & โข ๐ = ( I โWord (๐ผ ร 2o)) & โข โผ = ( ~FG โ๐ผ) & โข ๐บ = (freeGrpโ๐ผ) & โข ๐ = (Baseโ๐บ) & โข ๐ธ = ran (๐ โ ๐ โฆ โจ[๐] โผ , (๐ป ฮฃg (๐ โ ๐))โฉ) & โข ๐ = (varFGrpโ๐ผ) & โข (๐ โ ๐พ โ (๐บ GrpHom ๐ป)) & โข (๐ โ (๐พ โ ๐) = ๐น) โ โข (๐ โ ๐พ = ๐ธ) | ||
Theorem | frgpup3 19688* | 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 19689 | The free group on zero generators is trivial. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐บ = (freeGrpโโ ) & โข ๐ต = (Baseโ๐บ) โ โข ๐ต โ 1o | ||
Syntax | ccmn 19690 | Extend class notation with class of all commutative monoids. |
class CMnd | ||
Syntax | cabl 19691 | Extend class notation with class of all Abelian groups. |
class Abel | ||
Definition | df-cmn 19692* | Define class of all commutative monoids. (Contributed by Mario Carneiro, 6-Jan-2015.) |
โข CMnd = {๐ โ Mnd โฃ โ๐ โ (Baseโ๐)โ๐ โ (Baseโ๐)(๐(+gโ๐)๐) = (๐(+gโ๐)๐)} | ||
Definition | df-abl 19693 | Define class of all Abelian groups. (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
โข Abel = (Grp โฉ CMnd) | ||
Theorem | isabl 19694 | The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.) |
โข (๐บ โ Abel โ (๐บ โ Grp โง ๐บ โ CMnd)) | ||
Theorem | ablgrp 19695 | An Abelian group is a group. (Contributed by NM, 26-Aug-2011.) |
โข (๐บ โ Abel โ ๐บ โ Grp) | ||
Theorem | ablgrpd 19696 | An Abelian group is a group, deduction form of ablgrp 19695. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข (๐ โ ๐บ โ Abel) โ โข (๐ โ ๐บ โ Grp) | ||
Theorem | ablcmn 19697 | An Abelian group is a commutative monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
โข (๐บ โ Abel โ ๐บ โ CMnd) | ||
Theorem | ablcmnd 19698 | An Abelian group is a commutative monoid. (Contributed by SN, 1-Jun-2024.) |
โข (๐ โ ๐บ โ Abel) โ โข (๐ โ ๐บ โ CMnd) | ||
Theorem | iscmn 19699* | The predicate "is a commutative monoid". (Contributed by Mario Carneiro, 6-Jan-2015.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข (๐บ โ CMnd โ (๐บ โ Mnd โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐ฅ + ๐ฆ) = (๐ฆ + ๐ฅ))) | ||
Theorem | isabl2 19700* | The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข (๐บ โ Abel โ (๐บ โ Grp โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐ฅ + ๐ฆ) = (๐ฆ + ๐ฅ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |