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

Metamath Proof Explorer

Theorem revccat

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

Ref Expression
Assertion revccat ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ) → ( reverse ‘ ( 𝑆 ++ 𝑇 ) ) = ( ( reverse ‘ 𝑇 ) ++ ( reverse ‘ 𝑆 ) ) )

Proof

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