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 ⊢ W = I ⁡ Word I × 2 𝑜
efgval.r ⊢ ∼ ˙ = ~ FG ⁡ I
efgval2.m ⊢ M = y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z
efgval2.t ⊢ T = v ∈ W ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w M ⁡ w ”⟩
Assertion efginvrel2 ⊢ A ∈ W → A ++ M ∘ reverse ⁡ A ∼ ˙ ∅

Proof

Step Hyp Ref Expression
1 efgval.w ⊢ W = I ⁡ Word I × 2 𝑜
2 efgval.r ⊢ ∼ ˙ = ~ FG ⁡ I
3 efgval2.m ⊢ M = y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z
4 efgval2.t ⊢ T = v ∈ W ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w M ⁡ w ”⟩
5 fviss ⊢ I ⁡ Word I × 2 𝑜 ⊆ Word I × 2 𝑜
6 1 5 eqsstri ⊢ W ⊆ Word I × 2 𝑜
7 6 sseli ⊢ A ∈ W → A ∈ Word I × 2 𝑜
8 id ⊢ c = ∅ → c = ∅
9 fveq2 ⊢ c = ∅ → reverse ⁡ c = reverse ⁡ ∅
10 rev0 ⊢ reverse ⁡ ∅ = ∅
11 9 10 eqtrdi ⊢ c = ∅ → reverse ⁡ c = ∅
12 11 coeq2d ⊢ c = ∅ → M ∘ reverse ⁡ c = M ∘ ∅
13 co02 ⊢ M ∘ ∅ = ∅
14 12 13 eqtrdi ⊢ c = ∅ → M ∘ reverse ⁡ c = ∅
15 8 14 oveq12d ⊢ c = ∅ → c ++ M ∘ reverse ⁡ c = ∅ ++ ∅
16 15 breq1d ⊢ c = ∅ → c ++ M ∘ reverse ⁡ c ∼ ˙ ∅ ↔ ∅ ++ ∅ ∼ ˙ ∅
17 16 imbi2d ⊢ c = ∅ → A ∈ W → c ++ M ∘ reverse ⁡ c ∼ ˙ ∅ ↔ A ∈ W → ∅ ++ ∅ ∼ ˙ ∅
18 id ⊢ c = a → c = a
19 fveq2 ⊢ c = a → reverse ⁡ c = reverse ⁡ a
20 19 coeq2d ⊢ c = a → M ∘ reverse ⁡ c = M ∘ reverse ⁡ a
21 18 20 oveq12d ⊢ c = a → c ++ M ∘ reverse ⁡ c = a ++ M ∘ reverse ⁡ a
22 21 breq1d ⊢ c = a → c ++ M ∘ reverse ⁡ c ∼ ˙ ∅ ↔ a ++ M ∘ reverse ⁡ a ∼ ˙ ∅
23 22 imbi2d ⊢ c = a → A ∈ W → c ++ M ∘ reverse ⁡ c ∼ ˙ ∅ ↔ A ∈ W → a ++ M ∘ reverse ⁡ a ∼ ˙ ∅
24 id ⊢ c = a ++ ⟨“ b ”⟩ → c = a ++ ⟨“ b ”⟩
25 fveq2 ⊢ c = a ++ ⟨“ b ”⟩ → reverse ⁡ c = reverse ⁡ a ++ ⟨“ b ”⟩
26 25 coeq2d ⊢ c = a ++ ⟨“ b ”⟩ → M ∘ reverse ⁡ c = M ∘ reverse ⁡ a ++ ⟨“ b ”⟩
27 24 26 oveq12d ⊢ c = a ++ ⟨“ b ”⟩ → c ++ M ∘ reverse ⁡ c = a ++ ⟨“ b ”⟩ ++ M ∘ reverse ⁡ a ++ ⟨“ b ”⟩
28 27 breq1d ⊢ c = a ++ ⟨“ b ”⟩ → c ++ M ∘ reverse ⁡ c ∼ ˙ ∅ ↔ a ++ ⟨“ b ”⟩ ++ M ∘ reverse ⁡ a ++ ⟨“ b ”⟩ ∼ ˙ ∅
29 28 imbi2d ⊢ c = a ++ ⟨“ b ”⟩ → A ∈ W → c ++ M ∘ reverse ⁡ c ∼ ˙ ∅ ↔ A ∈ W → a ++ ⟨“ b ”⟩ ++ M ∘ reverse ⁡ a ++ ⟨“ b ”⟩ ∼ ˙ ∅
30 id ⊢ c = A → c = A
31 fveq2 ⊢ c = A → reverse ⁡ c = reverse ⁡ A
32 31 coeq2d ⊢ c = A → M ∘ reverse ⁡ c = M ∘ reverse ⁡ A
33 30 32 oveq12d ⊢ c = A → c ++ M ∘ reverse ⁡ c = A ++ M ∘ reverse ⁡ A
34 33 breq1d ⊢ c = A → c ++ M ∘ reverse ⁡ c ∼ ˙ ∅ ↔ A ++ M ∘ reverse ⁡ A ∼ ˙ ∅
35 34 imbi2d ⊢ c = A → A ∈ W → c ++ M ∘ reverse ⁡ c ∼ ˙ ∅ ↔ A ∈ W → A ++ M ∘ reverse ⁡ A ∼ ˙ ∅
36 ccatidid ⊢ ∅ ++ ∅ = ∅
37 1 2 efger ⊢ ∼ ˙ Er W
38 37 a1i ⊢ A ∈ W → ∼ ˙ Er W
39 wrd0 ⊢ ∅ ∈ Word I × 2 𝑜
40 1 efgrcl ⊢ A ∈ W → I ∈ V ∧ W = Word I × 2 𝑜
41 40 simprd ⊢ A ∈ W → W = Word I × 2 𝑜
42 39 41 eleqtrrid ⊢ A ∈ W → ∅ ∈ W
43 38 42 erref ⊢ A ∈ W → ∅ ∼ ˙ ∅
44 36 43 eqbrtrid ⊢ A ∈ W → ∅ ++ ∅ ∼ ˙ ∅
45 37 a1i ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → ∼ ˙ Er W
46 simprl ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ∈ Word I × 2 𝑜
47 revcl ⊢ a ∈ Word I × 2 𝑜 → reverse ⁡ a ∈ Word I × 2 𝑜
48 47 ad2antrl ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → reverse ⁡ a ∈ Word I × 2 𝑜
49 3 efgmf ⊢ M : I × 2 𝑜 ⟶ I × 2 𝑜
50 wrdco ⊢ reverse ⁡ a ∈ Word I × 2 𝑜 ∧ M : I × 2 𝑜 ⟶ I × 2 𝑜 → M ∘ reverse ⁡ a ∈ Word I × 2 𝑜
51 48 49 50 sylancl ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → M ∘ reverse ⁡ a ∈ Word I × 2 𝑜
52 ccatcl ⊢ a ∈ Word I × 2 𝑜 ∧ M ∘ reverse ⁡ a ∈ Word I × 2 𝑜 → a ++ M ∘ reverse ⁡ a ∈ Word I × 2 𝑜
53 46 51 52 syl2anc ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ++ M ∘ reverse ⁡ a ∈ Word I × 2 𝑜
54 41 adantr ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → W = Word I × 2 𝑜
55 53 54 eleqtrrd ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ++ M ∘ reverse ⁡ a ∈ W
56 lencl ⊢ a ∈ Word I × 2 𝑜 → a ∈ ℕ 0
57 56 ad2antrl ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ∈ ℕ 0
58 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
59 57 58 eleqtrdi ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ∈ ℤ ≥ 0
60 ccatlen ⊢ a ∈ Word I × 2 𝑜 ∧ M ∘ reverse ⁡ a ∈ Word I × 2 𝑜 → a ++ M ∘ reverse ⁡ a = a + M ∘ reverse ⁡ a
61 46 51 60 syl2anc ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ++ M ∘ reverse ⁡ a = a + M ∘ reverse ⁡ a
62 57 nn0zd ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ∈ ℤ
63 62 uzidd ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ∈ ℤ ≥ a
64 lencl ⊢ M ∘ reverse ⁡ a ∈ Word I × 2 𝑜 → M ∘ reverse ⁡ a ∈ ℕ 0
65 51 64 syl ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → M ∘ reverse ⁡ a ∈ ℕ 0
66 uzaddcl ⊢ a ∈ ℤ ≥ a ∧ M ∘ reverse ⁡ a ∈ ℕ 0 → a + M ∘ reverse ⁡ a ∈ ℤ ≥ a
67 63 65 66 syl2anc ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a + M ∘ reverse ⁡ a ∈ ℤ ≥ a
68 61 67 eqeltrd ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ++ M ∘ reverse ⁡ a ∈ ℤ ≥ a
69 elfzuzb ⊢ a ∈ 0 … a ++ M ∘ reverse ⁡ a ↔ a ∈ ℤ ≥ 0 ∧ a ++ M ∘ reverse ⁡ a ∈ ℤ ≥ a
70 59 68 69 sylanbrc ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ∈ 0 … a ++ M ∘ reverse ⁡ a
71 simprr ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → b ∈ I × 2 𝑜
72 1 2 3 4 efgtval ⊢ a ++ M ∘ reverse ⁡ a ∈ W ∧ a ∈ 0 … a ++ M ∘ reverse ⁡ a ∧ b ∈ I × 2 𝑜 → a T ⁡ a ++ M ∘ reverse ⁡ a b = a ++ M ∘ reverse ⁡ a splice a a ⟨“ b M ⁡ b ”⟩
73 55 70 71 72 syl3anc ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a T ⁡ a ++ M ∘ reverse ⁡ a b = a ++ M ∘ reverse ⁡ a splice a a ⟨“ b M ⁡ b ”⟩
74 39 a1i ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → ∅ ∈ Word I × 2 𝑜
75 49 ffvelcdmi ⊢ b ∈ I × 2 𝑜 → M ⁡ b ∈ I × 2 𝑜
76 75 ad2antll ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → M ⁡ b ∈ I × 2 𝑜
77 71 76 s2cld ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → ⟨“ b M ⁡ b ”⟩ ∈ Word I × 2 𝑜
78 ccatrid ⊢ a ∈ Word I × 2 𝑜 → a ++ ∅ = a
79 78 ad2antrl ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ++ ∅ = a
80 79 eqcomd ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a = a ++ ∅
81 80 oveq1d ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ++ M ∘ reverse ⁡ a = a ++ ∅ ++ M ∘ reverse ⁡ a
82 eqidd ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a = a
83 hash0 ⊢ ∅ = 0
84 83 oveq2i ⊢ a + ∅ = a + 0
85 57 nn0cnd ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ∈ ℂ
86 85 addridd ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a + 0 = a
87 84 86 eqtr2id ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a = a + ∅
88 46 74 51 77 81 82 87 splval2 ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ++ M ∘ reverse ⁡ a splice a a ⟨“ b M ⁡ b ”⟩ = a ++ ⟨“ b M ⁡ b ”⟩ ++ M ∘ reverse ⁡ a
89 71 s1cld ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → ⟨“ b ”⟩ ∈ Word I × 2 𝑜
90 revccat ⊢ a ∈ Word I × 2 𝑜 ∧ ⟨“ b ”⟩ ∈ Word I × 2 𝑜 → reverse ⁡ a ++ ⟨“ b ”⟩ = reverse ⁡ ⟨“ b ”⟩ ++ reverse ⁡ a
91 46 89 90 syl2anc ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → reverse ⁡ a ++ ⟨“ b ”⟩ = reverse ⁡ ⟨“ b ”⟩ ++ reverse ⁡ a
92 revs1 ⊢ reverse ⁡ ⟨“ b ”⟩ = ⟨“ b ”⟩
93 92 oveq1i ⊢ reverse ⁡ ⟨“ b ”⟩ ++ reverse ⁡ a = ⟨“ b ”⟩ ++ reverse ⁡ a
94 91 93 eqtrdi ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → reverse ⁡ a ++ ⟨“ b ”⟩ = ⟨“ b ”⟩ ++ reverse ⁡ a
95 94 coeq2d ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → M ∘ reverse ⁡ a ++ ⟨“ b ”⟩ = M ∘ ⟨“ b ”⟩ ++ reverse ⁡ a
96 49 a1i ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → M : I × 2 𝑜 ⟶ I × 2 𝑜
97 ccatco ⊢ ⟨“ b ”⟩ ∈ Word I × 2 𝑜 ∧ reverse ⁡ a ∈ Word I × 2 𝑜 ∧ M : I × 2 𝑜 ⟶ I × 2 𝑜 → M ∘ ⟨“ b ”⟩ ++ reverse ⁡ a = M ∘ ⟨“ b ”⟩ ++ M ∘ reverse ⁡ a
98 89 48 96 97 syl3anc ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → M ∘ ⟨“ b ”⟩ ++ reverse ⁡ a = M ∘ ⟨“ b ”⟩ ++ M ∘ reverse ⁡ a
99 s1co ⊢ b ∈ I × 2 𝑜 ∧ M : I × 2 𝑜 ⟶ I × 2 𝑜 → M ∘ ⟨“ b ”⟩ = ⟨“ M ⁡ b ”⟩
100 71 49 99 sylancl ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → M ∘ ⟨“ b ”⟩ = ⟨“ M ⁡ b ”⟩
101 100 oveq1d ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → M ∘ ⟨“ b ”⟩ ++ M ∘ reverse ⁡ a = ⟨“ M ⁡ b ”⟩ ++ M ∘ reverse ⁡ a
102 95 98 101 3eqtrd ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → M ∘ reverse ⁡ a ++ ⟨“ b ”⟩ = ⟨“ M ⁡ b ”⟩ ++ M ∘ reverse ⁡ a
103 102 oveq2d ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ++ ⟨“ b ”⟩ ++ M ∘ reverse ⁡ a ++ ⟨“ b ”⟩ = a ++ ⟨“ b ”⟩ ++ ⟨“ M ⁡ b ”⟩ ++ M ∘ reverse ⁡ a
104 ccatcl ⊢ a ∈ Word I × 2 𝑜 ∧ ⟨“ b ”⟩ ∈ Word I × 2 𝑜 → a ++ ⟨“ b ”⟩ ∈ Word I × 2 𝑜
105 46 89 104 syl2anc ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ++ ⟨“ b ”⟩ ∈ Word I × 2 𝑜
106 76 s1cld ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → ⟨“ M ⁡ b ”⟩ ∈ Word I × 2 𝑜
107 ccatass ⊢ a ++ ⟨“ b ”⟩ ∈ Word I × 2 𝑜 ∧ ⟨“ M ⁡ b ”⟩ ∈ Word I × 2 𝑜 ∧ M ∘ reverse ⁡ a ∈ Word I × 2 𝑜 → a ++ ⟨“ b ”⟩ ++ ⟨“ M ⁡ b ”⟩ ++ M ∘ reverse ⁡ a = a ++ ⟨“ b ”⟩ ++ ⟨“ M ⁡ b ”⟩ ++ M ∘ reverse ⁡ a
108 105 106 51 107 syl3anc ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ++ ⟨“ b ”⟩ ++ ⟨“ M ⁡ b ”⟩ ++ M ∘ reverse ⁡ a = a ++ ⟨“ b ”⟩ ++ ⟨“ M ⁡ b ”⟩ ++ M ∘ reverse ⁡ a
109 ccatass ⊢ a ∈ Word I × 2 𝑜 ∧ ⟨“ b ”⟩ ∈ Word I × 2 𝑜 ∧ ⟨“ M ⁡ b ”⟩ ∈ Word I × 2 𝑜 → a ++ ⟨“ b ”⟩ ++ ⟨“ M ⁡ b ”⟩ = a ++ ⟨“ b ”⟩ ++ ⟨“ M ⁡ b ”⟩
110 46 89 106 109 syl3anc ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ++ ⟨“ b ”⟩ ++ ⟨“ M ⁡ b ”⟩ = a ++ ⟨“ b ”⟩ ++ ⟨“ M ⁡ b ”⟩
111 df-s2 ⊢ ⟨“ b M ⁡ b ”⟩ = ⟨“ b ”⟩ ++ ⟨“ M ⁡ b ”⟩
112 111 oveq2i ⊢ a ++ ⟨“ b M ⁡ b ”⟩ = a ++ ⟨“ b ”⟩ ++ ⟨“ M ⁡ b ”⟩
113 110 112 eqtr4di ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ++ ⟨“ b ”⟩ ++ ⟨“ M ⁡ b ”⟩ = a ++ ⟨“ b M ⁡ b ”⟩
114 113 oveq1d ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ++ ⟨“ b ”⟩ ++ ⟨“ M ⁡ b ”⟩ ++ M ∘ reverse ⁡ a = a ++ ⟨“ b M ⁡ b ”⟩ ++ M ∘ reverse ⁡ a
115 103 108 114 3eqtr2rd ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ++ ⟨“ b M ⁡ b ”⟩ ++ M ∘ reverse ⁡ a = a ++ ⟨“ b ”⟩ ++ M ∘ reverse ⁡ a ++ ⟨“ b ”⟩
116 73 88 115 3eqtrd ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a T ⁡ a ++ M ∘ reverse ⁡ a b = a ++ ⟨“ b ”⟩ ++ M ∘ reverse ⁡ a ++ ⟨“ b ”⟩
117 1 2 3 4 efgtf ⊢ a ++ M ∘ reverse ⁡ a ∈ W → T ⁡ a ++ M ∘ reverse ⁡ a = m ∈ 0 … a ++ M ∘ reverse ⁡ a , u ∈ I × 2 𝑜 ⟼ a ++ M ∘ reverse ⁡ a splice m m ⟨“ u M ⁡ u ”⟩ ∧ T ⁡ a ++ M ∘ reverse ⁡ a : 0 … a ++ M ∘ reverse ⁡ a × I × 2 𝑜 ⟶ W
118 117 simprd ⊢ a ++ M ∘ reverse ⁡ a ∈ W → T ⁡ a ++ M ∘ reverse ⁡ a : 0 … a ++ M ∘ reverse ⁡ a × I × 2 𝑜 ⟶ W
119 55 118 syl ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → T ⁡ a ++ M ∘ reverse ⁡ a : 0 … a ++ M ∘ reverse ⁡ a × I × 2 𝑜 ⟶ W
120 119 ffnd ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → T ⁡ a ++ M ∘ reverse ⁡ a Fn 0 … a ++ M ∘ reverse ⁡ a × I × 2 𝑜
121 fnovrn ⊢ T ⁡ a ++ M ∘ reverse ⁡ a Fn 0 … a ++ M ∘ reverse ⁡ a × I × 2 𝑜 ∧ a ∈ 0 … a ++ M ∘ reverse ⁡ a ∧ b ∈ I × 2 𝑜 → a T ⁡ a ++ M ∘ reverse ⁡ a b ∈ ran ⁡ T ⁡ a ++ M ∘ reverse ⁡ a
122 120 70 71 121 syl3anc ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a T ⁡ a ++ M ∘ reverse ⁡ a b ∈ ran ⁡ T ⁡ a ++ M ∘ reverse ⁡ a
123 116 122 eqeltrrd ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ++ ⟨“ b ”⟩ ++ M ∘ reverse ⁡ a ++ ⟨“ b ”⟩ ∈ ran ⁡ T ⁡ a ++ M ∘ reverse ⁡ a
124 1 2 3 4 efgi2 ⊢ a ++ M ∘ reverse ⁡ a ∈ W ∧ a ++ ⟨“ b ”⟩ ++ M ∘ reverse ⁡ a ++ ⟨“ b ”⟩ ∈ ran ⁡ T ⁡ a ++ M ∘ reverse ⁡ a → a ++ M ∘ reverse ⁡ a ∼ ˙ a ++ ⟨“ b ”⟩ ++ M ∘ reverse ⁡ a ++ ⟨“ b ”⟩
125 55 123 124 syl2anc ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ++ M ∘ reverse ⁡ a ∼ ˙ a ++ ⟨“ b ”⟩ ++ M ∘ reverse ⁡ a ++ ⟨“ b ”⟩
126 45 125 ersym ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ++ ⟨“ b ”⟩ ++ M ∘ reverse ⁡ a ++ ⟨“ b ”⟩ ∼ ˙ a ++ M ∘ reverse ⁡ a
127 45 ertr ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ++ ⟨“ b ”⟩ ++ M ∘ reverse ⁡ a ++ ⟨“ b ”⟩ ∼ ˙ a ++ M ∘ reverse ⁡ a ∧ a ++ M ∘ reverse ⁡ a ∼ ˙ ∅ → a ++ ⟨“ b ”⟩ ++ M ∘ reverse ⁡ a ++ ⟨“ b ”⟩ ∼ ˙ ∅
128 126 127 mpand ⊢ A ∈ W ∧ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → a ++ M ∘ reverse ⁡ a ∼ ˙ ∅ → a ++ ⟨“ b ”⟩ ++ M ∘ reverse ⁡ a ++ ⟨“ b ”⟩ ∼ ˙ ∅
129 128 expcom ⊢ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → A ∈ W → a ++ M ∘ reverse ⁡ a ∼ ˙ ∅ → a ++ ⟨“ b ”⟩ ++ M ∘ reverse ⁡ a ++ ⟨“ b ”⟩ ∼ ˙ ∅
130 129 a2d ⊢ a ∈ Word I × 2 𝑜 ∧ b ∈ I × 2 𝑜 → A ∈ W → a ++ M ∘ reverse ⁡ a ∼ ˙ ∅ → A ∈ W → a ++ ⟨“ b ”⟩ ++ M ∘ reverse ⁡ a ++ ⟨“ b ”⟩ ∼ ˙ ∅
131 17 23 29 35 44 130 wrdind ⊢ A ∈ Word I × 2 𝑜 → A ∈ W → A ++ M ∘ reverse ⁡ A ∼ ˙ ∅
132 7 131 mpcom ⊢ A ∈ W → A ++ M ∘ reverse ⁡ A ∼ ˙ ∅