Metamath Proof Explorer

Theorem revccat

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

Ref Expression
Assertion revccat 
|- ( ( S e. Word A /\ T e. Word A ) -> ( reverse ` ( S ++ T ) ) = ( ( reverse ` T ) ++ ( reverse ` S ) ) )

Proof

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