Metamath Proof Explorer

Theorem revrev

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

Ref Expression
Assertion revrev ⊢ W ∈ Word A → reverse ⁡ reverse ⁡ W = W

Proof

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