Description: Define an operation which reverses the order of symbols in a word. This operation is also known as "word reversal" and "word mirroring". (Contributed by Stefan O'Rear, 26-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | df-reverse | |- reverse = ( s e. _V |-> ( x e. ( 0 ..^ ( # ` s ) ) |-> ( s ` ( ( ( # ` s ) - 1 ) - x ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | creverse | |- reverse |
|
1 | vs | |- s |
|
2 | cvv | |- _V |
|
3 | vx | |- x |
|
4 | cc0 | |- 0 |
|
5 | cfzo | |- ..^ |
|
6 | chash | |- # |
|
7 | 1 | cv | |- s |
8 | 7 6 | cfv | |- ( # ` s ) |
9 | 4 8 5 | co | |- ( 0 ..^ ( # ` s ) ) |
10 | cmin | |- - |
|
11 | c1 | |- 1 |
|
12 | 8 11 10 | co | |- ( ( # ` s ) - 1 ) |
13 | 3 | cv | |- x |
14 | 12 13 10 | co | |- ( ( ( # ` s ) - 1 ) - x ) |
15 | 14 7 | cfv | |- ( s ` ( ( ( # ` s ) - 1 ) - x ) ) |
16 | 3 9 15 | cmpt | |- ( x e. ( 0 ..^ ( # ` s ) ) |-> ( s ` ( ( ( # ` s ) - 1 ) - x ) ) ) |
17 | 1 2 16 | cmpt | |- ( s e. _V |-> ( x e. ( 0 ..^ ( # ` s ) ) |-> ( s ` ( ( ( # ` s ) - 1 ) - x ) ) ) ) |
18 | 0 17 | wceq | |- reverse = ( s e. _V |-> ( x e. ( 0 ..^ ( # ` s ) ) |-> ( s ` ( ( ( # ` s ) - 1 ) - x ) ) ) ) |