Metamath Proof Explorer

Theorem efginvrel2

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 efginvrel2 ( 𝐴 ∈ 𝑊 → ( 𝐴 ++ ( 𝑀 ∘ ( 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 id ⊢ ( 𝑐 = ∅ → 𝑐 = ∅ )
9 fveq2 ⊢ ( 𝑐 = ∅ → ( reverse ‘ 𝑐 ) = ( reverse ‘ ∅ ) )
10 rev0 ⊢ ( reverse ‘ ∅ ) = ∅
11 9 10 eqtrdi ⊢ ( 𝑐 = ∅ → ( reverse ‘ 𝑐 ) = ∅ )
12 11 coeq2d ⊢ ( 𝑐 = ∅ → ( 𝑀 ∘ ( reverse ‘ 𝑐 ) ) = ( 𝑀 ∘ ∅ ) )
13 co02 ⊢ ( 𝑀 ∘ ∅ ) = ∅
14 12 13 eqtrdi ⊢ ( 𝑐 = ∅ → ( 𝑀 ∘ ( reverse ‘ 𝑐 ) ) = ∅ )
15 8 14 oveq12d ⊢ ( 𝑐 = ∅ → ( 𝑐 ++ ( 𝑀 ∘ ( reverse ‘ 𝑐 ) ) ) = ( ∅ ++ ∅ ) )
16 15 breq1d ⊢ ( 𝑐 = ∅ → ( ( 𝑐 ++ ( 𝑀 ∘ ( reverse ‘ 𝑐 ) ) ) ∼ ∅ ↔ ( ∅ ++ ∅ ) ∼ ∅ ) )
17 16 imbi2d ⊢ ( 𝑐 = ∅ → ( ( 𝐴 ∈ 𝑊 → ( 𝑐 ++ ( 𝑀 ∘ ( reverse ‘ 𝑐 ) ) ) ∼ ∅ ) ↔ ( 𝐴 ∈ 𝑊 → ( ∅ ++ ∅ ) ∼ ∅ ) ) )
18 id ⊢ ( 𝑐 = 𝑎 → 𝑐 = 𝑎 )
19 fveq2 ⊢ ( 𝑐 = 𝑎 → ( reverse ‘ 𝑐 ) = ( reverse ‘ 𝑎 ) )
20 19 coeq2d ⊢ ( 𝑐 = 𝑎 → ( 𝑀 ∘ ( reverse ‘ 𝑐 ) ) = ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) )
21 18 20 oveq12d ⊢ ( 𝑐 = 𝑎 → ( 𝑐 ++ ( 𝑀 ∘ ( reverse ‘ 𝑐 ) ) ) = ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) )
22 21 breq1d ⊢ ( 𝑐 = 𝑎 → ( ( 𝑐 ++ ( 𝑀 ∘ ( reverse ‘ 𝑐 ) ) ) ∼ ∅ ↔ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ∼ ∅ ) )
23 22 imbi2d ⊢ ( 𝑐 = 𝑎 → ( ( 𝐴 ∈ 𝑊 → ( 𝑐 ++ ( 𝑀 ∘ ( reverse ‘ 𝑐 ) ) ) ∼ ∅ ) ↔ ( 𝐴 ∈ 𝑊 → ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ∼ ∅ ) ) )
24 id ⊢ ( 𝑐 = ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) → 𝑐 = ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) )
25 fveq2 ⊢ ( 𝑐 = ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) → ( reverse ‘ 𝑐 ) = ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) )
26 25 coeq2d ⊢ ( 𝑐 = ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) → ( 𝑀 ∘ ( reverse ‘ 𝑐 ) ) = ( 𝑀 ∘ ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) ) )
27 24 26 oveq12d ⊢ ( 𝑐 = ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) → ( 𝑐 ++ ( 𝑀 ∘ ( reverse ‘ 𝑐 ) ) ) = ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) ) ) )
28 27 breq1d ⊢ ( 𝑐 = ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) → ( ( 𝑐 ++ ( 𝑀 ∘ ( reverse ‘ 𝑐 ) ) ) ∼ ∅ ↔ ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) ) ) ∼ ∅ ) )
29 28 imbi2d ⊢ ( 𝑐 = ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) → ( ( 𝐴 ∈ 𝑊 → ( 𝑐 ++ ( 𝑀 ∘ ( reverse ‘ 𝑐 ) ) ) ∼ ∅ ) ↔ ( 𝐴 ∈ 𝑊 → ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) ) ) ∼ ∅ ) ) )
30 id ⊢ ( 𝑐 = 𝐴 → 𝑐 = 𝐴 )
31 fveq2 ⊢ ( 𝑐 = 𝐴 → ( reverse ‘ 𝑐 ) = ( reverse ‘ 𝐴 ) )
32 31 coeq2d ⊢ ( 𝑐 = 𝐴 → ( 𝑀 ∘ ( reverse ‘ 𝑐 ) ) = ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) )
33 30 32 oveq12d ⊢ ( 𝑐 = 𝐴 → ( 𝑐 ++ ( 𝑀 ∘ ( reverse ‘ 𝑐 ) ) ) = ( 𝐴 ++ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ) )
34 33 breq1d ⊢ ( 𝑐 = 𝐴 → ( ( 𝑐 ++ ( 𝑀 ∘ ( reverse ‘ 𝑐 ) ) ) ∼ ∅ ↔ ( 𝐴 ++ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ) ∼ ∅ ) )
35 34 imbi2d ⊢ ( 𝑐 = 𝐴 → ( ( 𝐴 ∈ 𝑊 → ( 𝑐 ++ ( 𝑀 ∘ ( reverse ‘ 𝑐 ) ) ) ∼ ∅ ) ↔ ( 𝐴 ∈ 𝑊 → ( 𝐴 ++ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ) ∼ ∅ ) ) )
36 ccatidid ⊢ ( ∅ ++ ∅ ) = ∅
37 1 2 efger ⊢ ∼ Er 𝑊
38 37 a1i ⊢ ( 𝐴 ∈ 𝑊 → ∼ Er 𝑊 )
39 wrd0 ⊢ ∅ ∈ Word ( 𝐼 × 2o )
40 1 efgrcl ⊢ ( 𝐴 ∈ 𝑊 → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )
41 40 simprd ⊢ ( 𝐴 ∈ 𝑊 → 𝑊 = Word ( 𝐼 × 2o ) )
42 39 41 eleqtrrid ⊢ ( 𝐴 ∈ 𝑊 → ∅ ∈ 𝑊 )
43 38 42 erref ⊢ ( 𝐴 ∈ 𝑊 → ∅ ∼ ∅ )
44 36 43 eqbrtrid ⊢ ( 𝐴 ∈ 𝑊 → ( ∅ ++ ∅ ) ∼ ∅ )
45 37 a1i ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ∼ Er 𝑊 )
46 simprl ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑎 ∈ Word ( 𝐼 × 2o ) )
47 revcl ⊢ ( 𝑎 ∈ Word ( 𝐼 × 2o ) → ( reverse ‘ 𝑎 ) ∈ Word ( 𝐼 × 2o ) )
48 47 ad2antrl ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( reverse ‘ 𝑎 ) ∈ Word ( 𝐼 × 2o ) )
49 3 efgmf ⊢ 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o )
50 wrdco ⊢ ( ( ( reverse ‘ 𝑎 ) ∈ Word ( 𝐼 × 2o ) ∧ 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o ) ) → ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ∈ Word ( 𝐼 × 2o ) )
51 48 49 50 sylancl ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ∈ Word ( 𝐼 × 2o ) )
52 ccatcl ⊢ ( ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ∈ Word ( 𝐼 × 2o ) ) → ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ∈ Word ( 𝐼 × 2o ) )
53 46 51 52 syl2anc ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ∈ Word ( 𝐼 × 2o ) )
54 41 adantr ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑊 = Word ( 𝐼 × 2o ) )
55 53 54 eleqtrrd ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ∈ 𝑊 )
56 lencl ⊢ ( 𝑎 ∈ Word ( 𝐼 × 2o ) → ( ♯ ‘ 𝑎 ) ∈ ℕ0 )
57 56 ad2antrl ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝑎 ) ∈ ℕ0 )
58 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
59 57 58 eleqtrdi ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝑎 ) ∈ ( ℤ≥ ‘ 0 ) )
60 ccatlen ⊢ ( ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ∈ Word ( 𝐼 × 2o ) ) → ( ♯ ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) = ( ( ♯ ‘ 𝑎 ) + ( ♯ ‘ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) )
61 46 51 60 syl2anc ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) = ( ( ♯ ‘ 𝑎 ) + ( ♯ ‘ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) )
62 57 nn0zd ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝑎 ) ∈ ℤ )
63 62 uzidd ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝑎 ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑎 ) ) )
64 lencl ⊢ ( ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ∈ Word ( 𝐼 × 2o ) → ( ♯ ‘ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ∈ ℕ0 )
65 51 64 syl ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ∈ ℕ0 )
66 uzaddcl ⊢ ( ( ( ♯ ‘ 𝑎 ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑎 ) ) ∧ ( ♯ ‘ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑎 ) + ( ♯ ‘ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑎 ) ) )
67 63 65 66 syl2anc ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝑎 ) + ( ♯ ‘ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑎 ) ) )
68 61 67 eqeltrd ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑎 ) ) )
69 elfzuzb ⊢ ( ( ♯ ‘ 𝑎 ) ∈ ( 0 ... ( ♯ ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) ) ↔ ( ( ♯ ‘ 𝑎 ) ∈ ( ℤ≥ ‘ 0 ) ∧ ( ♯ ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑎 ) ) ) )
70 59 68 69 sylanbrc ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝑎 ) ∈ ( 0 ... ( ♯ ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) ) )
71 simprr ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑏 ∈ ( 𝐼 × 2o ) )
72 1 2 3 4 efgtval ⊢ ( ( ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ∈ 𝑊 ∧ ( ♯ ‘ 𝑎 ) ∈ ( 0 ... ( ♯ ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) → ( ( ♯ ‘ 𝑎 ) ( 𝑇 ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) 𝑏 ) = ( ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) splice ⟨ ( ♯ ‘ 𝑎 ) , ( ♯ ‘ 𝑎 ) , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) )
73 55 70 71 72 syl3anc ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝑎 ) ( 𝑇 ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) 𝑏 ) = ( ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) splice ⟨ ( ♯ ‘ 𝑎 ) , ( ♯ ‘ 𝑎 ) , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) )
74 39 a1i ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ∅ ∈ Word ( 𝐼 × 2o ) )
75 49 ffvelrni ⊢ ( 𝑏 ∈ ( 𝐼 × 2o ) → ( 𝑀 ‘ 𝑏 ) ∈ ( 𝐼 × 2o ) )
76 75 ad2antll ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑀 ‘ 𝑏 ) ∈ ( 𝐼 × 2o ) )
77 71 76 s2cld ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ∈ Word ( 𝐼 × 2o ) )
78 ccatrid ⊢ ( 𝑎 ∈ Word ( 𝐼 × 2o ) → ( 𝑎 ++ ∅ ) = 𝑎 )
79 78 ad2antrl ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑎 ++ ∅ ) = 𝑎 )
80 79 eqcomd ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑎 = ( 𝑎 ++ ∅ ) )
81 80 oveq1d ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) = ( ( 𝑎 ++ ∅ ) ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) )
82 eqidd ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝑎 ) = ( ♯ ‘ 𝑎 ) )
83 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
84 83 oveq2i ⊢ ( ( ♯ ‘ 𝑎 ) + ( ♯ ‘ ∅ ) ) = ( ( ♯ ‘ 𝑎 ) + 0 )
85 57 nn0cnd ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝑎 ) ∈ ℂ )
86 85 addid1d ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝑎 ) + 0 ) = ( ♯ ‘ 𝑎 ) )
87 84 86 eqtr2id ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝑎 ) = ( ( ♯ ‘ 𝑎 ) + ( ♯ ‘ ∅ ) ) )
88 46 74 51 77 81 82 87 splval2 ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) splice ⟨ ( ♯ ‘ 𝑎 ) , ( ♯ ‘ 𝑎 ) , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) = ( ( 𝑎 ++ ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) )
89 71 s1cld ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ⟨“ 𝑏 ”⟩ ∈ Word ( 𝐼 × 2o ) )
90 revccat ⊢ ( ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ 𝑏 ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) = ( ( reverse ‘ ⟨“ 𝑏 ”⟩ ) ++ ( reverse ‘ 𝑎 ) ) )
91 46 89 90 syl2anc ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) = ( ( reverse ‘ ⟨“ 𝑏 ”⟩ ) ++ ( reverse ‘ 𝑎 ) ) )
92 revs1 ⊢ ( reverse ‘ ⟨“ 𝑏 ”⟩ ) = ⟨“ 𝑏 ”⟩
93 92 oveq1i ⊢ ( ( reverse ‘ ⟨“ 𝑏 ”⟩ ) ++ ( reverse ‘ 𝑎 ) ) = ( ⟨“ 𝑏 ”⟩ ++ ( reverse ‘ 𝑎 ) )
94 91 93 eqtrdi ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) = ( ⟨“ 𝑏 ”⟩ ++ ( reverse ‘ 𝑎 ) ) )
95 94 coeq2d ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑀 ∘ ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) ) = ( 𝑀 ∘ ( ⟨“ 𝑏 ”⟩ ++ ( reverse ‘ 𝑎 ) ) ) )
96 49 a1i ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o ) )
97 ccatco ⊢ ( ( ⟨“ 𝑏 ”⟩ ∈ Word ( 𝐼 × 2o ) ∧ ( reverse ‘ 𝑎 ) ∈ Word ( 𝐼 × 2o ) ∧ 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o ) ) → ( 𝑀 ∘ ( ⟨“ 𝑏 ”⟩ ++ ( reverse ‘ 𝑎 ) ) ) = ( ( 𝑀 ∘ ⟨“ 𝑏 ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) )
98 89 48 96 97 syl3anc ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑀 ∘ ( ⟨“ 𝑏 ”⟩ ++ ( reverse ‘ 𝑎 ) ) ) = ( ( 𝑀 ∘ ⟨“ 𝑏 ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) )
99 s1co ⊢ ( ( 𝑏 ∈ ( 𝐼 × 2o ) ∧ 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o ) ) → ( 𝑀 ∘ ⟨“ 𝑏 ”⟩ ) = ⟨“ ( 𝑀 ‘ 𝑏 ) ”⟩ )
100 71 49 99 sylancl ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑀 ∘ ⟨“ 𝑏 ”⟩ ) = ⟨“ ( 𝑀 ‘ 𝑏 ) ”⟩ )
101 100 oveq1d ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝑀 ∘ ⟨“ 𝑏 ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) = ( ⟨“ ( 𝑀 ‘ 𝑏 ) ”⟩ ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) )
102 95 98 101 3eqtrd ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑀 ∘ ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) ) = ( ⟨“ ( 𝑀 ‘ 𝑏 ) ”⟩ ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) )
103 102 oveq2d ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) ) ) = ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ( ⟨“ ( 𝑀 ‘ 𝑏 ) ”⟩ ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) )
104 ccatcl ⊢ ( ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ 𝑏 ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ∈ Word ( 𝐼 × 2o ) )
105 46 89 104 syl2anc ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ∈ Word ( 𝐼 × 2o ) )
106 76 s1cld ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ⟨“ ( 𝑀 ‘ 𝑏 ) ”⟩ ∈ Word ( 𝐼 × 2o ) )
107 ccatass ⊢ ( ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ ( 𝑀 ‘ 𝑏 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ∈ Word ( 𝐼 × 2o ) ) → ( ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑏 ) ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) = ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ( ⟨“ ( 𝑀 ‘ 𝑏 ) ”⟩ ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) )
108 105 106 51 107 syl3anc ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑏 ) ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) = ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ( ⟨“ ( 𝑀 ‘ 𝑏 ) ”⟩ ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) )
109 ccatass ⊢ ( ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ 𝑏 ”⟩ ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ ( 𝑀 ‘ 𝑏 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑏 ) ”⟩ ) = ( 𝑎 ++ ( ⟨“ 𝑏 ”⟩ ++ ⟨“ ( 𝑀 ‘ 𝑏 ) ”⟩ ) ) )
110 46 89 106 109 syl3anc ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑏 ) ”⟩ ) = ( 𝑎 ++ ( ⟨“ 𝑏 ”⟩ ++ ⟨“ ( 𝑀 ‘ 𝑏 ) ”⟩ ) ) )
111 df-s2 ⊢ ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ = ( ⟨“ 𝑏 ”⟩ ++ ⟨“ ( 𝑀 ‘ 𝑏 ) ”⟩ )
112 111 oveq2i ⊢ ( 𝑎 ++ ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) = ( 𝑎 ++ ( ⟨“ 𝑏 ”⟩ ++ ⟨“ ( 𝑀 ‘ 𝑏 ) ”⟩ ) )
113 110 112 eqtr4di ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑏 ) ”⟩ ) = ( 𝑎 ++ ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) )
114 113 oveq1d ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑏 ) ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) = ( ( 𝑎 ++ ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) )
115 103 108 114 3eqtr2rd ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝑎 ++ ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) = ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) ) ) )
116 73 88 115 3eqtrd ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝑎 ) ( 𝑇 ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) 𝑏 ) = ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) ) ) )
117 1 2 3 4 efgtf ⊢ ( ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ∈ 𝑊 → ( ( 𝑇 ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) = ( 𝑚 ∈ ( 0 ... ( ♯ ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) ) , 𝑢 ∈ ( 𝐼 × 2o ) ↦ ( ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”⟩ ⟩ ) ) ∧ ( 𝑇 ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) : ( ( 0 ... ( ♯ ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) )
118 117 simprd ⊢ ( ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ∈ 𝑊 → ( 𝑇 ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) : ( ( 0 ... ( ♯ ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 )
119 55 118 syl ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑇 ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) : ( ( 0 ... ( ♯ ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 )
120 119 ffnd ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑇 ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) Fn ( ( 0 ... ( ♯ ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) ) × ( 𝐼 × 2o ) ) )
121 fnovrn ⊢ ( ( ( 𝑇 ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) Fn ( ( 0 ... ( ♯ ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) ) × ( 𝐼 × 2o ) ) ∧ ( ♯ ‘ 𝑎 ) ∈ ( 0 ... ( ♯ ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) → ( ( ♯ ‘ 𝑎 ) ( 𝑇 ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) 𝑏 ) ∈ ran ( 𝑇 ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) )
122 120 70 71 121 syl3anc ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝑎 ) ( 𝑇 ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) 𝑏 ) ∈ ran ( 𝑇 ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) )
123 116 122 eqeltrrd ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) ) ) ∈ ran ( 𝑇 ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) )
124 1 2 3 4 efgi2 ⊢ ( ( ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ∈ 𝑊 ∧ ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) ) ) ∈ ran ( 𝑇 ‘ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ) ) → ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ∼ ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) ) ) )
125 55 123 124 syl2anc ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ∼ ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) ) ) )
126 45 125 ersym ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) ) ) ∼ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) )
127 45 ertr ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) ) ) ∼ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ∧ ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ∼ ∅ ) → ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) ) ) ∼ ∅ ) )
128 126 127 mpand ⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ∼ ∅ → ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) ) ) ∼ ∅ ) )
129 128 expcom ⊢ ( ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) → ( 𝐴 ∈ 𝑊 → ( ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ∼ ∅ → ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) ) ) ∼ ∅ ) ) )
130 129 a2d ⊢ ( ( 𝑎 ∈ Word ( 𝐼 × 2o ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) → ( ( 𝐴 ∈ 𝑊 → ( 𝑎 ++ ( 𝑀 ∘ ( reverse ‘ 𝑎 ) ) ) ∼ ∅ ) → ( 𝐴 ∈ 𝑊 → ( ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ++ ( 𝑀 ∘ ( reverse ‘ ( 𝑎 ++ ⟨“ 𝑏 ”⟩ ) ) ) ) ∼ ∅ ) ) )
131 17 23 29 35 44 130 wrdind ⊢ ( 𝐴 ∈ Word ( 𝐼 × 2o ) → ( 𝐴 ∈ 𝑊 → ( 𝐴 ++ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ) ∼ ∅ ) )
132 7 131 mpcom ⊢ ( 𝐴 ∈ 𝑊 → ( 𝐴 ++ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ) ∼ ∅ )