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

Metamath Proof Explorer

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 ffvelcdmda ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝑐 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( 𝐴 ‘ 𝑐 ) ∈ ( 𝐼 × 2o ) )
21 3 efgmnvl ⊢ ( ( 𝐴 ‘ 𝑐 ) ∈ ( 𝐼 × 2o ) → ( 𝑀 ‘ ( 𝑀 ‘ ( 𝐴 ‘ 𝑐 ) ) ) = ( 𝐴 ‘ 𝑐 ) )
22 20 21 syl ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝑐 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( 𝑀 ‘ ( 𝑀 ‘ ( 𝐴 ‘ 𝑐 ) ) ) = ( 𝐴 ‘ 𝑐 ) )
23 22 mpteq2dva ⊢ ( 𝐴 ∈ 𝑊 → ( 𝑐 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ↦ ( 𝑀 ‘ ( 𝑀 ‘ ( 𝐴 ‘ 𝑐 ) ) ) ) = ( 𝑐 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ↦ ( 𝐴 ‘ 𝑐 ) ) )
24 10 ffvelcdmi ⊢ ( ( 𝐴 ‘ 𝑐 ) ∈ ( 𝐼 × 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 ‘ 𝐴 ) ) ++ 𝐴 ) ∼ ∅ )