Metamath Proof Explorer

Theorem revcl

Description: The reverse of a word is a word. (Contributed by Stefan O'Rear, 26-Aug-2015)

Ref Expression
Assertion revcl ⊢ W ∈ Word A → reverse ⁡ W ∈ Word A

Proof

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