# Metamath Proof Explorer

## Theorem revco

Description: Mapping of words (i.e., a letterwise mapping) commutes with reversal. (Contributed by Stefan O'Rear, 27-Aug-2015)

Ref Expression
Assertion revco ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to {F}\circ \mathrm{reverse}\left({W}\right)=\mathrm{reverse}\left({F}\circ {W}\right)$

### Proof

Step Hyp Ref Expression
1 wrdfn ${⊢}{W}\in \mathrm{Word}{A}\to {W}Fn\left(0..^\left|{W}\right|\right)$
2 1 ad2antrr ${⊢}\left(\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\wedge {x}\in \left(0..^\left|{W}\right|\right)\right)\to {W}Fn\left(0..^\left|{W}\right|\right)$
3 lencl ${⊢}{W}\in \mathrm{Word}{A}\to \left|{W}\right|\in {ℕ}_{0}$
4 3 nn0zd ${⊢}{W}\in \mathrm{Word}{A}\to \left|{W}\right|\in ℤ$
5 fzoval ${⊢}\left|{W}\right|\in ℤ\to \left(0..^\left|{W}\right|\right)=\left(0\dots \left|{W}\right|-1\right)$
6 4 5 syl ${⊢}{W}\in \mathrm{Word}{A}\to \left(0..^\left|{W}\right|\right)=\left(0\dots \left|{W}\right|-1\right)$
7 6 adantr ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to \left(0..^\left|{W}\right|\right)=\left(0\dots \left|{W}\right|-1\right)$
8 7 eleq2d ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to \left({x}\in \left(0..^\left|{W}\right|\right)↔{x}\in \left(0\dots \left|{W}\right|-1\right)\right)$
9 8 biimpa ${⊢}\left(\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\wedge {x}\in \left(0..^\left|{W}\right|\right)\right)\to {x}\in \left(0\dots \left|{W}\right|-1\right)$
10 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)$
11 9 10 syl ${⊢}\left(\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\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)$
12 7 adantr ${⊢}\left(\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\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)$
13 11 12 eleqtrrd ${⊢}\left(\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\wedge {x}\in \left(0..^\left|{W}\right|\right)\right)\to \left|{W}\right|-1-{x}\in \left(0..^\left|{W}\right|\right)$
14 fvco2 ${⊢}\left({W}Fn\left(0..^\left|{W}\right|\right)\wedge \left|{W}\right|-1-{x}\in \left(0..^\left|{W}\right|\right)\right)\to \left({F}\circ {W}\right)\left(\left|{W}\right|-1-{x}\right)={F}\left({W}\left(\left|{W}\right|-1-{x}\right)\right)$
15 2 13 14 syl2anc ${⊢}\left(\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\wedge {x}\in \left(0..^\left|{W}\right|\right)\right)\to \left({F}\circ {W}\right)\left(\left|{W}\right|-1-{x}\right)={F}\left({W}\left(\left|{W}\right|-1-{x}\right)\right)$
16 lenco ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to \left|{F}\circ {W}\right|=\left|{W}\right|$
17 16 oveq1d ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to \left|{F}\circ {W}\right|-1=\left|{W}\right|-1$
18 17 oveq1d ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to \left|{F}\circ {W}\right|-1-{x}=\left|{W}\right|-1-{x}$
19 18 adantr ${⊢}\left(\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\wedge {x}\in \left(0..^\left|{W}\right|\right)\right)\to \left|{F}\circ {W}\right|-1-{x}=\left|{W}\right|-1-{x}$
20 19 fveq2d ${⊢}\left(\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\wedge {x}\in \left(0..^\left|{W}\right|\right)\right)\to \left({F}\circ {W}\right)\left(\left|{F}\circ {W}\right|-1-{x}\right)=\left({F}\circ {W}\right)\left(\left|{W}\right|-1-{x}\right)$
21 revfv ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {x}\in \left(0..^\left|{W}\right|\right)\right)\to \mathrm{reverse}\left({W}\right)\left({x}\right)={W}\left(\left|{W}\right|-1-{x}\right)$
22 21 adantlr ${⊢}\left(\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\wedge {x}\in \left(0..^\left|{W}\right|\right)\right)\to \mathrm{reverse}\left({W}\right)\left({x}\right)={W}\left(\left|{W}\right|-1-{x}\right)$
23 22 fveq2d ${⊢}\left(\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\wedge {x}\in \left(0..^\left|{W}\right|\right)\right)\to {F}\left(\mathrm{reverse}\left({W}\right)\left({x}\right)\right)={F}\left({W}\left(\left|{W}\right|-1-{x}\right)\right)$
24 15 20 23 3eqtr4d ${⊢}\left(\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\wedge {x}\in \left(0..^\left|{W}\right|\right)\right)\to \left({F}\circ {W}\right)\left(\left|{F}\circ {W}\right|-1-{x}\right)={F}\left(\mathrm{reverse}\left({W}\right)\left({x}\right)\right)$
25 24 mpteq2dva ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to \left({x}\in \left(0..^\left|{W}\right|\right)⟼\left({F}\circ {W}\right)\left(\left|{F}\circ {W}\right|-1-{x}\right)\right)=\left({x}\in \left(0..^\left|{W}\right|\right)⟼{F}\left(\mathrm{reverse}\left({W}\right)\left({x}\right)\right)\right)$
26 16 oveq2d ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to \left(0..^\left|{F}\circ {W}\right|\right)=\left(0..^\left|{W}\right|\right)$
27 26 mpteq1d ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to \left({x}\in \left(0..^\left|{F}\circ {W}\right|\right)⟼\left({F}\circ {W}\right)\left(\left|{F}\circ {W}\right|-1-{x}\right)\right)=\left({x}\in \left(0..^\left|{W}\right|\right)⟼\left({F}\circ {W}\right)\left(\left|{F}\circ {W}\right|-1-{x}\right)\right)$
28 revlen ${⊢}{W}\in \mathrm{Word}{A}\to \left|\mathrm{reverse}\left({W}\right)\right|=\left|{W}\right|$
29 28 adantr ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to \left|\mathrm{reverse}\left({W}\right)\right|=\left|{W}\right|$
30 29 oveq2d ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to \left(0..^\left|\mathrm{reverse}\left({W}\right)\right|\right)=\left(0..^\left|{W}\right|\right)$
31 30 mpteq1d ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to \left({x}\in \left(0..^\left|\mathrm{reverse}\left({W}\right)\right|\right)⟼{F}\left(\mathrm{reverse}\left({W}\right)\left({x}\right)\right)\right)=\left({x}\in \left(0..^\left|{W}\right|\right)⟼{F}\left(\mathrm{reverse}\left({W}\right)\left({x}\right)\right)\right)$
32 25 27 31 3eqtr4rd ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to \left({x}\in \left(0..^\left|\mathrm{reverse}\left({W}\right)\right|\right)⟼{F}\left(\mathrm{reverse}\left({W}\right)\left({x}\right)\right)\right)=\left({x}\in \left(0..^\left|{F}\circ {W}\right|\right)⟼\left({F}\circ {W}\right)\left(\left|{F}\circ {W}\right|-1-{x}\right)\right)$
33 simpr ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to {F}:{A}⟶{B}$
34 revcl ${⊢}{W}\in \mathrm{Word}{A}\to \mathrm{reverse}\left({W}\right)\in \mathrm{Word}{A}$
35 wrdf ${⊢}\mathrm{reverse}\left({W}\right)\in \mathrm{Word}{A}\to \mathrm{reverse}\left({W}\right):\left(0..^\left|\mathrm{reverse}\left({W}\right)\right|\right)⟶{A}$
36 34 35 syl ${⊢}{W}\in \mathrm{Word}{A}\to \mathrm{reverse}\left({W}\right):\left(0..^\left|\mathrm{reverse}\left({W}\right)\right|\right)⟶{A}$
37 36 adantr ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to \mathrm{reverse}\left({W}\right):\left(0..^\left|\mathrm{reverse}\left({W}\right)\right|\right)⟶{A}$
38 fcompt ${⊢}\left({F}:{A}⟶{B}\wedge \mathrm{reverse}\left({W}\right):\left(0..^\left|\mathrm{reverse}\left({W}\right)\right|\right)⟶{A}\right)\to {F}\circ \mathrm{reverse}\left({W}\right)=\left({x}\in \left(0..^\left|\mathrm{reverse}\left({W}\right)\right|\right)⟼{F}\left(\mathrm{reverse}\left({W}\right)\left({x}\right)\right)\right)$
39 33 37 38 syl2anc ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to {F}\circ \mathrm{reverse}\left({W}\right)=\left({x}\in \left(0..^\left|\mathrm{reverse}\left({W}\right)\right|\right)⟼{F}\left(\mathrm{reverse}\left({W}\right)\left({x}\right)\right)\right)$
40 ffun ${⊢}{F}:{A}⟶{B}\to \mathrm{Fun}{F}$
41 simpl ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to {W}\in \mathrm{Word}{A}$
42 cofunexg ${⊢}\left(\mathrm{Fun}{F}\wedge {W}\in \mathrm{Word}{A}\right)\to {F}\circ {W}\in \mathrm{V}$
43 40 41 42 syl2an2 ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to {F}\circ {W}\in \mathrm{V}$
44 revval ${⊢}{F}\circ {W}\in \mathrm{V}\to \mathrm{reverse}\left({F}\circ {W}\right)=\left({x}\in \left(0..^\left|{F}\circ {W}\right|\right)⟼\left({F}\circ {W}\right)\left(\left|{F}\circ {W}\right|-1-{x}\right)\right)$
45 43 44 syl ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to \mathrm{reverse}\left({F}\circ {W}\right)=\left({x}\in \left(0..^\left|{F}\circ {W}\right|\right)⟼\left({F}\circ {W}\right)\left(\left|{F}\circ {W}\right|-1-{x}\right)\right)$
46 32 39 45 3eqtr4d ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to {F}\circ \mathrm{reverse}\left({W}\right)=\mathrm{reverse}\left({F}\circ {W}\right)$