# Metamath Proof Explorer

## Theorem revccat

Description: Antiautomorphic property of the reversal operation. (Contributed by Stefan O'Rear, 27-Aug-2015)

Ref Expression
Assertion revccat ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \mathrm{reverse}\left({S}\mathrm{++}{T}\right)=\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)$

### Proof

Step Hyp Ref Expression
1 ccatcl ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to {S}\mathrm{++}{T}\in \mathrm{Word}{A}$
2 revcl ${⊢}{S}\mathrm{++}{T}\in \mathrm{Word}{A}\to \mathrm{reverse}\left({S}\mathrm{++}{T}\right)\in \mathrm{Word}{A}$
3 wrdfn ${⊢}\mathrm{reverse}\left({S}\mathrm{++}{T}\right)\in \mathrm{Word}{A}\to \mathrm{reverse}\left({S}\mathrm{++}{T}\right)Fn\left(0..^\left|\mathrm{reverse}\left({S}\mathrm{++}{T}\right)\right|\right)$
4 1 2 3 3syl ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \mathrm{reverse}\left({S}\mathrm{++}{T}\right)Fn\left(0..^\left|\mathrm{reverse}\left({S}\mathrm{++}{T}\right)\right|\right)$
5 revlen ${⊢}{S}\mathrm{++}{T}\in \mathrm{Word}{A}\to \left|\mathrm{reverse}\left({S}\mathrm{++}{T}\right)\right|=\left|{S}\mathrm{++}{T}\right|$
6 1 5 syl ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|\mathrm{reverse}\left({S}\mathrm{++}{T}\right)\right|=\left|{S}\mathrm{++}{T}\right|$
7 ccatlen ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{S}\mathrm{++}{T}\right|=\left|{S}\right|+\left|{T}\right|$
8 lencl ${⊢}{S}\in \mathrm{Word}{A}\to \left|{S}\right|\in {ℕ}_{0}$
9 8 nn0cnd ${⊢}{S}\in \mathrm{Word}{A}\to \left|{S}\right|\in ℂ$
10 lencl ${⊢}{T}\in \mathrm{Word}{A}\to \left|{T}\right|\in {ℕ}_{0}$
11 10 nn0cnd ${⊢}{T}\in \mathrm{Word}{A}\to \left|{T}\right|\in ℂ$
12 addcom ${⊢}\left(\left|{S}\right|\in ℂ\wedge \left|{T}\right|\in ℂ\right)\to \left|{S}\right|+\left|{T}\right|=\left|{T}\right|+\left|{S}\right|$
13 9 11 12 syl2an ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{S}\right|+\left|{T}\right|=\left|{T}\right|+\left|{S}\right|$
14 6 7 13 3eqtrd ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|\mathrm{reverse}\left({S}\mathrm{++}{T}\right)\right|=\left|{T}\right|+\left|{S}\right|$
15 14 oveq2d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left(0..^\left|\mathrm{reverse}\left({S}\mathrm{++}{T}\right)\right|\right)=\left(0..^\left|{T}\right|+\left|{S}\right|\right)$
16 15 fneq2d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left(\mathrm{reverse}\left({S}\mathrm{++}{T}\right)Fn\left(0..^\left|\mathrm{reverse}\left({S}\mathrm{++}{T}\right)\right|\right)↔\mathrm{reverse}\left({S}\mathrm{++}{T}\right)Fn\left(0..^\left|{T}\right|+\left|{S}\right|\right)\right)$
17 4 16 mpbid ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \mathrm{reverse}\left({S}\mathrm{++}{T}\right)Fn\left(0..^\left|{T}\right|+\left|{S}\right|\right)$
18 revcl ${⊢}{T}\in \mathrm{Word}{A}\to \mathrm{reverse}\left({T}\right)\in \mathrm{Word}{A}$
19 revcl ${⊢}{S}\in \mathrm{Word}{A}\to \mathrm{reverse}\left({S}\right)\in \mathrm{Word}{A}$
20 ccatcl ${⊢}\left(\mathrm{reverse}\left({T}\right)\in \mathrm{Word}{A}\wedge \mathrm{reverse}\left({S}\right)\in \mathrm{Word}{A}\right)\to \mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\in \mathrm{Word}{A}$
21 18 19 20 syl2anr ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\in \mathrm{Word}{A}$
22 wrdfn ${⊢}\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\in \mathrm{Word}{A}\to \left(\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\right)Fn\left(0..^\left|\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\right|\right)$
23 21 22 syl ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left(\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\right)Fn\left(0..^\left|\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\right|\right)$
24 ccatlen ${⊢}\left(\mathrm{reverse}\left({T}\right)\in \mathrm{Word}{A}\wedge \mathrm{reverse}\left({S}\right)\in \mathrm{Word}{A}\right)\to \left|\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\right|=\left|\mathrm{reverse}\left({T}\right)\right|+\left|\mathrm{reverse}\left({S}\right)\right|$
25 18 19 24 syl2anr ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\right|=\left|\mathrm{reverse}\left({T}\right)\right|+\left|\mathrm{reverse}\left({S}\right)\right|$
26 revlen ${⊢}{T}\in \mathrm{Word}{A}\to \left|\mathrm{reverse}\left({T}\right)\right|=\left|{T}\right|$
27 revlen ${⊢}{S}\in \mathrm{Word}{A}\to \left|\mathrm{reverse}\left({S}\right)\right|=\left|{S}\right|$
28 26 27 oveqan12rd ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|\mathrm{reverse}\left({T}\right)\right|+\left|\mathrm{reverse}\left({S}\right)\right|=\left|{T}\right|+\left|{S}\right|$
29 25 28 eqtrd ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\right|=\left|{T}\right|+\left|{S}\right|$
30 29 oveq2d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left(0..^\left|\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\right|\right)=\left(0..^\left|{T}\right|+\left|{S}\right|\right)$
31 30 fneq2d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left(\left(\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\right)Fn\left(0..^\left|\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\right|\right)↔\left(\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\right)Fn\left(0..^\left|{T}\right|+\left|{S}\right|\right)\right)$
32 23 31 mpbid ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left(\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\right)Fn\left(0..^\left|{T}\right|+\left|{S}\right|\right)$
33 id ${⊢}{x}\in \left(0..^\left|{T}\right|+\left|{S}\right|\right)\to {x}\in \left(0..^\left|{T}\right|+\left|{S}\right|\right)$
34 10 nn0zd ${⊢}{T}\in \mathrm{Word}{A}\to \left|{T}\right|\in ℤ$
35 34 adantl ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{T}\right|\in ℤ$
36 fzospliti ${⊢}\left({x}\in \left(0..^\left|{T}\right|+\left|{S}\right|\right)\wedge \left|{T}\right|\in ℤ\right)\to \left({x}\in \left(0..^\left|{T}\right|\right)\vee {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)$
37 33 35 36 syl2anr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|+\left|{S}\right|\right)\right)\to \left({x}\in \left(0..^\left|{T}\right|\right)\vee {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)$
38 simpll ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to {S}\in \mathrm{Word}{A}$
39 simplr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to {T}\in \mathrm{Word}{A}$
40 fzoval ${⊢}\left|{T}\right|\in ℤ\to \left(0..^\left|{T}\right|\right)=\left(0\dots \left|{T}\right|-1\right)$
41 34 40 syl ${⊢}{T}\in \mathrm{Word}{A}\to \left(0..^\left|{T}\right|\right)=\left(0\dots \left|{T}\right|-1\right)$
42 41 adantl ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left(0..^\left|{T}\right|\right)=\left(0\dots \left|{T}\right|-1\right)$
43 42 eleq2d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left({x}\in \left(0..^\left|{T}\right|\right)↔{x}\in \left(0\dots \left|{T}\right|-1\right)\right)$
44 43 biimpa ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to {x}\in \left(0\dots \left|{T}\right|-1\right)$
45 fznn0sub2 ${⊢}{x}\in \left(0\dots \left|{T}\right|-1\right)\to \left|{T}\right|-1-{x}\in \left(0\dots \left|{T}\right|-1\right)$
46 44 45 syl ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to \left|{T}\right|-1-{x}\in \left(0\dots \left|{T}\right|-1\right)$
47 41 ad2antlr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to \left(0..^\left|{T}\right|\right)=\left(0\dots \left|{T}\right|-1\right)$
48 46 47 eleqtrrd ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to \left|{T}\right|-1-{x}\in \left(0..^\left|{T}\right|\right)$
49 ccatval3 ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\wedge \left|{T}\right|-1-{x}\in \left(0..^\left|{T}\right|\right)\right)\to \left({S}\mathrm{++}{T}\right)\left(\left(\left|{T}\right|-1\right)-{x}+\left|{S}\right|\right)={T}\left(\left|{T}\right|-1-{x}\right)$
50 38 39 48 49 syl3anc ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to \left({S}\mathrm{++}{T}\right)\left(\left(\left|{T}\right|-1\right)-{x}+\left|{S}\right|\right)={T}\left(\left|{T}\right|-1-{x}\right)$
51 7 13 eqtrd ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{S}\mathrm{++}{T}\right|=\left|{T}\right|+\left|{S}\right|$
52 51 oveq1d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{S}\mathrm{++}{T}\right|-1=\left|{T}\right|+\left|{S}\right|-1$
53 11 adantl ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{T}\right|\in ℂ$
54 9 adantr ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{S}\right|\in ℂ$
55 1cnd ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to 1\in ℂ$
56 53 54 55 addsubd ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{T}\right|+\left|{S}\right|-1=\left|{T}\right|-1+\left|{S}\right|$
57 52 56 eqtrd ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{S}\mathrm{++}{T}\right|-1=\left|{T}\right|-1+\left|{S}\right|$
58 57 oveq1d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{S}\mathrm{++}{T}\right|-1-{x}=\left(\left|{T}\right|-1\right)+\left|{S}\right|-{x}$
59 58 adantr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to \left|{S}\mathrm{++}{T}\right|-1-{x}=\left(\left|{T}\right|-1\right)+\left|{S}\right|-{x}$
60 peano2zm ${⊢}\left|{T}\right|\in ℤ\to \left|{T}\right|-1\in ℤ$
61 34 60 syl ${⊢}{T}\in \mathrm{Word}{A}\to \left|{T}\right|-1\in ℤ$
62 61 zcnd ${⊢}{T}\in \mathrm{Word}{A}\to \left|{T}\right|-1\in ℂ$
63 62 ad2antlr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to \left|{T}\right|-1\in ℂ$
64 9 ad2antrr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to \left|{S}\right|\in ℂ$
65 elfzoelz ${⊢}{x}\in \left(0..^\left|{T}\right|\right)\to {x}\in ℤ$
66 65 zcnd ${⊢}{x}\in \left(0..^\left|{T}\right|\right)\to {x}\in ℂ$
67 66 adantl ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to {x}\in ℂ$
68 63 64 67 addsubd ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to \left(\left|{T}\right|-1\right)+\left|{S}\right|-{x}=\left(\left|{T}\right|-1\right)-{x}+\left|{S}\right|$
69 59 68 eqtrd ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to \left|{S}\mathrm{++}{T}\right|-1-{x}=\left(\left|{T}\right|-1\right)-{x}+\left|{S}\right|$
70 69 fveq2d ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to \left({S}\mathrm{++}{T}\right)\left(\left|{S}\mathrm{++}{T}\right|-1-{x}\right)=\left({S}\mathrm{++}{T}\right)\left(\left(\left|{T}\right|-1\right)-{x}+\left|{S}\right|\right)$
71 revfv ${⊢}\left({T}\in \mathrm{Word}{A}\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to \mathrm{reverse}\left({T}\right)\left({x}\right)={T}\left(\left|{T}\right|-1-{x}\right)$
72 71 adantll ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to \mathrm{reverse}\left({T}\right)\left({x}\right)={T}\left(\left|{T}\right|-1-{x}\right)$
73 50 70 72 3eqtr4d ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to \left({S}\mathrm{++}{T}\right)\left(\left|{S}\mathrm{++}{T}\right|-1-{x}\right)=\mathrm{reverse}\left({T}\right)\left({x}\right)$
74 34 uzidd ${⊢}{T}\in \mathrm{Word}{A}\to \left|{T}\right|\in {ℤ}_{\ge \left|{T}\right|}$
75 uzaddcl ${⊢}\left(\left|{T}\right|\in {ℤ}_{\ge \left|{T}\right|}\wedge \left|{S}\right|\in {ℕ}_{0}\right)\to \left|{T}\right|+\left|{S}\right|\in {ℤ}_{\ge \left|{T}\right|}$
76 74 8 75 syl2anr ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{T}\right|+\left|{S}\right|\in {ℤ}_{\ge \left|{T}\right|}$
77 51 76 eqeltrd ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{S}\mathrm{++}{T}\right|\in {ℤ}_{\ge \left|{T}\right|}$
78 fzoss2 ${⊢}\left|{S}\mathrm{++}{T}\right|\in {ℤ}_{\ge \left|{T}\right|}\to \left(0..^\left|{T}\right|\right)\subseteq \left(0..^\left|{S}\mathrm{++}{T}\right|\right)$
79 77 78 syl ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left(0..^\left|{T}\right|\right)\subseteq \left(0..^\left|{S}\mathrm{++}{T}\right|\right)$
80 79 sselda ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to {x}\in \left(0..^\left|{S}\mathrm{++}{T}\right|\right)$
81 revfv ${⊢}\left({S}\mathrm{++}{T}\in \mathrm{Word}{A}\wedge {x}\in \left(0..^\left|{S}\mathrm{++}{T}\right|\right)\right)\to \mathrm{reverse}\left({S}\mathrm{++}{T}\right)\left({x}\right)=\left({S}\mathrm{++}{T}\right)\left(\left|{S}\mathrm{++}{T}\right|-1-{x}\right)$
82 1 80 81 syl2an2r ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to \mathrm{reverse}\left({S}\mathrm{++}{T}\right)\left({x}\right)=\left({S}\mathrm{++}{T}\right)\left(\left|{S}\mathrm{++}{T}\right|-1-{x}\right)$
83 18 ad2antlr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to \mathrm{reverse}\left({T}\right)\in \mathrm{Word}{A}$
84 19 ad2antrr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to \mathrm{reverse}\left({S}\right)\in \mathrm{Word}{A}$
85 26 adantl ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|\mathrm{reverse}\left({T}\right)\right|=\left|{T}\right|$
86 85 oveq2d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left(0..^\left|\mathrm{reverse}\left({T}\right)\right|\right)=\left(0..^\left|{T}\right|\right)$
87 86 eleq2d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left({x}\in \left(0..^\left|\mathrm{reverse}\left({T}\right)\right|\right)↔{x}\in \left(0..^\left|{T}\right|\right)\right)$
88 87 biimpar ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to {x}\in \left(0..^\left|\mathrm{reverse}\left({T}\right)\right|\right)$
89 ccatval1 ${⊢}\left(\mathrm{reverse}\left({T}\right)\in \mathrm{Word}{A}\wedge \mathrm{reverse}\left({S}\right)\in \mathrm{Word}{A}\wedge {x}\in \left(0..^\left|\mathrm{reverse}\left({T}\right)\right|\right)\right)\to \left(\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\right)\left({x}\right)=\mathrm{reverse}\left({T}\right)\left({x}\right)$
90 83 84 88 89 syl3anc ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to \left(\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\right)\left({x}\right)=\mathrm{reverse}\left({T}\right)\left({x}\right)$
91 73 82 90 3eqtr4d ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|\right)\right)\to \mathrm{reverse}\left({S}\mathrm{++}{T}\right)\left({x}\right)=\left(\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\right)\left({x}\right)$
92 8 nn0zd ${⊢}{S}\in \mathrm{Word}{A}\to \left|{S}\right|\in ℤ$
93 peano2zm ${⊢}\left|{S}\right|\in ℤ\to \left|{S}\right|-1\in ℤ$
94 92 93 syl ${⊢}{S}\in \mathrm{Word}{A}\to \left|{S}\right|-1\in ℤ$
95 94 zcnd ${⊢}{S}\in \mathrm{Word}{A}\to \left|{S}\right|-1\in ℂ$
96 95 ad2antrr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to \left|{S}\right|-1\in ℂ$
97 elfzoelz ${⊢}{x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\to {x}\in ℤ$
98 97 zcnd ${⊢}{x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\to {x}\in ℂ$
99 98 adantl ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to {x}\in ℂ$
100 11 ad2antlr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to \left|{T}\right|\in ℂ$
101 96 99 100 subsub3d ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to \left|{S}\right|-1-\left({x}-\left|{T}\right|\right)=\left(\left|{S}\right|-1\right)+\left|{T}\right|-{x}$
102 26 oveq2d ${⊢}{T}\in \mathrm{Word}{A}\to {x}-\left|\mathrm{reverse}\left({T}\right)\right|={x}-\left|{T}\right|$
103 102 oveq2d ${⊢}{T}\in \mathrm{Word}{A}\to \left|{S}\right|-1-\left({x}-\left|\mathrm{reverse}\left({T}\right)\right|\right)=\left|{S}\right|-1-\left({x}-\left|{T}\right|\right)$
104 103 ad2antlr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to \left|{S}\right|-1-\left({x}-\left|\mathrm{reverse}\left({T}\right)\right|\right)=\left|{S}\right|-1-\left({x}-\left|{T}\right|\right)$
105 7 oveq1d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{S}\mathrm{++}{T}\right|-1=\left|{S}\right|+\left|{T}\right|-1$
106 54 53 55 addsubd ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{S}\right|+\left|{T}\right|-1=\left|{S}\right|-1+\left|{T}\right|$
107 105 106 eqtrd ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{S}\mathrm{++}{T}\right|-1=\left|{S}\right|-1+\left|{T}\right|$
108 107 oveq1d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{S}\mathrm{++}{T}\right|-1-{x}=\left(\left|{S}\right|-1\right)+\left|{T}\right|-{x}$
109 108 adantr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to \left|{S}\mathrm{++}{T}\right|-1-{x}=\left(\left|{S}\right|-1\right)+\left|{T}\right|-{x}$
110 101 104 109 3eqtr4rd ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to \left|{S}\mathrm{++}{T}\right|-1-{x}=\left|{S}\right|-1-\left({x}-\left|\mathrm{reverse}\left({T}\right)\right|\right)$
111 110 fveq2d ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to {S}\left(\left|{S}\mathrm{++}{T}\right|-1-{x}\right)={S}\left(\left|{S}\right|-1-\left({x}-\left|\mathrm{reverse}\left({T}\right)\right|\right)\right)$
112 simpll ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to {S}\in \mathrm{Word}{A}$
113 simplr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to {T}\in \mathrm{Word}{A}$
114 zaddcl ${⊢}\left(\left|{T}\right|\in ℤ\wedge \left|{S}\right|\in ℤ\right)\to \left|{T}\right|+\left|{S}\right|\in ℤ$
115 34 92 114 syl2anr ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{T}\right|+\left|{S}\right|\in ℤ$
116 peano2zm ${⊢}\left|{T}\right|+\left|{S}\right|\in ℤ\to \left|{T}\right|+\left|{S}\right|-1\in ℤ$
117 115 116 syl ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{T}\right|+\left|{S}\right|-1\in ℤ$
118 fzoval ${⊢}\left|{T}\right|+\left|{S}\right|\in ℤ\to \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)=\left(\left|{T}\right|\dots \left|{T}\right|+\left|{S}\right|-1\right)$
119 115 118 syl ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)=\left(\left|{T}\right|\dots \left|{T}\right|+\left|{S}\right|-1\right)$
120 119 eleq2d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left({x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)↔{x}\in \left(\left|{T}\right|\dots \left|{T}\right|+\left|{S}\right|-1\right)\right)$
121 120 biimpa ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to {x}\in \left(\left|{T}\right|\dots \left|{T}\right|+\left|{S}\right|-1\right)$
122 fzrev2i ${⊢}\left(\left|{T}\right|+\left|{S}\right|-1\in ℤ\wedge {x}\in \left(\left|{T}\right|\dots \left|{T}\right|+\left|{S}\right|-1\right)\right)\to \left(\left|{T}\right|+\left|{S}\right|\right)-1-{x}\in \left(\left(\left|{T}\right|+\left|{S}\right|\right)-1-\left(\left|{T}\right|+\left|{S}\right|-1\right)\dots \left(\left|{T}\right|+\left|{S}\right|\right)-1-\left|{T}\right|\right)$
123 117 121 122 syl2an2r ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to \left(\left|{T}\right|+\left|{S}\right|\right)-1-{x}\in \left(\left(\left|{T}\right|+\left|{S}\right|\right)-1-\left(\left|{T}\right|+\left|{S}\right|-1\right)\dots \left(\left|{T}\right|+\left|{S}\right|\right)-1-\left|{T}\right|\right)$
124 52 oveq1d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{S}\mathrm{++}{T}\right|-1-{x}=\left(\left|{T}\right|+\left|{S}\right|\right)-1-{x}$
125 124 adantr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to \left|{S}\mathrm{++}{T}\right|-1-{x}=\left(\left|{T}\right|+\left|{S}\right|\right)-1-{x}$
126 92 adantr ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{S}\right|\in ℤ$
127 fzoval ${⊢}\left|{S}\right|\in ℤ\to \left(0..^\left|{S}\right|\right)=\left(0\dots \left|{S}\right|-1\right)$
128 126 127 syl ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left(0..^\left|{S}\right|\right)=\left(0\dots \left|{S}\right|-1\right)$
129 117 zcnd ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{T}\right|+\left|{S}\right|-1\in ℂ$
130 129 subidd ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left(\left|{T}\right|+\left|{S}\right|\right)-1-\left(\left|{T}\right|+\left|{S}\right|-1\right)=0$
131 addcl ${⊢}\left(\left|{T}\right|\in ℂ\wedge \left|{S}\right|\in ℂ\right)\to \left|{T}\right|+\left|{S}\right|\in ℂ$
132 11 9 131 syl2anr ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{T}\right|+\left|{S}\right|\in ℂ$
133 132 55 53 sub32d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left(\left|{T}\right|+\left|{S}\right|\right)-1-\left|{T}\right|=\left(\left|{T}\right|+\left|{S}\right|\right)-\left|{T}\right|-1$
134 pncan2 ${⊢}\left(\left|{T}\right|\in ℂ\wedge \left|{S}\right|\in ℂ\right)\to \left|{T}\right|+\left|{S}\right|-\left|{T}\right|=\left|{S}\right|$
135 11 9 134 syl2anr ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left|{T}\right|+\left|{S}\right|-\left|{T}\right|=\left|{S}\right|$
136 135 oveq1d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left(\left|{T}\right|+\left|{S}\right|\right)-\left|{T}\right|-1=\left|{S}\right|-1$
137 133 136 eqtrd ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left(\left|{T}\right|+\left|{S}\right|\right)-1-\left|{T}\right|=\left|{S}\right|-1$
138 130 137 oveq12d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left(\left(\left|{T}\right|+\left|{S}\right|\right)-1-\left(\left|{T}\right|+\left|{S}\right|-1\right)\dots \left(\left|{T}\right|+\left|{S}\right|\right)-1-\left|{T}\right|\right)=\left(0\dots \left|{S}\right|-1\right)$
139 128 138 eqtr4d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left(0..^\left|{S}\right|\right)=\left(\left(\left|{T}\right|+\left|{S}\right|\right)-1-\left(\left|{T}\right|+\left|{S}\right|-1\right)\dots \left(\left|{T}\right|+\left|{S}\right|\right)-1-\left|{T}\right|\right)$
140 139 adantr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to \left(0..^\left|{S}\right|\right)=\left(\left(\left|{T}\right|+\left|{S}\right|\right)-1-\left(\left|{T}\right|+\left|{S}\right|-1\right)\dots \left(\left|{T}\right|+\left|{S}\right|\right)-1-\left|{T}\right|\right)$
141 123 125 140 3eltr4d ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to \left|{S}\mathrm{++}{T}\right|-1-{x}\in \left(0..^\left|{S}\right|\right)$
142 ccatval1 ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\wedge \left|{S}\mathrm{++}{T}\right|-1-{x}\in \left(0..^\left|{S}\right|\right)\right)\to \left({S}\mathrm{++}{T}\right)\left(\left|{S}\mathrm{++}{T}\right|-1-{x}\right)={S}\left(\left|{S}\mathrm{++}{T}\right|-1-{x}\right)$
143 112 113 141 142 syl3anc ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to \left({S}\mathrm{++}{T}\right)\left(\left|{S}\mathrm{++}{T}\right|-1-{x}\right)={S}\left(\left|{S}\mathrm{++}{T}\right|-1-{x}\right)$
144 simpl ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to {S}\in \mathrm{Word}{A}$
145 102 ad2antlr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to {x}-\left|\mathrm{reverse}\left({T}\right)\right|={x}-\left|{T}\right|$
146 id ${⊢}{x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\to {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)$
147 fzosubel3 ${⊢}\left({x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\wedge \left|{S}\right|\in ℤ\right)\to {x}-\left|{T}\right|\in \left(0..^\left|{S}\right|\right)$
148 146 126 147 syl2anr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to {x}-\left|{T}\right|\in \left(0..^\left|{S}\right|\right)$
149 145 148 eqeltrd ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to {x}-\left|\mathrm{reverse}\left({T}\right)\right|\in \left(0..^\left|{S}\right|\right)$
150 revfv ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {x}-\left|\mathrm{reverse}\left({T}\right)\right|\in \left(0..^\left|{S}\right|\right)\right)\to \mathrm{reverse}\left({S}\right)\left({x}-\left|\mathrm{reverse}\left({T}\right)\right|\right)={S}\left(\left|{S}\right|-1-\left({x}-\left|\mathrm{reverse}\left({T}\right)\right|\right)\right)$
151 144 149 150 syl2an2r ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to \mathrm{reverse}\left({S}\right)\left({x}-\left|\mathrm{reverse}\left({T}\right)\right|\right)={S}\left(\left|{S}\right|-1-\left({x}-\left|\mathrm{reverse}\left({T}\right)\right|\right)\right)$
152 111 143 151 3eqtr4d ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to \left({S}\mathrm{++}{T}\right)\left(\left|{S}\mathrm{++}{T}\right|-1-{x}\right)=\mathrm{reverse}\left({S}\right)\left({x}-\left|\mathrm{reverse}\left({T}\right)\right|\right)$
153 fzoss1 ${⊢}\left|{T}\right|\in {ℤ}_{\ge 0}\to \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\subseteq \left(0..^\left|{T}\right|+\left|{S}\right|\right)$
154 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
155 153 154 eleq2s ${⊢}\left|{T}\right|\in {ℕ}_{0}\to \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\subseteq \left(0..^\left|{T}\right|+\left|{S}\right|\right)$
156 10 155 syl ${⊢}{T}\in \mathrm{Word}{A}\to \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\subseteq \left(0..^\left|{T}\right|+\left|{S}\right|\right)$
157 156 adantl ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\subseteq \left(0..^\left|{T}\right|+\left|{S}\right|\right)$
158 51 oveq2d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left(0..^\left|{S}\mathrm{++}{T}\right|\right)=\left(0..^\left|{T}\right|+\left|{S}\right|\right)$
159 157 158 sseqtrrd ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\subseteq \left(0..^\left|{S}\mathrm{++}{T}\right|\right)$
160 159 sselda ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to {x}\in \left(0..^\left|{S}\mathrm{++}{T}\right|\right)$
161 1 160 81 syl2an2r ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to \mathrm{reverse}\left({S}\mathrm{++}{T}\right)\left({x}\right)=\left({S}\mathrm{++}{T}\right)\left(\left|{S}\mathrm{++}{T}\right|-1-{x}\right)$
162 18 ad2antlr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to \mathrm{reverse}\left({T}\right)\in \mathrm{Word}{A}$
163 19 ad2antrr ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to \mathrm{reverse}\left({S}\right)\in \mathrm{Word}{A}$
164 85 28 oveq12d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left(\left|\mathrm{reverse}\left({T}\right)\right|..^\left|\mathrm{reverse}\left({T}\right)\right|+\left|\mathrm{reverse}\left({S}\right)\right|\right)=\left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)$
165 164 eleq2d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \left({x}\in \left(\left|\mathrm{reverse}\left({T}\right)\right|..^\left|\mathrm{reverse}\left({T}\right)\right|+\left|\mathrm{reverse}\left({S}\right)\right|\right)↔{x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)$
166 165 biimpar ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to {x}\in \left(\left|\mathrm{reverse}\left({T}\right)\right|..^\left|\mathrm{reverse}\left({T}\right)\right|+\left|\mathrm{reverse}\left({S}\right)\right|\right)$
167 ccatval2 ${⊢}\left(\mathrm{reverse}\left({T}\right)\in \mathrm{Word}{A}\wedge \mathrm{reverse}\left({S}\right)\in \mathrm{Word}{A}\wedge {x}\in \left(\left|\mathrm{reverse}\left({T}\right)\right|..^\left|\mathrm{reverse}\left({T}\right)\right|+\left|\mathrm{reverse}\left({S}\right)\right|\right)\right)\to \left(\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\right)\left({x}\right)=\mathrm{reverse}\left({S}\right)\left({x}-\left|\mathrm{reverse}\left({T}\right)\right|\right)$
168 162 163 166 167 syl3anc ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to \left(\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\right)\left({x}\right)=\mathrm{reverse}\left({S}\right)\left({x}-\left|\mathrm{reverse}\left({T}\right)\right|\right)$
169 152 161 168 3eqtr4d ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\to \mathrm{reverse}\left({S}\mathrm{++}{T}\right)\left({x}\right)=\left(\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\right)\left({x}\right)$
170 91 169 jaodan ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge \left({x}\in \left(0..^\left|{T}\right|\right)\vee {x}\in \left(\left|{T}\right|..^\left|{T}\right|+\left|{S}\right|\right)\right)\right)\to \mathrm{reverse}\left({S}\mathrm{++}{T}\right)\left({x}\right)=\left(\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\right)\left({x}\right)$
171 37 170 syldan ${⊢}\left(\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\wedge {x}\in \left(0..^\left|{T}\right|+\left|{S}\right|\right)\right)\to \mathrm{reverse}\left({S}\mathrm{++}{T}\right)\left({x}\right)=\left(\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)\right)\left({x}\right)$
172 17 32 171 eqfnfvd ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{A}\right)\to \mathrm{reverse}\left({S}\mathrm{++}{T}\right)=\mathrm{reverse}\left({T}\right)\mathrm{++}\mathrm{reverse}\left({S}\right)$