This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( reverse ‘ 𝑊 ) ) = ( reverse ‘ ( 𝐹 ∘ 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 wrdfn ⊢ ( 𝑊 ∈ Word 𝐴 → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
2 1 ad2antrr ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
3 lencl ⊢ ( 𝑊 ∈ Word 𝐴 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
4 3 nn0zd ⊢ ( 𝑊 ∈ Word 𝐴 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
5 fzoval ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℤ → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
6 4 5 syl ⊢ ( 𝑊 ∈ Word 𝐴 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
7 6 adantr ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
8 7 eleq2d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ 𝑥 ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) )
9 8 biimpa ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑥 ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
10 fznn0sub2 ⊢ ( 𝑥 ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
11 9 10 syl ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
12 7 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
13 11 12 eleqtrrd ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
14 fvco2 ⊢ ( ( 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹 ∘ 𝑊 ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) = ( 𝐹 ‘ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) )
15 2 13 14 syl2anc ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹 ∘ 𝑊 ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) = ( 𝐹 ‘ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) )
16 lenco ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) = ( ♯ ‘ 𝑊 ) )
17 16 oveq1d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) − 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
18 17 oveq1d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ( ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) − 1 ) − 𝑥 ) = ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) )
19 18 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) − 1 ) − 𝑥 ) = ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) )
20 19 fveq2d ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹 ∘ 𝑊 ) ‘ ( ( ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) − 1 ) − 𝑥 ) ) = ( ( 𝐹 ∘ 𝑊 ) ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) )
21 revfv ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( reverse ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) )
22 21 adantlr ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( reverse ‘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) )
23 22 fveq2d ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐹 ‘ ( ( reverse ‘ 𝑊 ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) )
24 15 20 23 3eqtr4d ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹 ∘ 𝑊 ) ‘ ( ( ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) − 1 ) − 𝑥 ) ) = ( 𝐹 ‘ ( ( reverse ‘ 𝑊 ) ‘ 𝑥 ) ) )
25 24 mpteq2dva ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( ( 𝐹 ∘ 𝑊 ) ‘ ( ( ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) − 1 ) − 𝑥 ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝐹 ‘ ( ( reverse ‘ 𝑊 ) ‘ 𝑥 ) ) ) )
26 16 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 0 ..^ ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
27 26 mpteq1d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ↦ ( ( 𝐹 ∘ 𝑊 ) ‘ ( ( ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) − 1 ) − 𝑥 ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( ( 𝐹 ∘ 𝑊 ) ‘ ( ( ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) − 1 ) − 𝑥 ) ) ) )
28 revlen ⊢ ( 𝑊 ∈ Word 𝐴 → ( ♯ ‘ ( reverse ‘ 𝑊 ) ) = ( ♯ ‘ 𝑊 ) )
29 28 adantr ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ♯ ‘ ( reverse ‘ 𝑊 ) ) = ( ♯ ‘ 𝑊 ) )
30 29 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 0 ..^ ( ♯ ‘ ( reverse ‘ 𝑊 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
31 30 mpteq1d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( reverse ‘ 𝑊 ) ) ) ↦ ( 𝐹 ‘ ( ( reverse ‘ 𝑊 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝐹 ‘ ( ( reverse ‘ 𝑊 ) ‘ 𝑥 ) ) ) )
32 25 27 31 3eqtr4rd ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( reverse ‘ 𝑊 ) ) ) ↦ ( 𝐹 ‘ ( ( reverse ‘ 𝑊 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ↦ ( ( 𝐹 ∘ 𝑊 ) ‘ ( ( ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) − 1 ) − 𝑥 ) ) ) )
33 simpr ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
34 revcl ⊢ ( 𝑊 ∈ Word 𝐴 → ( reverse ‘ 𝑊 ) ∈ Word 𝐴 )
35 wrdf ⊢ ( ( reverse ‘ 𝑊 ) ∈ Word 𝐴 → ( reverse ‘ 𝑊 ) : ( 0 ..^ ( ♯ ‘ ( reverse ‘ 𝑊 ) ) ) ⟶ 𝐴 )
36 34 35 syl ⊢ ( 𝑊 ∈ Word 𝐴 → ( reverse ‘ 𝑊 ) : ( 0 ..^ ( ♯ ‘ ( reverse ‘ 𝑊 ) ) ) ⟶ 𝐴 )
37 36 adantr ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( reverse ‘ 𝑊 ) : ( 0 ..^ ( ♯ ‘ ( reverse ‘ 𝑊 ) ) ) ⟶ 𝐴 )
38 fcompt ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( reverse ‘ 𝑊 ) : ( 0 ..^ ( ♯ ‘ ( reverse ‘ 𝑊 ) ) ) ⟶ 𝐴 ) → ( 𝐹 ∘ ( reverse ‘ 𝑊 ) ) = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( reverse ‘ 𝑊 ) ) ) ↦ ( 𝐹 ‘ ( ( reverse ‘ 𝑊 ) ‘ 𝑥 ) ) ) )
39 33 37 38 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( reverse ‘ 𝑊 ) ) = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( reverse ‘ 𝑊 ) ) ) ↦ ( 𝐹 ‘ ( ( reverse ‘ 𝑊 ) ‘ 𝑥 ) ) ) )
40 ffun ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → Fun 𝐹 )
41 simpl ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝑊 ∈ Word 𝐴 )
42 cofunexg ⊢ ( ( Fun 𝐹 ∧ 𝑊 ∈ Word 𝐴 ) → ( 𝐹 ∘ 𝑊 ) ∈ V )
43 40 41 42 syl2an2 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝑊 ) ∈ V )
44 revval ⊢ ( ( 𝐹 ∘ 𝑊 ) ∈ V → ( reverse ‘ ( 𝐹 ∘ 𝑊 ) ) = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ↦ ( ( 𝐹 ∘ 𝑊 ) ‘ ( ( ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) − 1 ) − 𝑥 ) ) ) )
45 43 44 syl ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( reverse ‘ ( 𝐹 ∘ 𝑊 ) ) = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ↦ ( ( 𝐹 ∘ 𝑊 ) ‘ ( ( ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) − 1 ) − 𝑥 ) ) ) )
46 32 39 45 3eqtr4d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( reverse ‘ 𝑊 ) ) = ( reverse ‘ ( 𝐹 ∘ 𝑊 ) ) )