This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐼 )
frgpadd.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
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 ‘ 𝐴 ) ) ] ∼ )