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	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
	efgval.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
	efgval2.m	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
	efgval2.t	⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
Assertion	efginvrel1	⊢ ( 𝐴 ∈ 𝑊 → ( ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ++ 𝐴 ) ∼ ∅ )

Proof

Step	Hyp	Ref	Expression
1		efgval.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
2		efgval.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
3		efgval2.m	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
4		efgval2.t	⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
5		fviss	⊢ ( I ‘ Word ( 𝐼 × 2o ) ) ⊆ Word ( 𝐼 × 2o )
6	1 5	eqsstri	⊢ 𝑊 ⊆ Word ( 𝐼 × 2o )
7	6	sseli	⊢ ( 𝐴 ∈ 𝑊 → 𝐴 ∈ Word ( 𝐼 × 2o ) )
8		revcl	⊢ ( 𝐴 ∈ Word ( 𝐼 × 2o ) → ( reverse ‘ 𝐴 ) ∈ Word ( 𝐼 × 2o ) )
9	7 8	syl	⊢ ( 𝐴 ∈ 𝑊 → ( reverse ‘ 𝐴 ) ∈ Word ( 𝐼 × 2o ) )
10	3	efgmf	⊢ 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o )
11		revco	⊢ ( ( ( reverse ‘ 𝐴 ) ∈ Word ( 𝐼 × 2o ) ∧ 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o ) ) → ( 𝑀 ∘ ( reverse ‘ ( reverse ‘ 𝐴 ) ) ) = ( reverse ‘ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ) )
12	9 10 11	sylancl	⊢ ( 𝐴 ∈ 𝑊 → ( 𝑀 ∘ ( reverse ‘ ( reverse ‘ 𝐴 ) ) ) = ( reverse ‘ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ) )
13		revrev	⊢ ( 𝐴 ∈ Word ( 𝐼 × 2o ) → ( reverse ‘ ( reverse ‘ 𝐴 ) ) = 𝐴 )
14	7 13	syl	⊢ ( 𝐴 ∈ 𝑊 → ( reverse ‘ ( reverse ‘ 𝐴 ) ) = 𝐴 )
15	14	coeq2d	⊢ ( 𝐴 ∈ 𝑊 → ( 𝑀 ∘ ( reverse ‘ ( reverse ‘ 𝐴 ) ) ) = ( 𝑀 ∘ 𝐴 ) )
16	12 15	eqtr3d	⊢ ( 𝐴 ∈ 𝑊 → ( reverse ‘ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ) = ( 𝑀 ∘ 𝐴 ) )
17	16	coeq2d	⊢ ( 𝐴 ∈ 𝑊 → ( 𝑀 ∘ ( reverse ‘ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ) ) = ( 𝑀 ∘ ( 𝑀 ∘ 𝐴 ) ) )
18		wrdf	⊢ ( 𝐴 ∈ Word ( 𝐼 × 2o ) → 𝐴 : ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ⟶ ( 𝐼 × 2o ) )
19	7 18	syl	⊢ ( 𝐴 ∈ 𝑊 → 𝐴 : ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ⟶ ( 𝐼 × 2o ) )
20	19	ffvelrnda	⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝑐 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( 𝐴 ‘ 𝑐 ) ∈ ( 𝐼 × 2o ) )
21	3	efgmnvl	⊢ ( ( 𝐴 ‘ 𝑐 ) ∈ ( 𝐼 × 2o ) → ( 𝑀 ‘ ( 𝑀 ‘ ( 𝐴 ‘ 𝑐 ) ) ) = ( 𝐴 ‘ 𝑐 ) )
22	20 21	syl	⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝑐 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( 𝑀 ‘ ( 𝑀 ‘ ( 𝐴 ‘ 𝑐 ) ) ) = ( 𝐴 ‘ 𝑐 ) )
23	22	mpteq2dva	⊢ ( 𝐴 ∈ 𝑊 → ( 𝑐 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ↦ ( 𝑀 ‘ ( 𝑀 ‘ ( 𝐴 ‘ 𝑐 ) ) ) ) = ( 𝑐 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ↦ ( 𝐴 ‘ 𝑐 ) ) )
24	10	ffvelrni	⊢ ( ( 𝐴 ‘ 𝑐 ) ∈ ( 𝐼 × 2o ) → ( 𝑀 ‘ ( 𝐴 ‘ 𝑐 ) ) ∈ ( 𝐼 × 2o ) )
25	20 24	syl	⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝑐 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( 𝑀 ‘ ( 𝐴 ‘ 𝑐 ) ) ∈ ( 𝐼 × 2o ) )
26		fcompt	⊢ ( ( 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o ) ∧ 𝐴 : ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ⟶ ( 𝐼 × 2o ) ) → ( 𝑀 ∘ 𝐴 ) = ( 𝑐 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ↦ ( 𝑀 ‘ ( 𝐴 ‘ 𝑐 ) ) ) )
27	10 19 26	sylancr	⊢ ( 𝐴 ∈ 𝑊 → ( 𝑀 ∘ 𝐴 ) = ( 𝑐 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ↦ ( 𝑀 ‘ ( 𝐴 ‘ 𝑐 ) ) ) )
28	10	a1i	⊢ ( 𝐴 ∈ 𝑊 → 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o ) )
29	28	feqmptd	⊢ ( 𝐴 ∈ 𝑊 → 𝑀 = ( 𝑎 ∈ ( 𝐼 × 2o ) ↦ ( 𝑀 ‘ 𝑎 ) ) )
30		fveq2	⊢ ( 𝑎 = ( 𝑀 ‘ ( 𝐴 ‘ 𝑐 ) ) → ( 𝑀 ‘ 𝑎 ) = ( 𝑀 ‘ ( 𝑀 ‘ ( 𝐴 ‘ 𝑐 ) ) ) )
31	25 27 29 30	fmptco	⊢ ( 𝐴 ∈ 𝑊 → ( 𝑀 ∘ ( 𝑀 ∘ 𝐴 ) ) = ( 𝑐 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ↦ ( 𝑀 ‘ ( 𝑀 ‘ ( 𝐴 ‘ 𝑐 ) ) ) ) )
32	19	feqmptd	⊢ ( 𝐴 ∈ 𝑊 → 𝐴 = ( 𝑐 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ↦ ( 𝐴 ‘ 𝑐 ) ) )
33	23 31 32	3eqtr4d	⊢ ( 𝐴 ∈ 𝑊 → ( 𝑀 ∘ ( 𝑀 ∘ 𝐴 ) ) = 𝐴 )
34	17 33	eqtrd	⊢ ( 𝐴 ∈ 𝑊 → ( 𝑀 ∘ ( reverse ‘ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ) ) = 𝐴 )
35	34	oveq2d	⊢ ( 𝐴 ∈ 𝑊 → ( ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ++ ( 𝑀 ∘ ( reverse ‘ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ) ) ) = ( ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ++ 𝐴 ) )
36		wrdco	⊢ ( ( ( reverse ‘ 𝐴 ) ∈ Word ( 𝐼 × 2o ) ∧ 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o ) ) → ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ∈ Word ( 𝐼 × 2o ) )
37	9 10 36	sylancl	⊢ ( 𝐴 ∈ 𝑊 → ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ∈ Word ( 𝐼 × 2o ) )
38	1	efgrcl	⊢ ( 𝐴 ∈ 𝑊 → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )
39	38	simprd	⊢ ( 𝐴 ∈ 𝑊 → 𝑊 = Word ( 𝐼 × 2o ) )
40	37 39	eleqtrrd	⊢ ( 𝐴 ∈ 𝑊 → ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ∈ 𝑊 )
41	1 2 3 4	efginvrel2	⊢ ( ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ∈ 𝑊 → ( ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ++ ( 𝑀 ∘ ( reverse ‘ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ) ) ) ∼ ∅ )
42	40 41	syl	⊢ ( 𝐴 ∈ 𝑊 → ( ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ++ ( 𝑀 ∘ ( reverse ‘ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ) ) ) ∼ ∅ )
43	35 42	eqbrtrrd	⊢ ( 𝐴 ∈ 𝑊 → ( ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ++ 𝐴 ) ∼ ∅ )