Metamath Proof Explorer


Theorem revrev

Description: Reversal is an involution on words. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Assertion revrev ( 𝑊 ∈ Word 𝐴 → ( reverse ‘ ( reverse ‘ 𝑊 ) ) = 𝑊 )

Proof

Step Hyp Ref Expression
1 revcl ( 𝑊 ∈ Word 𝐴 → ( reverse ‘ 𝑊 ) ∈ Word 𝐴 )
2 revcl ( ( reverse ‘ 𝑊 ) ∈ Word 𝐴 → ( reverse ‘ ( reverse ‘ 𝑊 ) ) ∈ Word 𝐴 )
3 wrdf ( ( reverse ‘ ( reverse ‘ 𝑊 ) ) ∈ Word 𝐴 → ( reverse ‘ ( reverse ‘ 𝑊 ) ) : ( 0 ..^ ( ♯ ‘ ( reverse ‘ ( reverse ‘ 𝑊 ) ) ) ) ⟶ 𝐴 )
4 ffn ( ( reverse ‘ ( reverse ‘ 𝑊 ) ) : ( 0 ..^ ( ♯ ‘ ( reverse ‘ ( reverse ‘ 𝑊 ) ) ) ) ⟶ 𝐴 → ( reverse ‘ ( reverse ‘ 𝑊 ) ) Fn ( 0 ..^ ( ♯ ‘ ( reverse ‘ ( reverse ‘ 𝑊 ) ) ) ) )
5 1 2 3 4 4syl ( 𝑊 ∈ Word 𝐴 → ( reverse ‘ ( reverse ‘ 𝑊 ) ) Fn ( 0 ..^ ( ♯ ‘ ( reverse ‘ ( reverse ‘ 𝑊 ) ) ) ) )
6 revlen ( ( reverse ‘ 𝑊 ) ∈ Word 𝐴 → ( ♯ ‘ ( reverse ‘ ( reverse ‘ 𝑊 ) ) ) = ( ♯ ‘ ( reverse ‘ 𝑊 ) ) )
7 1 6 syl ( 𝑊 ∈ Word 𝐴 → ( ♯ ‘ ( reverse ‘ ( reverse ‘ 𝑊 ) ) ) = ( ♯ ‘ ( reverse ‘ 𝑊 ) ) )
8 revlen ( 𝑊 ∈ Word 𝐴 → ( ♯ ‘ ( reverse ‘ 𝑊 ) ) = ( ♯ ‘ 𝑊 ) )
9 7 8 eqtrd ( 𝑊 ∈ Word 𝐴 → ( ♯ ‘ ( reverse ‘ ( reverse ‘ 𝑊 ) ) ) = ( ♯ ‘ 𝑊 ) )
10 9 oveq2d ( 𝑊 ∈ Word 𝐴 → ( 0 ..^ ( ♯ ‘ ( reverse ‘ ( reverse ‘ 𝑊 ) ) ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
11 10 fneq2d ( 𝑊 ∈ Word 𝐴 → ( ( reverse ‘ ( reverse ‘ 𝑊 ) ) Fn ( 0 ..^ ( ♯ ‘ ( reverse ‘ ( reverse ‘ 𝑊 ) ) ) ) ↔ ( reverse ‘ ( reverse ‘ 𝑊 ) ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
12 5 11 mpbid ( 𝑊 ∈ Word 𝐴 → ( reverse ‘ ( reverse ‘ 𝑊 ) ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
13 wrdfn ( 𝑊 ∈ Word 𝐴𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
14 simpr ( ( 𝑊 ∈ Word 𝐴𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
15 8 adantr ( ( 𝑊 ∈ Word 𝐴𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( reverse ‘ 𝑊 ) ) = ( ♯ ‘ 𝑊 ) )
16 15 oveq2d ( ( 𝑊 ∈ Word 𝐴𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 0 ..^ ( ♯ ‘ ( reverse ‘ 𝑊 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
17 14 16 eleqtrrd ( ( 𝑊 ∈ Word 𝐴𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( reverse ‘ 𝑊 ) ) ) )
18 revfv ( ( ( reverse ‘ 𝑊 ) ∈ Word 𝐴𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( reverse ‘ 𝑊 ) ) ) ) → ( ( reverse ‘ ( reverse ‘ 𝑊 ) ) ‘ 𝑥 ) = ( ( reverse ‘ 𝑊 ) ‘ ( ( ( ♯ ‘ ( reverse ‘ 𝑊 ) ) − 1 ) − 𝑥 ) ) )
19 1 17 18 syl2an2r ( ( 𝑊 ∈ Word 𝐴𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( reverse ‘ ( reverse ‘ 𝑊 ) ) ‘ 𝑥 ) = ( ( reverse ‘ 𝑊 ) ‘ ( ( ( ♯ ‘ ( reverse ‘ 𝑊 ) ) − 1 ) − 𝑥 ) ) )
20 15 oveq1d ( ( 𝑊 ∈ Word 𝐴𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ ( reverse ‘ 𝑊 ) ) − 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
21 20 fvoveq1d ( ( 𝑊 ∈ Word 𝐴𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( reverse ‘ 𝑊 ) ‘ ( ( ( ♯ ‘ ( reverse ‘ 𝑊 ) ) − 1 ) − 𝑥 ) ) = ( ( reverse ‘ 𝑊 ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) )
22 lencl ( 𝑊 ∈ Word 𝐴 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
23 22 nn0zd ( 𝑊 ∈ Word 𝐴 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
24 fzoval ( ( ♯ ‘ 𝑊 ) ∈ ℤ → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
25 23 24 syl ( 𝑊 ∈ Word 𝐴 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
26 25 eleq2d ( 𝑊 ∈ Word 𝐴 → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 𝑥 ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) )
27 26 biimpa ( ( 𝑊 ∈ Word 𝐴𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑥 ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
28 fznn0sub2 ( 𝑥 ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
29 27 28 syl ( ( 𝑊 ∈ Word 𝐴𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
30 25 adantr ( ( 𝑊 ∈ Word 𝐴𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
31 29 30 eleqtrrd ( ( 𝑊 ∈ Word 𝐴𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
32 revfv ( ( 𝑊 ∈ Word 𝐴 ∧ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( reverse ‘ 𝑊 ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) = ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) )
33 31 32 syldan ( ( 𝑊 ∈ Word 𝐴𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( reverse ‘ 𝑊 ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) = ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) )
34 peano2zm ( ( ♯ ‘ 𝑊 ) ∈ ℤ → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℤ )
35 23 34 syl ( 𝑊 ∈ Word 𝐴 → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℤ )
36 35 zcnd ( 𝑊 ∈ Word 𝐴 → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℂ )
37 elfzoelz ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝑥 ∈ ℤ )
38 37 zcnd ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝑥 ∈ ℂ )
39 nncan ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) = 𝑥 )
40 36 38 39 syl2an ( ( 𝑊 ∈ Word 𝐴𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) = 𝑥 )
41 40 fveq2d ( ( 𝑊 ∈ Word 𝐴𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) = ( 𝑊𝑥 ) )
42 33 41 eqtrd ( ( 𝑊 ∈ Word 𝐴𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( reverse ‘ 𝑊 ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) = ( 𝑊𝑥 ) )
43 21 42 eqtrd ( ( 𝑊 ∈ Word 𝐴𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( reverse ‘ 𝑊 ) ‘ ( ( ( ♯ ‘ ( reverse ‘ 𝑊 ) ) − 1 ) − 𝑥 ) ) = ( 𝑊𝑥 ) )
44 19 43 eqtrd ( ( 𝑊 ∈ Word 𝐴𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( reverse ‘ ( reverse ‘ 𝑊 ) ) ‘ 𝑥 ) = ( 𝑊𝑥 ) )
45 12 13 44 eqfnfvd ( 𝑊 ∈ Word 𝐴 → ( reverse ‘ ( reverse ‘ 𝑊 ) ) = 𝑊 )