Metamath Proof Explorer

Theorem revlen

Description: The reverse of a word has the same length as the original. (Contributed by Stefan O'Rear, 26-Aug-2015)

Ref Expression
Assertion revlen ( 𝑊 ∈ Word 𝐴 → ( ♯ ‘ ( reverse ‘ 𝑊 ) ) = ( ♯ ‘ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 revval ⊢ ( 𝑊 ∈ Word 𝐴 → ( reverse ‘ 𝑊 ) = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) )
2 1 fveq2d ⊢ ( 𝑊 ∈ Word 𝐴 → ( ♯ ‘ ( reverse ‘ 𝑊 ) ) = ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) ) )
3 wrdf ⊢ ( 𝑊 ∈ Word 𝐴 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )
4 3 adantr ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )
5 simpr ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
6 lencl ⊢ ( 𝑊 ∈ Word 𝐴 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
7 6 adantr ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
8 nn0z ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
9 fzoval ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℤ → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
10 7 8 9 3syl ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
11 5 10 eleqtrd ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑥 ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
12 fznn0sub2 ⊢ ( 𝑥 ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
13 11 12 syl ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
14 13 10 eleqtrrd ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
15 4 14 ffvelrnd ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ∈ 𝐴 )
16 15 fmpttd ⊢ ( 𝑊 ∈ Word 𝐴 → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )
17 ffn ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
18 hashfn ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
19 16 17 18 3syl ⊢ ( 𝑊 ∈ Word 𝐴 → ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
20 hashfzo0 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) = ( ♯ ‘ 𝑊 ) )
21 6 20 syl ⊢ ( 𝑊 ∈ Word 𝐴 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) = ( ♯ ‘ 𝑊 ) )
22 2 19 21 3eqtrd ⊢ ( 𝑊 ∈ Word 𝐴 → ( ♯ ‘ ( reverse ‘ 𝑊 ) ) = ( ♯ ‘ 𝑊 ) )