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

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 ( 𝑊 ∈ Word 𝐴 → ( reverse ‘ 𝑊 ) ∈ Word 𝐴 )

Proof

Step Hyp Ref Expression
1 revval ⊢ ( 𝑊 ∈ Word 𝐴 → ( reverse ‘ 𝑊 ) = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) )
2 wrdf ⊢ ( 𝑊 ∈ Word 𝐴 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )
3 2 adantr ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )
4 simpr ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
5 lencl ⊢ ( 𝑊 ∈ Word 𝐴 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
6 5 adantr ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
7 6 nn0zd ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ℤ )
8 fzoval ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℤ → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
9 7 8 syl ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
10 4 9 eleqtrd ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑥 ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
11 fznn0sub2 ⊢ ( 𝑥 ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
12 10 11 syl ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
13 12 9 eleqtrrd ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
14 3 13 ffvelcdmd ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ∈ 𝐴 )
15 14 fmpttd ⊢ ( 𝑊 ∈ Word 𝐴 → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )
16 iswrdi ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) ∈ Word 𝐴 )
17 15 16 syl ⊢ ( 𝑊 ∈ Word 𝐴 → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) ∈ Word 𝐴 )
18 1 17 eqeltrd ⊢ ( 𝑊 ∈ Word 𝐴 → ( reverse ‘ 𝑊 ) ∈ Word 𝐴 )