# 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}=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
efgval.r
efgval2.m ${⊢}{M}=\left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)$
efgval2.t ${⊢}{T}=\left({v}\in {W}⟼\left({n}\in \left(0\dots \left|{v}\right|\right),{w}\in \left({I}×{2}_{𝑜}\right)⟼{v}\mathrm{splice}⟨{n},{n},⟨“{w}{M}\left({w}\right)”⟩⟩\right)\right)$
Assertion efginvrel2

### Proof

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