# Metamath Proof Explorer

## Theorem frgpinv

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

Ref Expression
Hypotheses frgpadd.w 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
frgpadd.g 𝐺 = ( freeGrp ‘ 𝐼 )
frgpinv.n 𝑁 = ( invg𝐺 )
frgpinv.m 𝑀 = ( 𝑦𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ )
Assertion frgpinv ( 𝐴𝑊 → ( 𝑁 ‘ [ 𝐴 ] ) = [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] )

### Proof

Step Hyp Ref Expression
1 frgpadd.w 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
2 frgpadd.g 𝐺 = ( freeGrp ‘ 𝐼 )
3 frgpadd.r = ( ~FG𝐼 )
4 frgpinv.n 𝑁 = ( invg𝐺 )
5 frgpinv.m 𝑀 = ( 𝑦𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ )
6 fviss ( I ‘ Word ( 𝐼 × 2o ) ) ⊆ Word ( 𝐼 × 2o )
7 1 6 eqsstri 𝑊 ⊆ Word ( 𝐼 × 2o )
8 7 sseli ( 𝐴𝑊𝐴 ∈ Word ( 𝐼 × 2o ) )
9 revcl ( 𝐴 ∈ Word ( 𝐼 × 2o ) → ( reverse ‘ 𝐴 ) ∈ Word ( 𝐼 × 2o ) )
10 8 9 syl ( 𝐴𝑊 → ( reverse ‘ 𝐴 ) ∈ Word ( 𝐼 × 2o ) )
11 5 efgmf 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o )
12 wrdco ( ( ( reverse ‘ 𝐴 ) ∈ Word ( 𝐼 × 2o ) ∧ 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o ) ) → ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ∈ Word ( 𝐼 × 2o ) )
13 10 11 12 sylancl ( 𝐴𝑊 → ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ∈ Word ( 𝐼 × 2o ) )
14 1 efgrcl ( 𝐴𝑊 → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )
15 14 simprd ( 𝐴𝑊𝑊 = Word ( 𝐼 × 2o ) )
16 13 15 eleqtrrd ( 𝐴𝑊 → ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ∈ 𝑊 )
17 eqid ( +g𝐺 ) = ( +g𝐺 )
18 1 2 3 17 frgpadd ( ( 𝐴𝑊 ∧ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ∈ 𝑊 ) → ( [ 𝐴 ] ( +g𝐺 ) [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ) = [ ( 𝐴 ++ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ) ] )
19 16 18 mpdan ( 𝐴𝑊 → ( [ 𝐴 ] ( +g𝐺 ) [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ) = [ ( 𝐴 ++ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ) ] )
20 1 3 efger Er 𝑊
21 20 a1i ( 𝐴𝑊 Er 𝑊 )
22 eqid ( 𝑣𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀𝑤 ) ”⟩ ⟩ ) ) ) = ( 𝑣𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀𝑤 ) ”⟩ ⟩ ) ) )
23 1 3 5 22 efginvrel2 ( 𝐴𝑊 → ( 𝐴 ++ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ) ∅ )
24 21 23 erthi ( 𝐴𝑊 → [ ( 𝐴 ++ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ) ] = [ ∅ ] )
25 2 3 frgp0 ( 𝐼 ∈ V → ( 𝐺 ∈ Grp ∧ [ ∅ ] = ( 0g𝐺 ) ) )
26 25 adantr ( ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) → ( 𝐺 ∈ Grp ∧ [ ∅ ] = ( 0g𝐺 ) ) )
27 14 26 syl ( 𝐴𝑊 → ( 𝐺 ∈ Grp ∧ [ ∅ ] = ( 0g𝐺 ) ) )
28 27 simprd ( 𝐴𝑊 → [ ∅ ] = ( 0g𝐺 ) )
29 19 24 28 3eqtrd ( 𝐴𝑊 → ( [ 𝐴 ] ( +g𝐺 ) [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ) = ( 0g𝐺 ) )
30 27 simpld ( 𝐴𝑊𝐺 ∈ Grp )
31 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
32 2 3 1 31 frgpeccl ( 𝐴𝑊 → [ 𝐴 ] ∈ ( Base ‘ 𝐺 ) )
33 2 3 1 31 frgpeccl ( ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ∈ 𝑊 → [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ∈ ( Base ‘ 𝐺 ) )
34 16 33 syl ( 𝐴𝑊 → [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ∈ ( Base ‘ 𝐺 ) )
35 eqid ( 0g𝐺 ) = ( 0g𝐺 )
36 31 17 35 4 grpinvid1 ( ( 𝐺 ∈ Grp ∧ [ 𝐴 ] ∈ ( Base ‘ 𝐺 ) ∧ [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑁 ‘ [ 𝐴 ] ) = [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ↔ ( [ 𝐴 ] ( +g𝐺 ) [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ) = ( 0g𝐺 ) ) )
37 30 32 34 36 syl3anc ( 𝐴𝑊 → ( ( 𝑁 ‘ [ 𝐴 ] ) = [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ↔ ( [ 𝐴 ] ( +g𝐺 ) [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ) = ( 0g𝐺 ) ) )
38 29 37 mpbird ( 𝐴𝑊 → ( 𝑁 ‘ [ 𝐴 ] ) = [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] )