P. 154 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 15301-15400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	efgmnvl 15301*	The inversion function on the generators is an involution. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   =>    |- ( A e. ( I X. 2o ) -> ( M ` ( M ` A ) ) = A )
Theorem	efgrcl 15302	Lemma for efgval 15304. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
|- W = ( _I ` Word ( I X. 2o ) )   =>    |- ( A e. W -> ( I e. _V /\ W = Word ( I X. 2o ) ) )
Theorem	efglem 15303*	Lemma for efgval 15304. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   =>    |- E. r ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) )
Theorem	efgval 15304*	Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   =>    |- .~ = |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) }
Theorem	efger 15305	Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   =>    |- .~ Er W
Theorem	efgi 15306	Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   =>    |- ( ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) ) /\ ( J e. I /\ K e. 2o ) ) -> A .~ ( A splice <. N , N , <" <. J , K >. <. J , ( 1o \ K ) >. "> >. ) )
Theorem	efgi0 15307	Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   =>    |- ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) /\ J e. I ) -> A .~ ( A splice <. N , N , <" <. J , (/) >. <. J , 1o >. "> >. ) )
Theorem	efgi1 15308	Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   =>    |- ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) /\ J e. I ) -> A .~ ( A splice <. N , N , <" <. J , 1o >. <. J , (/) >. "> >. ) )
Theorem	efgtf 15309*	Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   =>    |- ( X e. W -> ( ( T ` X ) = ( a e. ( 0 ... ( # ` X ) ) , b e. ( I X. 2o ) |-> ( X splice <. a , a , <" b ( M ` b ) "> >. ) ) /\ ( T ` X ) : ( ( 0 ... ( # ` X ) ) X. ( I X. 2o ) ) --> W ) )
Theorem	efgtval 15310*	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.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   =>    |- ( ( X e. W /\ N e. ( 0 ... ( # ` X ) ) /\ A e. ( I X. 2o ) ) -> ( N ( T ` X ) A ) = ( X splice <. N , N , <" A ( M ` A ) "> >. ) )
Theorem	efgval2 15311*	Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   =>    |- .~ = |^| { r | ( r Er W /\ A. x e. W ran ( T ` x ) C_ [ x ] r ) }
Theorem	efgi2 15312*	Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   =>    |- ( ( A e. W /\ B e. ran ( T ` A ) ) -> A .~ B )
Theorem	efgtlen 15313*	Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   =>    |- ( ( X e. W /\ A e. ran ( T ` X ) ) -> ( # ` A ) = ( ( # ` X ) + 2 ) )
Theorem	efginvrel2 15314*	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.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   =>    |- ( A e. W -> ( A concat ( M o. (reverse ` A ) ) ) .~ (/) )
Theorem	efginvrel1 15315*	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.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   =>    |- ( A e. W -> ( ( M o. (reverse ` A ) ) concat A ) .~ (/) )
Theorem	efgsf 15316*	Value of the auxiliary function S defining a sequence of extensions starting at some irreducible word. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   =>    |- S : { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } --> W
Theorem	efgsdm 15317*	Elementhood in the domain of S, the set of sequences of extensions starting at an irreducible word. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   =>    |- ( F e. dom S <-> ( F e. (Word W \ { (/) } ) /\ ( F ` 0 ) e. D /\ A. i e. ( 1..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) )
Theorem	efgsval 15318*	Value of the auxiliary function S defining a sequence of extensions (Contributed by Mario Carneiro, 27-Sep-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   =>    |- ( F e. dom S -> ( S ` F ) = ( F ` ( ( # ` F ) - 1 ) ) )
Theorem	efgsdmi 15319*	Property of the last link in the chain of extensions. (Contributed by Mario Carneiro, 29-Sep-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   =>    |- ( ( F e. dom S /\ ( ( # ` F ) - 1 ) e. NN ) -> ( S ` F ) e. ran ( T ` ( F ` ( ( ( # ` F ) - 1 ) - 1 ) ) ) )
Theorem	efgsval2 15320*	Value of the auxiliary function S defining a sequence of extensions (Contributed by Mario Carneiro, 1-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   =>    |- ( ( A e. Word W /\ B e. W /\ ( A concat <" B "> ) e. dom S ) -> ( S ` ( A concat <" B "> ) ) = B )
Theorem	efgsrel 15321*	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.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   =>    |- ( F e. dom S -> ( F ` 0 ) .~ ( S ` F ) )
Theorem	efgs1 15322*	A singleton of an irreducible word is an extension sequence. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   =>    |- ( A e. D -> <" A "> e. dom S )
Theorem	efgs1b 15323*	Every extension sequence ending in an irreducible word is trivial. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   =>    |- ( A e. dom S -> ( ( S ` A ) e. D <-> ( # ` A ) = 1 ) )
Theorem	efgsp1 15324*	If F is an extension sequence and A is an extension of the last element of F, then F + <" A "> is an extension sequence. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   =>    |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( F concat <" A "> ) e. dom S )
Theorem	efgsres 15325*	An initial segment of an extension sequence is an extension sequence. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   =>    |- ( ( F e. dom S /\ N e. ( 1 ... ( # ` F ) ) ) -> ( F |` ( 0..^ N ) ) e. dom S )
Theorem	efgsfo 15326*	For any word, there is a sequence of extensions starting at a reduced word and ending at the target word, such that each word in the chain is an extension of the previous (inserting an element and its inverse at adjacent indexes somewhere in the sequence). (Contributed by Mario Carneiro, 27-Sep-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   =>    |- S : dom S -onto-> W
Theorem	efgredlema 15327*	The reduced word that forms the base of the sequence in efgsval 15318 is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   &    |- ( ph -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )   &    |- ( ph -> A e. dom S )   &    |- ( ph -> B e. dom S )   &    |- ( ph -> ( S ` A ) = ( S ` B ) )   &    |- ( ph -> -. ( A ` 0 ) = ( B ` 0 ) )   =>    |- ( ph -> ( ( ( # ` A ) - 1 ) e. NN /\ ( ( # ` B ) - 1 ) e. NN ) )
Theorem	efgredlemf 15328*	Lemma for efgredleme 15330. (Contributed by Mario Carneiro, 4-Jun-2016.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   &    |- ( ph -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )   &    |- ( ph -> A e. dom S )   &    |- ( ph -> B e. dom S )   &    |- ( ph -> ( S ` A ) = ( S ` B ) )   &    |- ( ph -> -. ( A ` 0 ) = ( B ` 0 ) )   &    |- K = ( ( ( # ` A ) - 1 ) - 1 )   &    |- L = ( ( ( # ` B ) - 1 ) - 1 )   =>    |- ( ph -> ( ( A ` K ) e. W /\ ( B ` L ) e. W ) )
Theorem	efgredlemg 15329*	Lemma for efgred 15335. (Contributed by Mario Carneiro, 4-Jun-2016.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   &    |- ( ph -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )   &    |- ( ph -> A e. dom S )   &    |- ( ph -> B e. dom S )   &    |- ( ph -> ( S ` A ) = ( S ` B ) )   &    |- ( ph -> -. ( A ` 0 ) = ( B ` 0 ) )   &    |- K = ( ( ( # ` A ) - 1 ) - 1 )   &    |- L = ( ( ( # ` B ) - 1 ) - 1 )   &    |- ( ph -> P e. ( 0 ... ( # ` ( A ` K ) ) ) )   &    |- ( ph -> Q e. ( 0 ... ( # ` ( B ` L ) ) ) )   &    |- ( ph -> U e. ( I X. 2o ) )   &    |- ( ph -> V e. ( I X. 2o ) )   &    |- ( ph -> ( S ` A ) = ( P ( T ` ( A ` K ) ) U ) )   &    |- ( ph -> ( S ` B ) = ( Q ( T ` ( B ` L ) ) V ) )   =>    |- ( ph -> ( # ` ( A ` K ) ) = ( # ` ( B ` L ) ) )
Theorem	efgredleme 15330*	Lemma for efgred 15335. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   &    |- ( ph -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )   &    |- ( ph -> A e. dom S )   &    |- ( ph -> B e. dom S )   &    |- ( ph -> ( S ` A ) = ( S ` B ) )   &    |- ( ph -> -. ( A ` 0 ) = ( B ` 0 ) )   &    |- K = ( ( ( # ` A ) - 1 ) - 1 )   &    |- L = ( ( ( # ` B ) - 1 ) - 1 )   &    |- ( ph -> P e. ( 0 ... ( # ` ( A ` K ) ) ) )   &    |- ( ph -> Q e. ( 0 ... ( # ` ( B ` L ) ) ) )   &    |- ( ph -> U e. ( I X. 2o ) )   &    |- ( ph -> V e. ( I X. 2o ) )   &    |- ( ph -> ( S ` A ) = ( P ( T ` ( A ` K ) ) U ) )   &    |- ( ph -> ( S ` B ) = ( Q ( T ` ( B ` L ) ) V ) )   &    |- ( ph -> -. ( A ` K ) = ( B ` L ) )   &    |- ( ph -> P e. ( ZZ>= ` ( Q + 2 ) ) )   &    |- ( ph -> C e. dom S )   &    |- ( ph -> ( S ` C ) = ( ( ( B ` L ) substr <. 0 , Q >. ) concat ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) )   =>    |- ( ph -> ( ( A ` K ) e. ran ( T ` ( S ` C ) ) /\ ( B ` L ) e. ran ( T ` ( S ` C ) ) ) )
Theorem	efgredlemd 15331*	The reduced word that forms the base of the sequence in efgsval 15318 is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   &    |- ( ph -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )   &    |- ( ph -> A e. dom S )   &    |- ( ph -> B e. dom S )   &    |- ( ph -> ( S ` A ) = ( S ` B ) )   &    |- ( ph -> -. ( A ` 0 ) = ( B ` 0 ) )   &    |- K = ( ( ( # ` A ) - 1 ) - 1 )   &    |- L = ( ( ( # ` B ) - 1 ) - 1 )   &    |- ( ph -> P e. ( 0 ... ( # ` ( A ` K ) ) ) )   &    |- ( ph -> Q e. ( 0 ... ( # ` ( B ` L ) ) ) )   &    |- ( ph -> U e. ( I X. 2o ) )   &    |- ( ph -> V e. ( I X. 2o ) )   &    |- ( ph -> ( S ` A ) = ( P ( T ` ( A ` K ) ) U ) )   &    |- ( ph -> ( S ` B ) = ( Q ( T ` ( B ` L ) ) V ) )   &    |- ( ph -> -. ( A ` K ) = ( B ` L ) )   &    |- ( ph -> P e. ( ZZ>= ` ( Q + 2 ) ) )   &    |- ( ph -> C e. dom S )   &    |- ( ph -> ( S ` C ) = ( ( ( B ` L ) substr <. 0 , Q >. ) concat ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) )   =>    |- ( ph -> ( A ` 0 ) = ( B ` 0 ) )
Theorem	efgredlemc 15332*	The reduced word that forms the base of the sequence in efgsval 15318 is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   &    |- ( ph -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )   &    |- ( ph -> A e. dom S )   &    |- ( ph -> B e. dom S )   &    |- ( ph -> ( S ` A ) = ( S ` B ) )   &    |- ( ph -> -. ( A ` 0 ) = ( B ` 0 ) )   &    |- K = ( ( ( # ` A ) - 1 ) - 1 )   &    |- L = ( ( ( # ` B ) - 1 ) - 1 )   &    |- ( ph -> P e. ( 0 ... ( # ` ( A ` K ) ) ) )   &    |- ( ph -> Q e. ( 0 ... ( # ` ( B ` L ) ) ) )   &    |- ( ph -> U e. ( I X. 2o ) )   &    |- ( ph -> V e. ( I X. 2o ) )   &    |- ( ph -> ( S ` A ) = ( P ( T ` ( A ` K ) ) U ) )   &    |- ( ph -> ( S ` B ) = ( Q ( T ` ( B ` L ) ) V ) )   &    |- ( ph -> -. ( A ` K ) = ( B ` L ) )   =>    |- ( ph -> ( P e. ( ZZ>= ` Q ) -> ( A ` 0 ) = ( B ` 0 ) ) )
Theorem	efgredlemb 15333*	The reduced word that forms the base of the sequence in efgsval 15318 is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 30-Sep-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   &    |- ( ph -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )   &    |- ( ph -> A e. dom S )   &    |- ( ph -> B e. dom S )   &    |- ( ph -> ( S ` A ) = ( S ` B ) )   &    |- ( ph -> -. ( A ` 0 ) = ( B ` 0 ) )   &    |- K = ( ( ( # ` A ) - 1 ) - 1 )   &    |- L = ( ( ( # ` B ) - 1 ) - 1 )   &    |- ( ph -> P e. ( 0 ... ( # ` ( A ` K ) ) ) )   &    |- ( ph -> Q e. ( 0 ... ( # ` ( B ` L ) ) ) )   &    |- ( ph -> U e. ( I X. 2o ) )   &    |- ( ph -> V e. ( I X. 2o ) )   &    |- ( ph -> ( S ` A ) = ( P ( T ` ( A ` K ) ) U ) )   &    |- ( ph -> ( S ` B ) = ( Q ( T ` ( B ` L ) ) V ) )   &    |- ( ph -> -. ( A ` K ) = ( B ` L ) )   =>    |- -. ph
Theorem	efgredlem 15334*	The reduced word that forms the base of the sequence in efgsval 15318 is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 30-Sep-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   &    |- ( ph -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )   &    |- ( ph -> A e. dom S )   &    |- ( ph -> B e. dom S )   &    |- ( ph -> ( S ` A ) = ( S ` B ) )   &    |- ( ph -> -. ( A ` 0 ) = ( B ` 0 ) )   =>    |- -. ph
Theorem	efgred 15335*	The reduced word that forms the base of the sequence in efgsval 15318 is uniquely determined, given the terminal point. (Contributed by Mario Carneiro, 28-Sep-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   =>    |- ( ( A e. dom S /\ B e. dom S /\ ( S ` A ) = ( S ` B ) ) -> ( A ` 0 ) = ( B ` 0 ) )
Theorem	efgrelexlema 15336*	If two words A , B are related under the free group equivalence, then there exist two extension sequences a , b such that a ends at A, b ends at B, and a and B have the same starting point. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   &    |- L = { <. i , j >. | E. c e. ( `' S " { i } ) E. d e. ( `' S " { j } ) ( c ` 0 ) = ( d ` 0 ) }   =>    |- ( A L B <-> E. a e. ( `' S " { A } ) E. b e. ( `' S " { B } ) ( a ` 0 ) = ( b ` 0 ) )
Theorem	efgrelexlemb 15337*	If two words A , B are related under the free group equivalence, then there exist two extension sequences a , b such that a ends at A, b ends at B, and a and B have the same starting point. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   &    |- L = { <. i , j >. | E. c e. ( `' S " { i } ) E. d e. ( `' S " { j } ) ( c ` 0 ) = ( d ` 0 ) }   =>    |- .~ C_ L
Theorem	efgrelex 15338*	If two words A , B are related under the free group equivalence, then there exist two extension sequences a , b such that a ends at A, b ends at B, and a and B have the same starting point. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   =>    |- ( A .~ B -> E. a e. ( `' S " { A } ) E. b e. ( `' S " { B } ) ( a ` 0 ) = ( b ` 0 ) )
Theorem	efgredeu 15339*	There is a unique reduced word equivalent to a given word. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   =>    |- ( A e. W -> E! d e. D d .~ A )
Theorem	efgred2 15340*	Two extension sequences have related endpoints iff they have the same base. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   =>    |- ( ( A e. dom S /\ B e. dom S ) -> ( ( S ` A ) .~ ( S ` B ) <-> ( A ` 0 ) = ( B ` 0 ) ) )
Theorem	efgcpbllema 15341*	Lemma for efgrelex 15338. Define an auxiliary equivalence relation L such that A L B if there are sequences from A to B passing through the same reduced word. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   &    |- L = { <. i , j >. | ( { i , j } C_ W /\ ( ( A concat i ) concat B ) .~ ( ( A concat j ) concat B ) ) }   =>    |- ( X L Y <-> ( X e. W /\ Y e. W /\ ( ( A concat X ) concat B ) .~ ( ( A concat Y ) concat B ) ) )
Theorem	efgcpbllemb 15342*	Lemma for efgrelex 15338. Show that L is an equivalence relation containing all direct extensions of a word, so is closed under .~. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   &    |- L = { <. i , j >. | ( { i , j } C_ W /\ ( ( A concat i ) concat B ) .~ ( ( A concat j ) concat B ) ) }   =>    |- ( ( A e. W /\ B e. W ) -> .~ C_ L )
Theorem	efgcpbl 15343*	Two extension sequences have related endpoints iff they have the same base. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   =>    |- ( ( A e. W /\ B e. W /\ X .~ Y ) -> ( ( A concat X ) concat B ) .~ ( ( A concat Y ) concat B ) )
Theorem	efgcpbl2 15344*	Two extension sequences have related endpoints iff they have the same base. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   &    |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )   &    |- D = ( W \ U_ x e. W ran ( T ` x ) )   &    |- S = ( m e. { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )   =>    |- ( ( A .~ X /\ B .~ Y ) -> ( A concat B ) .~ ( X concat Y ) )
Theorem	frgpval 15345	Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- G = (freeGrp ` I )   &    |- M = (freeMnd ` ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   =>    |- ( I e. V -> G = ( M /.s .~ ) )
Theorem	frgpcpbl 15346	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.)
|- G = (freeGrp ` I )   &    |- M = (freeMnd ` ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- .+ = ( +g ` M )   =>    |- ( ( A .~ C /\ B .~ D ) -> ( A .+ B ) .~ ( C .+ D ) )
Theorem	frgp0 15347	The free group is a group. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
|- G = (freeGrp ` I )   &    |- .~ = ( ~FG ` I )   =>    |- ( I e. V -> ( G e. Grp /\ [ (/) ] .~ = ( 0g ` G ) ) )
Theorem	frgpeccl 15348	Closure of the quotient map in a free group. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- G = (freeGrp ` I )   &    |- .~ = ( ~FG ` I )   &    |- W = ( _I ` Word ( I X. 2o ) )   &    |- B = ( Base ` G )   =>    |- ( X e. W -> [ X ] .~ e. B )
Theorem	frgpgrp 15349	The free group is a group. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- G = (freeGrp ` I )   =>    |- ( I e. V -> G e. Grp )
Theorem	frgpadd 15350	Addition in the free group is given by concatenation. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- G = (freeGrp ` I )   &    |- .~ = ( ~FG ` I )   &    |- .+ = ( +g ` G )   =>    |- ( ( A e. W /\ B e. W ) -> ( [ A ] .~ .+ [ B ] .~ ) = [ ( A concat B ) ] .~ )
Theorem	frgpinv 15351*	The inverse of an element of the free group. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- W = ( _I ` Word ( I X. 2o ) )   &    |- G = (freeGrp ` I )   &    |- .~ = ( ~FG ` I )   &    |- N = ( inv g ` G )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   =>    |- ( A e. W -> ( N ` [ A ] .~ ) = [ ( M o. (reverse ` A ) ) ] .~ )
Theorem	frgpmhm 15352*	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.)
|- M = (freeMnd ` ( I X. 2o ) )   &    |- W = ( Base ` M )   &    |- G = (freeGrp ` I )   &    |- .~ = ( ~FG ` I )   &    |- F = ( x e. W |-> [ x ] .~ )   =>    |- ( I e. V -> F e. ( M MndHom G ) )
Theorem	vrgpfval 15353*	The canonical injection from the generating set I to the base set of the free group. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- .~ = ( ~FG ` I )   &    |- U = (varFGrp ` I )   =>    |- ( I e. V -> U = ( j e. I |-> [ <" <. j , (/) >. "> ] .~ ) )
Theorem	vrgpval 15354	The value of the generating elements of a free group. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- .~ = ( ~FG ` I )   &    |- U = (varFGrp ` I )   =>    |- ( ( I e. V /\ A e. I ) -> ( U ` A ) = [ <" <. A , (/) >. "> ] .~ )
Theorem	vrgpf 15355	The mapping from the index set to the generators is a function into the free group. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- .~ = ( ~FG ` I )   &    |- U = (varFGrp ` I )   &    |- G = (freeGrp ` I )   &    |- X = ( Base ` G )   =>    |- ( I e. V -> U : I --> X )
Theorem	vrgpinv 15356	The inverse of a generating element is represented by <. A , 1 >. instead of <. A , 0 >.. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- .~ = ( ~FG ` I )   &    |- U = (varFGrp ` I )   &    |- G = (freeGrp ` I )   &    |- N = ( inv g ` G )   =>    |- ( ( I e. V /\ A e. I ) -> ( N ` ( U ` A ) ) = [ <" <. A , 1o >. "> ] .~ )
Theorem	frgpuptf 15357*	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.)
|- B = ( Base ` H )   &    |- N = ( inv g ` H )   &    |- T = ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) )   &    |- ( ph -> H e. Grp )   &    |- ( ph -> I e. V )   &    |- ( ph -> F : I --> B )   =>    |- ( ph -> T : ( I X. 2o ) --> B )
Theorem	frgpuptinv 15358*	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.)
|- B = ( Base ` H )   &    |- N = ( inv g ` H )   &    |- T = ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) )   &    |- ( ph -> H e. Grp )   &    |- ( ph -> I e. V )   &    |- ( ph -> F : I --> B )   &    |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   =>    |- ( ( ph /\ A e. ( I X. 2o ) ) -> ( T ` ( M ` A ) ) = ( N ` ( T ` A ) ) )
Theorem	frgpuplem 15359*	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.)
|- B = ( Base ` H )   &    |- N = ( inv g ` H )   &    |- T = ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) )   &    |- ( ph -> H e. Grp )   &    |- ( ph -> I e. V )   &    |- ( ph -> F : I --> B )   &    |- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   =>    |- ( ( ph /\ A .~ C ) -> ( H gsumg ( T o. A ) ) = ( H gsumg ( T o. C ) ) )
Theorem	frgpupf 15360*	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.)
|- B = ( Base ` H )   &    |- N = ( inv g ` H )   &    |- T = ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) )   &    |- ( ph -> H e. Grp )   &    |- ( ph -> I e. V )   &    |- ( ph -> F : I --> B )   &    |- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- G = (freeGrp ` I )   &    |- X = ( Base ` G )   &    |- E = ran ( g e. W |-> <. [ g ] .~ , ( H gsumg ( T o. g ) ) >. )   =>    |- ( ph -> E : X --> B )
Theorem	frgpupval 15361*	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.)
|- B = ( Base ` H )   &    |- N = ( inv g ` H )   &    |- T = ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) )   &    |- ( ph -> H e. Grp )   &    |- ( ph -> I e. V )   &    |- ( ph -> F : I --> B )   &    |- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- G = (freeGrp ` I )   &    |- X = ( Base ` G )   &    |- E = ran ( g e. W |-> <. [ g ] .~ , ( H gsumg ( T o. g ) ) >. )   =>    |- ( ( ph /\ A e. W ) -> ( E ` [ A ] .~ ) = ( H gsumg ( T o. A ) ) )
Theorem	frgpup1 15362*	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.)
|- B = ( Base ` H )   &    |- N = ( inv g ` H )   &    |- T = ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) )   &    |- ( ph -> H e. Grp )   &    |- ( ph -> I e. V )   &    |- ( ph -> F : I --> B )   &    |- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- G = (freeGrp ` I )   &    |- X = ( Base ` G )   &    |- E = ran ( g e. W |-> <. [ g ] .~ , ( H gsumg ( T o. g ) ) >. )   =>    |- ( ph -> E e. ( G GrpHom H ) )
Theorem	frgpup2 15363*	The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)
|- B = ( Base ` H )   &    |- N = ( inv g ` H )   &    |- T = ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) )   &    |- ( ph -> H e. Grp )   &    |- ( ph -> I e. V )   &    |- ( ph -> F : I --> B )   &    |- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- G = (freeGrp ` I )   &    |- X = ( Base ` G )   &    |- E = ran ( g e. W |-> <. [ g ] .~ , ( H gsumg ( T o. g ) ) >. )   &    |- U = (varFGrp ` I )   &    |- ( ph -> A e. I )   =>    |- ( ph -> ( E ` ( U ` A ) ) = ( F ` A ) )
Theorem	frgpup3lem 15364*	The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)
|- B = ( Base ` H )   &    |- N = ( inv g ` H )   &    |- T = ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) )   &    |- ( ph -> H e. Grp )   &    |- ( ph -> I e. V )   &    |- ( ph -> F : I --> B )   &    |- W = ( _I ` Word ( I X. 2o ) )   &    |- .~ = ( ~FG ` I )   &    |- G = (freeGrp ` I )   &    |- X = ( Base ` G )   &    |- E = ran ( g e. W |-> <. [ g ] .~ , ( H gsumg ( T o. g ) ) >. )   &    |- U = (varFGrp ` I )   &    |- ( ph -> K e. ( G GrpHom H ) )   &    |- ( ph -> ( K o. U ) = F )   =>    |- ( ph -> K = E )
Theorem	frgpup3 15365*	Universal property of the free monoid by existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)
|- G = (freeGrp ` I )   &    |- B = ( Base ` H )   &    |- U = (varFGrp ` I )   =>    |- ( ( H e. Grp /\ I e. V /\ F : I --> B ) -> E! m e. ( G GrpHom H ) ( m o. U ) = F )
Theorem	0frgp 15366	The free group on zero generators is trivial. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- G = (freeGrp ` (/) )   &    |- B = ( Base ` G )   =>    |- B ~~ 1o
10.3  Abelian groups
10.3.1  Definition and basic properties
Syntax	ccmn 15367	Extend class notation with class of all commutative monoids.
class CMnd
Syntax	cabel 15368	Extend class notation with class of all Abelian groups.
class Abel
Definition	df-cmn 15369*	Define class of all commutative monoids. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- CMnd = { g e. Mnd | A. a e. ( Base ` g ) A. b e. ( Base ` g ) ( a ( +g ` g ) b ) = ( b ( +g ` g ) a ) }
Definition	df-abl 15370	Define class of all Abelian groups. (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- Abel = ( Grp i^i CMnd )
Theorem	isabl 15371	The predicate "is an Abelian (commutative) group." (Contributed by NM, 17-Oct-2011.)
|- ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )
Theorem	ablgrp 15372	An Abelian group is a group. (Contributed by NM, 26-Aug-2011.)
|- ( G e. Abel -> G e. Grp )
Theorem	ablcmn 15373	An Abelian group is a commutative monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( G e. Abel -> G e. CMnd )
Theorem	iscmn 15374*	The predicate "is a commutative monoid." (Contributed by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. CMnd <-> ( G e. Mnd /\ A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) ) )
Theorem	isabl2 15375*	The predicate "is an Abelian (commutative) group." (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. Abel <-> ( G e. Grp /\ A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) ) )
Theorem	cmnpropd 15376*	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.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   =>    |- ( ph -> ( K e. CMnd <-> L e. CMnd ) )
Theorem	ablpropd 15377*	If two structures have the same group components (properties), one is an Abelian group iff the other one is. (Contributed by NM, 6-Dec-2014.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   =>    |- ( ph -> ( K e. Abel <-> L e. Abel ) )
Theorem	ablprop 15378	If two structures have the same group components (properties), one is an Abelian group iff the other one is. (Contributed by NM, 11-Oct-2013.)
|- ( Base ` K ) = ( Base ` L )   &    |- ( +g ` K ) = ( +g ` L )   =>    |- ( K e. Abel <-> L e. Abel )
Theorem	iscmnd 15379*	Properties that determine a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ph -> G e. Mnd )   &    |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) = ( y .+ x ) )   =>    |- ( ph -> G e. CMnd )
Theorem	isabld 15380*	Properties that determine an Abelian group. (Contributed by NM, 6-Aug-2013.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ph -> G e. Grp )   &    |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) = ( y .+ x ) )   =>    |- ( ph -> G e. Abel )
Theorem	isabli 15381*	Properties that determine an Abelian group. (Contributed by NM, 4-Sep-2011.)
|- G e. Grp   &    |- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ( x e. B /\ y e. B ) -> ( x .+ y ) = ( y .+ x ) )   =>    |- G e. Abel
Theorem	cmnmnd 15382	A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( G e. CMnd -> G e. Mnd )
Theorem	cmncom 15383	A commutative monoid is commutative. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. CMnd /\ X e. B /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )
Theorem	ablcom 15384	An Abelian group operation is commutative. (Contributed by NM, 26-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )
Theorem	cmn32 15385	Commutative/associative law for Abelian groups. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. CMnd /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .+ Z ) = ( ( X .+ Z ) .+ Y ) )
Theorem	cmn4 15386	Commutative/associative law for Abelian groups. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. CMnd /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .+ ( Z .+ W ) ) = ( ( X .+ Z ) .+ ( Y .+ W ) ) )
Theorem	cmn12 15387	Commutative/associative law for Abelian monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. CMnd /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .+ ( Y .+ Z ) ) = ( Y .+ ( X .+ Z ) ) )
Theorem	abl32 15388	Commutative/associative law for Abelian groups. (Contributed by Stefan O'Rear, 10-Apr-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .+ Y ) .+ Z ) = ( ( X .+ Z ) .+ Y ) )
Theorem	ablinvadd 15389	The inverse of an Abelian group operation. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- N = ( inv g ` G )   =>    |- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> ( N ` ( X .+ Y ) ) = ( ( N ` X ) .+ ( N ` Y ) ) )
Theorem	ablsub2inv 15390	Abelian group subtraction of two inverses. (Contributed by Stefan O'Rear, 24-May-2015.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- N = ( inv g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( N ` X ) .- ( N ` Y ) ) = ( Y .- X ) )
Theorem	ablsubadd 15391	Relationship between Abelian group subtraction and addition. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .- Y ) = Z <-> ( Y .+ Z ) = X ) )
Theorem	ablsub4 15392	Commutative/associative subtraction law for Abelian groups. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .- ( Z .+ W ) ) = ( ( X .- Z ) .+ ( Y .- W ) ) )
Theorem	abladdsub4 15393	Abelian group addition/subtraction law. (Contributed by NM, 31-Mar-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) = ( Z .+ W ) <-> ( X .- Z ) = ( W .- Y ) ) )
Theorem	abladdsub 15394	Associative-type law for group subtraction and addition. (Contributed by NM, 19-Apr-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .- Z ) = ( ( X .- Z ) .+ Y ) )
Theorem	ablpncan2 15395	Cancellation law for subtraction. (Contributed by NM, 2-Oct-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ X e. B /\ Y e. B ) -> ( ( X .+ Y ) .- X ) = Y )
Theorem	ablpncan3 15396	A cancellation law for commutative groups. (Contributed by NM, 23-Mar-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ( G e. Abel /\ ( X e. B /\ Y e. B ) ) -> ( X .+ ( Y .- X ) ) = Y )
Theorem	ablsubsub 15397	Law for double subtraction. (Contributed by NM, 7-Apr-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( X .- ( Y .- Z ) ) = ( ( X .- Y ) .+ Z ) )
Theorem	ablsubsub4 15398	Law for double subtraction. (Contributed by NM, 7-Apr-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .- Y ) .- Z ) = ( X .- ( Y .+ Z ) ) )
Theorem	ablpnpcan 15399	Cancellation law for mixed addition and subtraction. (pnpcan 9296 analog.) (Contributed by NM, 29-May-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .+ Y ) .- ( X .+ Z ) ) = ( Y .- Z ) )
Theorem	ablnncan 15400	Cancellation law for group division. (nncan 9286 analog.) (Contributed by NM, 7-Apr-2015.)
|- B = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .- ( X .- Y ) ) = Y )