frgpinv

Description: The inverse of an element of the free group. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	frgpadd.w	\|- W = ( _I ` Word ( I X. 2o ) )
	frgpadd.g	\|- G = ( freeGrp ` I )
	frgpadd.r	\|- .~ = ( ~FG ` I )
	frgpinv.n	\|- N = ( invg ` G )
	frgpinv.m	\|- M = ( y e. I , z e. 2o \|-> <. y , ( 1o \ z ) >. )
Assertion	frgpinv	\|- ( A e. W -> ( N ` [ A ] .~ ) = [ ( M o. ( reverse ` A ) ) ] .~ )

Proof

Step	Hyp	Ref	Expression
1		frgpadd.w	\|- W = ( _I ` Word ( I X. 2o ) )
2		frgpadd.g	\|- G = ( freeGrp ` I )
3		frgpadd.r	\|- .~ = ( ~FG ` I )
4		frgpinv.n	\|- N = ( invg ` G )
5		frgpinv.m	\|- M = ( y e. I , z e. 2o \|-> <. y , ( 1o \ z ) >. )
6		fviss	\|- ( _I ` Word ( I X. 2o ) ) C_ Word ( I X. 2o )
7	1 6	eqsstri	\|- W C_ Word ( I X. 2o )
8	7	sseli	\|- ( A e. W -> A e. Word ( I X. 2o ) )
9		revcl	\|- ( A e. Word ( I X. 2o ) -> ( reverse ` A ) e. Word ( I X. 2o ) )
10	8 9	syl	\|- ( A e. W -> ( reverse ` A ) e. Word ( I X. 2o ) )
11	5	efgmf	\|- M : ( I X. 2o ) --> ( I X. 2o )
12		wrdco	\|- ( ( ( reverse ` A ) e. Word ( I X. 2o ) /\ M : ( I X. 2o ) --> ( I X. 2o ) ) -> ( M o. ( reverse ` A ) ) e. Word ( I X. 2o ) )
13	10 11 12	sylancl	\|- ( A e. W -> ( M o. ( reverse ` A ) ) e. Word ( I X. 2o ) )
14	1	efgrcl	\|- ( A e. W -> ( I e. _V /\ W = Word ( I X. 2o ) ) )
15	14	simprd	\|- ( A e. W -> W = Word ( I X. 2o ) )
16	13 15	eleqtrrd	\|- ( A e. W -> ( M o. ( reverse ` A ) ) e. W )
17		eqid	\|- ( +g ` G ) = ( +g ` G )
18	1 2 3 17	frgpadd	\|- ( ( A e. W /\ ( M o. ( reverse ` A ) ) e. W ) -> ( [ A ] .~ ( +g ` G ) [ ( M o. ( reverse ` A ) ) ] .~ ) = [ ( A ++ ( M o. ( reverse ` A ) ) ) ] .~ )
19	16 18	mpdan	\|- ( A e. W -> ( [ A ] .~ ( +g ` G ) [ ( M o. ( reverse ` A ) ) ] .~ ) = [ ( A ++ ( M o. ( reverse ` A ) ) ) ] .~ )
20	1 3	efger	\|- .~ Er W
21	20	a1i	\|- ( A e. W -> .~ Er W )
22		eqid	\|- ( v e. W \|-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) \|-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) ) = ( v e. W \|-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) \|-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
23	1 3 5 22	efginvrel2	\|- ( A e. W -> ( A ++ ( M o. ( reverse ` A ) ) ) .~ (/) )
24	21 23	erthi	\|- ( A e. W -> [ ( A ++ ( M o. ( reverse ` A ) ) ) ] .~ = [ (/) ] .~ )
25	2 3	frgp0	\|- ( I e. _V -> ( G e. Grp /\ [ (/) ] .~ = ( 0g ` G ) ) )
26	25	adantr	\|- ( ( I e. _V /\ W = Word ( I X. 2o ) ) -> ( G e. Grp /\ [ (/) ] .~ = ( 0g ` G ) ) )
27	14 26	syl	\|- ( A e. W -> ( G e. Grp /\ [ (/) ] .~ = ( 0g ` G ) ) )
28	27	simprd	\|- ( A e. W -> [ (/) ] .~ = ( 0g ` G ) )
29	19 24 28	3eqtrd	\|- ( A e. W -> ( [ A ] .~ ( +g ` G ) [ ( M o. ( reverse ` A ) ) ] .~ ) = ( 0g ` G ) )
30	27	simpld	\|- ( A e. W -> G e. Grp )
31		eqid	\|- ( Base ` G ) = ( Base ` G )
32	2 3 1 31	frgpeccl	\|- ( A e. W -> [ A ] .~ e. ( Base ` G ) )
33	2 3 1 31	frgpeccl	\|- ( ( M o. ( reverse ` A ) ) e. W -> [ ( M o. ( reverse ` A ) ) ] .~ e. ( Base ` G ) )
34	16 33	syl	\|- ( A e. W -> [ ( M o. ( reverse ` A ) ) ] .~ e. ( Base ` G ) )
35		eqid	\|- ( 0g ` G ) = ( 0g ` G )
36	31 17 35 4	grpinvid1	\|- ( ( G e. Grp /\ [ A ] .~ e. ( Base ` G ) /\ [ ( M o. ( reverse ` A ) ) ] .~ e. ( Base ` G ) ) -> ( ( N ` [ A ] .~ ) = [ ( M o. ( reverse ` A ) ) ] .~ <-> ( [ A ] .~ ( +g ` G ) [ ( M o. ( reverse ` A ) ) ] .~ ) = ( 0g ` G ) ) )
37	30 32 34 36	syl3anc	\|- ( A e. W -> ( ( N ` [ A ] .~ ) = [ ( M o. ( reverse ` A ) ) ] .~ <-> ( [ A ] .~ ( +g ` G ) [ ( M o. ( reverse ` A ) ) ] .~ ) = ( 0g ` G ) ) )
38	29 37	mpbird	\|- ( A e. W -> ( N ` [ A ] .~ ) = [ ( M o. ( reverse ` A ) ) ] .~ )

Metamath Proof Explorer

Theorem frgpinv

Proof