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 ‘ 𝑊 ) ) = 𝑊 )