![]() |
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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | subgdisj2 19601 | 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 19602 | Vectors belonging to disjoint commuting subgroups are uniquely determined by their sum. Analogous to opth 5475, 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 19603* | 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 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 | pj1eu 19605* | Uniqueness of a left projection. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ + = (+gβπΊ) & β’ β = (LSSumβπΊ) & β’ 0 = (0gβπΊ) & β’ π = (CntzβπΊ) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β (π β© π) = { 0 }) & β’ (π β π β (πβπ)) β β’ ((π β§ π β (π β π)) β β!π₯ β π βπ¦ β π π = (π₯ + π¦)) | ||
Theorem | pj1f 19606 | 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 19607 | 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 19608 | 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 19609 | 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 19610 | 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 19611 | 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 19612 | 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 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 (πΊ βΎs π))) | ||
Theorem | lsmhash 19614 | 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 19615 | Extend class notation with the free group equivalence relation. |
class ~FG | ||
Syntax | cfrgp 19616 | Extend class notation with the free group construction. |
class freeGrp | ||
Syntax | cvrgp 19617 | Extend class notation with free group injection. |
class varFGrp | ||
Definition | df-efg 19618* | 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 19619 | 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 19618. (Contributed by Mario Carneiro, 1-Oct-2015.) |
β’ freeGrp = (π β V β¦ ((freeMndβ(π Γ 2o)) /s ( ~FG βπ))) | ||
Definition | df-vrgp 19620* | 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 19621* | 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 19622* | The formal inverse operation is an endofunction on the generating set. (Contributed by Mario Carneiro, 27-Sep-2015.) |
β’ π = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) β β’ π:(πΌ Γ 2o)βΆ(πΌ Γ 2o) | ||
Theorem | efgmnvl 19623* | The inversion function on the generators is an involution. (Contributed by Mario Carneiro, 1-Oct-2015.) |
β’ π = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) β β’ (π΄ β (πΌ Γ 2o) β (πβ(πβπ΄)) = π΄) | ||
Theorem | efgrcl 19624 | Lemma for efgval 19626. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
β’ π = ( I βWord (πΌ Γ 2o)) β β’ (π΄ β π β (πΌ β V β§ π = Word (πΌ Γ 2o))) | ||
Theorem | efglem 19625* | Lemma for efgval 19626. (Contributed by Mario Carneiro, 27-Sep-2015.) |
β’ π = ( I βWord (πΌ Γ 2o)) β β’ βπ(π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©)) | ||
Theorem | efgval 19626* | Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015.) |
β’ π = ( I βWord (πΌ Γ 2o)) & β’ βΌ = ( ~FG βπΌ) β β’ βΌ = β© {π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))} | ||
Theorem | efger 19627 | 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 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 βπΌ) β β’ (((π΄ β π β§ π β (0...(β―βπ΄))) β§ (π½ β πΌ β§ πΎ β 2o)) β π΄ βΌ (π΄ splice β¨π, π, β¨ββ¨π½, πΎβ©β¨π½, (1o β πΎ)β©ββ©β©)) | ||
Theorem | efgi0 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...(β―βπ΄)) β§ π½ β πΌ) β π΄ βΌ (π΄ splice β¨π, π, β¨ββ¨π½, β β©β¨π½, 1oβ©ββ©β©)) | ||
Theorem | efgi1 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 | efgtf 19631* | 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 19632* | 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 19633* | 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 19634* | 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 19635* | 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 19636* | 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 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 | efgsf 19638* | 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 19639* | 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 19640* | 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 19641* | 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 19642* | 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 19643* | 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 19644* | 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 19645* | 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 19646* | 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 19647* | 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 19648* | 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 19649* | The reduced word that forms the base of the sequence in efgsval 19640 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 19650* | Lemma for efgredleme 19652. (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 19651* | Lemma for efgred 19657. (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 19652* | Lemma for efgred 19657. (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 19653* | The reduced word that forms the base of the sequence in efgsval 19640 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 19654* | The reduced word that forms the base of the sequence in efgsval 19640 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 19655* | The reduced word that forms the base of the sequence in efgsval 19640 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 19656* | The reduced word that forms the base of the sequence in efgsval 19640 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 19657* | The reduced word that forms the base of the sequence in efgsval 19640 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 19658* | 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 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)} β β’ βΌ β πΏ | ||
Theorem | efgrelex 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 | efgredeu 19661* | 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 19662* | 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 19663* | Lemma for efgrelex 19660. 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 19664* | Lemma for efgrelex 19660. 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 19665* | 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 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 | frgpval 19667 | Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015.) |
β’ πΊ = (freeGrpβπΌ) & β’ π = (freeMndβ(πΌ Γ 2o)) & β’ βΌ = ( ~FG βπΌ) β β’ (πΌ β π β πΊ = (π /s βΌ )) | ||
Theorem | frgpcpbl 19668 | 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 19669 | 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 19670 | Closure of the quotient map in a free group. (Contributed by Mario Carneiro, 1-Oct-2015.) |
β’ πΊ = (freeGrpβπΌ) & β’ βΌ = ( ~FG βπΌ) & β’ π = ( I βWord (πΌ Γ 2o)) & β’ π΅ = (BaseβπΊ) β β’ (π β π β [π] βΌ β π΅) | ||
Theorem | frgpgrp 19671 | The free group is a group. (Contributed by Mario Carneiro, 1-Oct-2015.) |
β’ πΊ = (freeGrpβπΌ) β β’ (πΌ β π β πΊ β Grp) | ||
Theorem | frgpadd 19672 | Addition in the free group is given by concatenation. (Contributed by Mario Carneiro, 1-Oct-2015.) |
β’ π = ( I βWord (πΌ Γ 2o)) & β’ πΊ = (freeGrpβπΌ) & β’ βΌ = ( ~FG βπΌ) & β’ + = (+gβπΊ) β β’ ((π΄ β π β§ π΅ β π) β ([π΄] βΌ + [π΅] βΌ ) = [(π΄ ++ π΅)] βΌ ) | ||
Theorem | frgpinv 19673* | 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 19674* | 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 19675* | 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 19676 | The value of the generating elements of a free group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ βΌ = ( ~FG βπΌ) & β’ π = (varFGrpβπΌ) β β’ ((πΌ β π β§ π΄ β πΌ) β (πβπ΄) = [β¨ββ¨π΄, β β©ββ©] βΌ ) | ||
Theorem | vrgpf 19677 | 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 19678 | 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 19679* | 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 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 β¦ β¨π¦, (1o β π§)β©) β β’ ((π β§ π΄ β (πΌ Γ 2o)) β (πβ(πβπ΄)) = (πβ(πβπ΄))) | ||
Theorem | frgpuplem 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) & β’ (π β πΌ β π) & β’ (π β πΉ:πΌβΆπ΅) & β’ π = ( I βWord (πΌ Γ 2o)) & β’ βΌ = ( ~FG βπΌ) β β’ ((π β§ π΄ βΌ πΆ) β (π» Ξ£g (π β π΄)) = (π» Ξ£g (π β πΆ))) | ||
Theorem | frgpupf 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 βπΌ) & β’ πΊ = (freeGrpβπΌ) & β’ π = (BaseβπΊ) & β’ πΈ = ran (π β π β¦ β¨[π] βΌ , (π» Ξ£g (π β π))β©) β β’ (π β πΈ:πβΆπ΅) | ||
Theorem | frgpupval 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 (π β π))β©) β β’ ((π β§ π΄ β π) β (πΈβ[π΄] βΌ ) = (π» Ξ£g (π β π΄))) | ||
Theorem | frgpup1 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.) (Revised by Mario Carneiro, 28-Feb-2016.) |
β’ π΅ = (Baseβπ») & β’ π = (invgβπ») & β’ π = (π¦ β πΌ, π§ β 2o β¦ if(π§ = β , (πΉβπ¦), (πβ(πΉβπ¦)))) & β’ (π β π» β Grp) & β’ (π β πΌ β π) & β’ (π β πΉ:πΌβΆπ΅) & β’ π = ( I βWord (πΌ Γ 2o)) & β’ βΌ = ( ~FG βπΌ) & β’ πΊ = (freeGrpβπΌ) & β’ π = (BaseβπΊ) & β’ πΈ = ran (π β π β¦ β¨[π] βΌ , (π» Ξ£g (π β π))β©) β β’ (π β πΈ β (πΊ GrpHom π»)) | ||
Theorem | frgpup2 19685* | 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 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βπΌ) & β’ (π β πΎ β (πΊ GrpHom π»)) & β’ (π β (πΎ β π) = πΉ) β β’ (π β πΎ = πΈ) | ||
Theorem | frgpup3 19687* | 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 19688 | The free group on zero generators is trivial. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ πΊ = (freeGrpββ ) & β’ π΅ = (BaseβπΊ) β β’ π΅ β 1o | ||
Syntax | ccmn 19689 | Extend class notation with class of all commutative monoids. |
class CMnd | ||
Syntax | cabl 19690 | Extend class notation with class of all Abelian groups. |
class Abel | ||
Definition | df-cmn 19691* | Define class of all commutative monoids. (Contributed by Mario Carneiro, 6-Jan-2015.) |
β’ CMnd = {π β Mnd β£ βπ β (Baseβπ)βπ β (Baseβπ)(π(+gβπ)π) = (π(+gβπ)π)} | ||
Definition | df-abl 19692 | Define class of all Abelian groups. (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
β’ Abel = (Grp β© CMnd) | ||
Theorem | isabl 19693 | The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.) |
β’ (πΊ β Abel β (πΊ β Grp β§ πΊ β CMnd)) | ||
Theorem | ablgrp 19694 | An Abelian group is a group. (Contributed by NM, 26-Aug-2011.) |
β’ (πΊ β Abel β πΊ β Grp) | ||
Theorem | ablgrpd 19695 | An Abelian group is a group, deduction form of ablgrp 19694. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ (π β πΊ β Abel) β β’ (π β πΊ β Grp) | ||
Theorem | ablcmn 19696 | An Abelian group is a commutative monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
β’ (πΊ β Abel β πΊ β CMnd) | ||
Theorem | ablcmnd 19697 | An Abelian group is a commutative monoid. (Contributed by SN, 1-Jun-2024.) |
β’ (π β πΊ β Abel) β β’ (π β πΊ β CMnd) | ||
Theorem | iscmn 19698* | The predicate "is a commutative monoid". (Contributed by Mario Carneiro, 6-Jan-2015.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ (πΊ β CMnd β (πΊ β Mnd β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ + π¦) = (π¦ + π₯))) | ||
Theorem | isabl2 19699* | The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ (πΊ β Abel β (πΊ β Grp β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ + π¦) = (π¦ + π₯))) | ||
Theorem | cmnpropd 19700* | If two structures have the same group components (properties), one is a commutative monoid iff the other one is. (Contributed by Mario Carneiro, 6-Jan-2015.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) β β’ (π β (πΎ β CMnd β πΏ β CMnd)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |