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	lsmss2b 15301	Subgroup sum with a subset. (Contributed by NM, 10-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .(+) = ( LSSum ` G )   =>    |- ( ( T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) ) -> ( U C_ T <-> ( T .(+) U ) = T ) )
Theorem	lsmass 15302	Subgroup sum is associative. (Contributed by NM, 2-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .(+) = ( LSSum ` G )   =>    |- ( ( R e. (SubGrp ` G ) /\ T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) ) -> ( ( R .(+) T ) .(+) U ) = ( R .(+) ( T .(+) U ) ) )
Theorem	lsm01 15303	Subgroup sum with the zero subgroup. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .0. = ( 0g ` G )   &    |- .(+) = ( LSSum ` G )   =>    |- ( X e. (SubGrp ` G ) -> ( X .(+) { .0. } ) = X )
Theorem	lsm02 15304	Subgroup sum with the zero subgroup. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .0. = ( 0g ` G )   &    |- .(+) = ( LSSum ` G )   =>    |- ( X e. (SubGrp ` G ) -> ( { .0. } .(+) X ) = X )
Theorem	subglsm 15305	The subgroup sum evaluated within a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.)
|- H = ( G ↾s S )   &    |- .(+) = ( LSSum ` G )   &    |- A = ( LSSum ` H )   =>    |- ( ( S e. (SubGrp ` G ) /\ T C_ S /\ U C_ S ) -> ( T .(+) U ) = ( T A U ) )
Theorem	lssnle 15306	Equivalent expressions for "not less than". (chnlei 22987 analog.) (Contributed by NM, 10-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   =>    |- ( ph -> ( -. U C_ T <-> T C. ( T .(+) U ) ) )
Theorem	lsmmod 15307	The modular law holds for subgroup sum. Similar to part of Theorem 16.9 of [MaedaMaeda] p. 70. (Contributed by NM, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .(+) = ( LSSum ` G )   =>    |- ( ( ( S e. (SubGrp ` G ) /\ T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) ) /\ S C_ U ) -> ( S .(+) ( T i^i U ) ) = ( ( S .(+) T ) i^i U ) )
Theorem	lsmmod2 15308	Modular law dual for subgroup sum. Similar to part of Theorem 16.9 of [MaedaMaeda] p. 70. (Contributed by NM, 8-Jan-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- .(+) = ( LSSum ` G )   =>    |- ( ( ( S e. (SubGrp ` G ) /\ T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) ) /\ U C_ S ) -> ( S i^i ( T .(+) U ) ) = ( ( S i^i T ) .(+) U ) )
Theorem	lsmpropd 15309*	If two structures have the same components (properties), they have the same subspace structure. (Contributed by Mario Carneiro, 29-Jun-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. _V )   &    |- ( ph -> L e. _V )   =>    |- ( ph -> ( LSSum ` K ) = ( LSSum ` L ) )
Theorem	cntzrecd 15310	Commute the "subgroups commute" predicate. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> T C_ ( Z ` U ) )   =>    |- ( ph -> U C_ ( Z ` T ) )
Theorem	lsmcntz 15311	The "subgroups commute" predicate applied to a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- Z = (Cntz ` G )   =>    |- ( ph -> ( ( S .(+) T ) C_ ( Z ` U ) <-> ( S C_ ( Z ` U ) /\ T C_ ( Z ` U ) ) ) )
Theorem	lsmcntzr 15312	The "subgroups commute" predicate applied to a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- Z = (Cntz ` G )   =>    |- ( ph -> ( S C_ ( Z ` ( T .(+) U ) ) <-> ( S C_ ( Z ` T ) /\ S C_ ( Z ` U ) ) ) )
Theorem	lsmdisj 15313	Disjointness from a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> ( ( S .(+) T ) i^i U ) = { .0. } )   =>    |- ( ph -> ( ( S i^i U ) = { .0. } /\ ( T i^i U ) = { .0. } ) )
Theorem	lsmdisj2 15314	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 22-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> ( ( S .(+) T ) i^i U ) = { .0. } )   &    |- ( ph -> ( S i^i T ) = { .0. } )   =>    |- ( ph -> ( T i^i ( S .(+) U ) ) = { .0. } )
Theorem	lsmdisj3 15315	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> ( ( S .(+) T ) i^i U ) = { .0. } )   &    |- ( ph -> ( S i^i T ) = { .0. } )   &    |- Z = (Cntz ` G )   &    |- ( ph -> S C_ ( Z ` T ) )   =>    |- ( ph -> ( S i^i ( T .(+) U ) ) = { .0. } )
Theorem	lsmdisjr 15316	Disjointness from a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> ( S i^i ( T .(+) U ) ) = { .0. } )   =>    |- ( ph -> ( ( S i^i T ) = { .0. } /\ ( S i^i U ) = { .0. } ) )
Theorem	lsmdisj2r 15317	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 22-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> ( S i^i ( T .(+) U ) ) = { .0. } )   &    |- ( ph -> ( T i^i U ) = { .0. } )   =>    |- ( ph -> ( ( S .(+) U ) i^i T ) = { .0. } )
Theorem	lsmdisj3r 15318	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 22-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> ( S i^i ( T .(+) U ) ) = { .0. } )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T C_ ( Z ` U ) )   =>    |- ( ph -> ( ( S .(+) T ) i^i U ) = { .0. } )
Theorem	lsmdisj2a 15319	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- .0. = ( 0g ` G )   =>    |- ( ph -> ( ( ( ( S .(+) T ) i^i U ) = { .0. } /\ ( S i^i T ) = { .0. } ) <-> ( ( T i^i ( S .(+) U ) ) = { .0. } /\ ( S i^i U ) = { .0. } ) ) )
Theorem	lsmdisj2b 15320	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- .0. = ( 0g ` G )   =>    |- ( ph -> ( ( ( ( S .(+) U ) i^i T ) = { .0. } /\ ( S i^i U ) = { .0. } ) <-> ( ( S i^i ( T .(+) U ) ) = { .0. } /\ ( T i^i U ) = { .0. } ) ) )
Theorem	lsmdisj3a 15321	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> S C_ ( Z ` T ) )   =>    |- ( ph -> ( ( ( ( S .(+) T ) i^i U ) = { .0. } /\ ( S i^i T ) = { .0. } ) <-> ( ( S i^i ( T .(+) U ) ) = { .0. } /\ ( T i^i U ) = { .0. } ) ) )
Theorem	lsmdisj3b 15322	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T C_ ( Z ` U ) )   =>    |- ( ph -> ( ( ( ( S .(+) T ) i^i U ) = { .0. } /\ ( S i^i T ) = { .0. } ) <-> ( ( S i^i ( T .(+) U ) ) = { .0. } /\ ( T i^i U ) = { .0. } ) ) )
Theorem	subgdisj1 15323	Vectors belonging to disjoint commuting subgroups are uniquely determined by their sum. (Contributed by NM, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- ( ph -> A e. T )   &    |- ( ph -> C e. T )   &    |- ( ph -> B e. U )   &    |- ( ph -> D e. U )   &    |- ( ph -> ( A .+ B ) = ( C .+ D ) )   =>    |- ( ph -> A = C )
Theorem	subgdisj2 15324	Vectors belonging to disjoint subgroups are uniquely determined by their sum. (Contributed by NM, 12-Jul-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- ( ph -> A e. T )   &    |- ( ph -> C e. T )   &    |- ( ph -> B e. U )   &    |- ( ph -> D e. U )   &    |- ( ph -> ( A .+ B ) = ( C .+ D ) )   =>    |- ( ph -> B = D )
Theorem	subgdisjb 15325	Vectors belonging to disjoint subgroups are uniquely determined by their sum. Analogous to opth 4435, 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 ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- ( ph -> A e. T )   &    |- ( ph -> C e. T )   &    |- ( ph -> B e. U )   &    |- ( ph -> D e. U )   =>    |- ( ph -> ( ( A .+ B ) = ( C .+ D ) <-> ( A = C /\ B = D ) ) )
Theorem	pj1fval 15326*	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.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- P = ( proj 1 ` G )   =>    |- ( ( G e. V /\ T C_ B /\ U C_ B ) -> ( T P U ) = ( z e. ( T .(+) U ) |-> ( iota_ x e. T E. y e. U z = ( x .+ y ) ) ) )
Theorem	pj1val 15327*	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.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- P = ( proj 1 ` G )   =>    |- ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ X e. ( T .(+) U ) ) -> ( ( T P U ) ` X ) = ( iota_ x e. T E. y e. U X = ( x .+ y ) ) )
Theorem	pj1eu 15328*	Uniqueness of a left projection. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   =>    |- ( ( ph /\ X e. ( T .(+) U ) ) -> E! x e. T E. y e. U X = ( x .+ y ) )
Theorem	pj1f 15329	The left projection function maps a direct subspace sum onto the left factor. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- P = ( proj 1 ` G )   =>    |- ( ph -> ( T P U ) : ( T .(+) U ) --> T )
Theorem	pj2f 15330	The right projection function maps a direct subspace sum onto the right factor. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- P = ( proj 1 ` G )   =>    |- ( ph -> ( U P T ) : ( T .(+) U ) --> U )
Theorem	pj1id 15331	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 ` G )   &    |- .(+) = ( LSSum ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- P = ( proj 1 ` G )   =>    |- ( ( ph /\ X e. ( T .(+) U ) ) -> X = ( ( ( T P U ) ` X ) .+ ( ( U P T ) ` X ) ) )
Theorem	pj1eq 15332	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 ` G )   &    |- .(+) = ( LSSum ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- P = ( proj 1 ` G )   &    |- ( ph -> X e. ( T .(+) U ) )   &    |- ( ph -> B e. T )   &    |- ( ph -> C e. U )   =>    |- ( ph -> ( X = ( B .+ C ) <-> ( ( ( T P U ) ` X ) = B /\ ( ( U P T ) ` X ) = C ) ) )
Theorem	pj1lid 15333	The left projection function is the identity on the left subspace. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- P = ( proj 1 ` G )   =>    |- ( ( ph /\ X e. T ) -> ( ( T P U ) ` X ) = X )
Theorem	pj1rid 15334	The left projection function is the zero operator on the right subspace. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- P = ( proj 1 ` G )   =>    |- ( ( ph /\ X e. U ) -> ( ( T P U ) ` X ) = .0. )
Theorem	pj1ghm 15335	The left projection function is a group homomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- P = ( proj 1 ` G )   =>    |- ( ph -> ( T P U ) e. ( ( G ↾s ( T .(+) U ) ) GrpHom G ) )
Theorem	pj1ghm2 15336	The left projection function is a group homomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- P = ( proj 1 ` G )   =>    |- ( ph -> ( T P U ) e. ( ( G ↾s ( T .(+) U ) ) GrpHom ( G ↾s T ) ) )
Theorem	lsmhash 15337	The order of the direct product of groups. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- ( ph -> T e. Fin )   &    |- ( ph -> U e. Fin )   =>    |- ( ph -> ( # ` ( T .(+) U ) ) = ( ( # ` T ) x. ( # ` U ) ) )
10.2.11  Free groups
Syntax	cefg 15338	Extend class notation with the free group equivalence relation.
class ~FG
Syntax	cfrgp 15339	Extend class notation with the free group construction.
class freeGrp
Syntax	cvrgp 15340	Extend class notation with free group injection.
class varFGrp
Definition	df-efg 15341*	Define the free group equivalence relation, which is the smallest equivalence relation ~~ such that for any words A , B and formal symbol x with inverse inv g x, A B ~~ A x ( inv g x ) B. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- ~FG = ( i e. _V |-> |^| { r | ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } )
Definition	df-frgp 15342	Define the free group on a set I of generators, defined as the quotient of the free monoid on I X. 2o (representing the generator elements and their formal inverses) by the free group equivalence relation df-efg 15341. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- freeGrp = ( i e. _V |-> ( (freeMnd ` ( i X. 2o ) ) /.s ( ~FG ` i ) ) )
Definition	df-vrgp 15343*	Define the canonical injection from the generating set I into the base set of the free group. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- varFGrp = ( i e. _V |-> ( j e. i |-> [ <" <. j , (/) >. "> ] ( ~FG ` i ) ) )
Theorem	efgmval 15344*	Value of the formal inverse operation for the generating set of a free group. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   =>    |- ( ( A e. I /\ B e. 2o ) -> ( A M B ) = <. A , ( 1o \ B ) >. )
Theorem	efgmf 15345*	The formal inverse operation is an endofunction on the generating set. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )   =>    |- M : ( I X. 2o ) --> ( I X. 2o )
Theorem	efgmnvl 15346*	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 15347	Lemma for efgval 15349. (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 15348*	Lemma for efgval 15349. (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 15349*	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 15350	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 15351	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 15352	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 15353	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 15354*	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 15355*	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 15356*	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 15357*	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 15358*	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 15359*	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 15360*	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 15361*	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 15362*	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 15363*	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 15364*	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 15365*	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 15366*	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 15367*	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 15368*	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 15369*	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 15370*	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 15371*	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 15372*	The reduced word that forms the base of the sequence in efgsval 15363 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 15373*	Lemma for efgredleme 15375. (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 15374*	Lemma for efgred 15380. (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 15375*	Lemma for efgred 15380. (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 15376*	The reduced word that forms the base of the sequence in efgsval 15363 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 15377*	The reduced word that forms the base of the sequence in efgsval 15363 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 15378*	The reduced word that forms the base of the sequence in efgsval 15363 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 15379*	The reduced word that forms the base of the sequence in efgsval 15363 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 15380*	The reduced word that forms the base of the sequence in efgsval 15363 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 15381*	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 15382*	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 15383*	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 15384*	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 15385*	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 15386*	Lemma for efgrelex 15383. 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 15387*	Lemma for efgrelex 15383. 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 15388*	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 15389*	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 15390	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 15391	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 15392	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 15393	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 15394	The free group is a group. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- G = (freeGrp ` I )   =>    |- ( I e. V -> G e. Grp )
Theorem	frgpadd 15395	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 15396*	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 15397*	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 15398*	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 15399	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 15400	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 )