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}\in \mathrm{Word}{A}\to \mathrm{reverse}\left({W}\right)\in \mathrm{Word}{A}$

Proof

Step Hyp Ref Expression
1 revval ${⊢}{W}\in \mathrm{Word}{A}\to \mathrm{reverse}\left({W}\right)=\left({x}\in \left(0..^\left|{W}\right|\right)⟼{W}\left(\left|{W}\right|-1-{x}\right)\right)$
2 wrdf ${⊢}{W}\in \mathrm{Word}{A}\to {W}:\left(0..^\left|{W}\right|\right)⟶{A}$
3 2 adantr ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {x}\in \left(0..^\left|{W}\right|\right)\right)\to {W}:\left(0..^\left|{W}\right|\right)⟶{A}$
4 simpr ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {x}\in \left(0..^\left|{W}\right|\right)\right)\to {x}\in \left(0..^\left|{W}\right|\right)$
5 lencl ${⊢}{W}\in \mathrm{Word}{A}\to \left|{W}\right|\in {ℕ}_{0}$
6 5 adantr ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {x}\in \left(0..^\left|{W}\right|\right)\right)\to \left|{W}\right|\in {ℕ}_{0}$
7 6 nn0zd ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {x}\in \left(0..^\left|{W}\right|\right)\right)\to \left|{W}\right|\in ℤ$
8 fzoval ${⊢}\left|{W}\right|\in ℤ\to \left(0..^\left|{W}\right|\right)=\left(0\dots \left|{W}\right|-1\right)$
9 7 8 syl ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {x}\in \left(0..^\left|{W}\right|\right)\right)\to \left(0..^\left|{W}\right|\right)=\left(0\dots \left|{W}\right|-1\right)$
10 4 9 eleqtrd ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {x}\in \left(0..^\left|{W}\right|\right)\right)\to {x}\in \left(0\dots \left|{W}\right|-1\right)$
11 fznn0sub2 ${⊢}{x}\in \left(0\dots \left|{W}\right|-1\right)\to \left|{W}\right|-1-{x}\in \left(0\dots \left|{W}\right|-1\right)$
12 10 11 syl ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {x}\in \left(0..^\left|{W}\right|\right)\right)\to \left|{W}\right|-1-{x}\in \left(0\dots \left|{W}\right|-1\right)$
13 12 9 eleqtrrd ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {x}\in \left(0..^\left|{W}\right|\right)\right)\to \left|{W}\right|-1-{x}\in \left(0..^\left|{W}\right|\right)$
14 3 13 ffvelrnd ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {x}\in \left(0..^\left|{W}\right|\right)\right)\to {W}\left(\left|{W}\right|-1-{x}\right)\in {A}$
15 14 fmpttd ${⊢}{W}\in \mathrm{Word}{A}\to \left({x}\in \left(0..^\left|{W}\right|\right)⟼{W}\left(\left|{W}\right|-1-{x}\right)\right):\left(0..^\left|{W}\right|\right)⟶{A}$
16 iswrdi ${⊢}\left({x}\in \left(0..^\left|{W}\right|\right)⟼{W}\left(\left|{W}\right|-1-{x}\right)\right):\left(0..^\left|{W}\right|\right)⟶{A}\to \left({x}\in \left(0..^\left|{W}\right|\right)⟼{W}\left(\left|{W}\right|-1-{x}\right)\right)\in \mathrm{Word}{A}$
17 15 16 syl ${⊢}{W}\in \mathrm{Word}{A}\to \left({x}\in \left(0..^\left|{W}\right|\right)⟼{W}\left(\left|{W}\right|-1-{x}\right)\right)\in \mathrm{Word}{A}$
18 1 17 eqeltrd ${⊢}{W}\in \mathrm{Word}{A}\to \mathrm{reverse}\left({W}\right)\in \mathrm{Word}{A}$