Metamath Proof Explorer

Theorem revlen

Description: The reverse of a word has the same length as the original. (Contributed by Stefan O'Rear, 26-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 revval ⊢ W ∈ Word A → reverse ⁡ W = x ∈ 0 ..^ W ⟼ W ⁡ W - 1 - x
2 1 fveq2d ⊢ W ∈ Word A → reverse ⁡ W = x ∈ 0 ..^ W ⟼ W ⁡ W - 1 - x
3 wrdf ⊢ W ∈ Word A → W : 0 ..^ W ⟶ A
4 3 adantr ⊢ W ∈ Word A ∧ x ∈ 0 ..^ W → W : 0 ..^ W ⟶ A
5 simpr ⊢ W ∈ Word A ∧ x ∈ 0 ..^ W → x ∈ 0 ..^ W
6 lencl ⊢ W ∈ Word A → W ∈ ℕ 0
7 6 adantr ⊢ W ∈ Word A ∧ x ∈ 0 ..^ W → W ∈ ℕ 0
8 nn0z ⊢ W ∈ ℕ 0 → W ∈ ℤ
9 fzoval ⊢ W ∈ ℤ → 0 ..^ W = 0 … W − 1
10 7 8 9 3syl ⊢ W ∈ Word A ∧ x ∈ 0 ..^ W → 0 ..^ W = 0 … W − 1
11 5 10 eleqtrd ⊢ W ∈ Word A ∧ x ∈ 0 ..^ W → x ∈ 0 … W − 1
12 fznn0sub2 ⊢ x ∈ 0 … W − 1 → W - 1 - x ∈ 0 … W − 1
13 11 12 syl ⊢ W ∈ Word A ∧ x ∈ 0 ..^ W → W - 1 - x ∈ 0 … W − 1
14 13 10 eleqtrrd ⊢ W ∈ Word A ∧ x ∈ 0 ..^ W → W - 1 - x ∈ 0 ..^ W
15 4 14 ffvelrnd ⊢ W ∈ Word A ∧ x ∈ 0 ..^ W → W ⁡ W - 1 - x ∈ A
16 15 fmpttd ⊢ W ∈ Word A → x ∈ 0 ..^ W ⟼ W ⁡ W - 1 - x : 0 ..^ W ⟶ A
17 ffn ⊢ x ∈ 0 ..^ W ⟼ W ⁡ W - 1 - x : 0 ..^ W ⟶ A → x ∈ 0 ..^ W ⟼ W ⁡ W - 1 - x Fn 0 ..^ W
18 hashfn ⊢ x ∈ 0 ..^ W ⟼ W ⁡ W - 1 - x Fn 0 ..^ W → x ∈ 0 ..^ W ⟼ W ⁡ W - 1 - x = 0 ..^ W
19 16 17 18 3syl ⊢ W ∈ Word A → x ∈ 0 ..^ W ⟼ W ⁡ W - 1 - x = 0 ..^ W
20 hashfzo0 ⊢ W ∈ ℕ 0 → 0 ..^ W = W
21 6 20 syl ⊢ W ∈ Word A → 0 ..^ W = W
22 2 19 21 3eqtrd ⊢ W ∈ Word A → reverse ⁡ W = W