Theorem efginvrel1

Description: 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)

	Ref	Expression
Hypotheses	efgval.w	|- W = ( _I ` Word ( I X. 2o ) )
	efgval.r	|- .~ = ( ~FG ` I )
	efgval2.m	|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
	efgval2.t	|- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
Assertion	efginvrel1	|- ( A e. W -> ( ( M o. ( reverse ` A ) ) ++ A ) .~ (/) )

Proof

Step	Hyp	Ref	Expression
1		efgval.w	|- W = ( _I ` Word ( I X. 2o ) )
2		efgval.r	|- .~ = ( ~FG ` I )
3		efgval2.m	|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
4		efgval2.t	|- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
5		fviss	|- ( _I ` Word ( I X. 2o ) ) C_ Word ( I X. 2o )
6	1 5	eqsstri	|- W C_ Word ( I X. 2o )
7	6	sseli	|- ( A e. W -> A e. Word ( I X. 2o ) )
8		revcl	|- ( A e. Word ( I X. 2o ) -> ( reverse ` A ) e. Word ( I X. 2o ) )
9	7 8	syl	|- ( A e. W -> ( reverse ` A ) e. Word ( I X. 2o ) )
10	3	efgmf	|- M : ( I X. 2o ) --> ( I X. 2o )
11		revco	|- ( ( ( reverse ` A ) e. Word ( I X. 2o ) /\ M : ( I X. 2o ) --> ( I X. 2o ) ) -> ( M o. ( reverse ` ( reverse ` A ) ) ) = ( reverse ` ( M o. ( reverse ` A ) ) ) )
12	9 10 11	sylancl	|- ( A e. W -> ( M o. ( reverse ` ( reverse ` A ) ) ) = ( reverse ` ( M o. ( reverse ` A ) ) ) )
13		revrev	|- ( A e. Word ( I X. 2o ) -> ( reverse ` ( reverse ` A ) ) = A )
14	7 13	syl	|- ( A e. W -> ( reverse ` ( reverse ` A ) ) = A )
15	14	coeq2d	|- ( A e. W -> ( M o. ( reverse ` ( reverse ` A ) ) ) = ( M o. A ) )
16	12 15	eqtr3d	|- ( A e. W -> ( reverse ` ( M o. ( reverse ` A ) ) ) = ( M o. A ) )
17	16	coeq2d	|- ( A e. W -> ( M o. ( reverse ` ( M o. ( reverse ` A ) ) ) ) = ( M o. ( M o. A ) ) )
18		wrdf	|- ( A e. Word ( I X. 2o ) -> A : ( 0 ..^ ( # ` A ) ) --> ( I X. 2o ) )
19	7 18	syl	|- ( A e. W -> A : ( 0 ..^ ( # ` A ) ) --> ( I X. 2o ) )
20	19	ffvelrnda	|- ( ( A e. W /\ c e. ( 0 ..^ ( # ` A ) ) ) -> ( A ` c ) e. ( I X. 2o ) )
21	3	efgmnvl	|- ( ( A ` c ) e. ( I X. 2o ) -> ( M ` ( M ` ( A ` c ) ) ) = ( A ` c ) )
22	20 21	syl	|- ( ( A e. W /\ c e. ( 0 ..^ ( # ` A ) ) ) -> ( M ` ( M ` ( A ` c ) ) ) = ( A ` c ) )
23	22	mpteq2dva	|- ( A e. W -> ( c e. ( 0 ..^ ( # ` A ) ) |-> ( M ` ( M ` ( A ` c ) ) ) ) = ( c e. ( 0 ..^ ( # ` A ) ) |-> ( A ` c ) ) )
24	10	ffvelrni	|- ( ( A ` c ) e. ( I X. 2o ) -> ( M ` ( A ` c ) ) e. ( I X. 2o ) )
25	20 24	syl	|- ( ( A e. W /\ c e. ( 0 ..^ ( # ` A ) ) ) -> ( M ` ( A ` c ) ) e. ( I X. 2o ) )
26		fcompt	|- ( ( M : ( I X. 2o ) --> ( I X. 2o ) /\ A : ( 0 ..^ ( # ` A ) ) --> ( I X. 2o ) ) -> ( M o. A ) = ( c e. ( 0 ..^ ( # ` A ) ) |-> ( M ` ( A ` c ) ) ) )
27	10 19 26	sylancr	|- ( A e. W -> ( M o. A ) = ( c e. ( 0 ..^ ( # ` A ) ) |-> ( M ` ( A ` c ) ) ) )
28	10	a1i	|- ( A e. W -> M : ( I X. 2o ) --> ( I X. 2o ) )
29	28	feqmptd	|- ( A e. W -> M = ( a e. ( I X. 2o ) |-> ( M ` a ) ) )
30		fveq2	|- ( a = ( M ` ( A ` c ) ) -> ( M ` a ) = ( M ` ( M ` ( A ` c ) ) ) )
31	25 27 29 30	fmptco	|- ( A e. W -> ( M o. ( M o. A ) ) = ( c e. ( 0 ..^ ( # ` A ) ) |-> ( M ` ( M ` ( A ` c ) ) ) ) )
32	19	feqmptd	|- ( A e. W -> A = ( c e. ( 0 ..^ ( # ` A ) ) |-> ( A ` c ) ) )
33	23 31 32	3eqtr4d	|- ( A e. W -> ( M o. ( M o. A ) ) = A )
34	17 33	eqtrd	|- ( A e. W -> ( M o. ( reverse ` ( M o. ( reverse ` A ) ) ) ) = A )
35	34	oveq2d	|- ( A e. W -> ( ( M o. ( reverse ` A ) ) ++ ( M o. ( reverse ` ( M o. ( reverse ` A ) ) ) ) ) = ( ( M o. ( reverse ` A ) ) ++ A ) )
36		wrdco	|- ( ( ( reverse ` A ) e. Word ( I X. 2o ) /\ M : ( I X. 2o ) --> ( I X. 2o ) ) -> ( M o. ( reverse ` A ) ) e. Word ( I X. 2o ) )
37	9 10 36	sylancl	|- ( A e. W -> ( M o. ( reverse ` A ) ) e. Word ( I X. 2o ) )
38	1	efgrcl	|- ( A e. W -> ( I e. _V /\ W = Word ( I X. 2o ) ) )
39	38	simprd	|- ( A e. W -> W = Word ( I X. 2o ) )
40	37 39	eleqtrrd	|- ( A e. W -> ( M o. ( reverse ` A ) ) e. W )
41	1 2 3 4	efginvrel2	|- ( ( M o. ( reverse ` A ) ) e. W -> ( ( M o. ( reverse ` A ) ) ++ ( M o. ( reverse ` ( M o. ( reverse ` A ) ) ) ) ) .~ (/) )
42	40 41	syl	|- ( A e. W -> ( ( M o. ( reverse ` A ) ) ++ ( M o. ( reverse ` ( M o. ( reverse ` A ) ) ) ) ) .~ (/) )
43	35 42	eqbrtrrd	|- ( A e. W -> ( ( M o. ( reverse ` A ) ) ++ A ) .~ (/) )