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 ⊢W∈WordA→reverse⁡W=W

Proof

Step Hyp Ref Expression
1 revval ⊢W∈WordA→reverse⁡W=x∈0..^W⟼W⁡W-1-x
2 1 fveq2d ⊢W∈WordA→reverse⁡W=x∈0..^W⟼W⁡W-1-x
3 wrdf ⊢W∈WordA→W:0..^W⟶A
4 3 adantr ⊢W∈WordA∧x∈0..^W→W:0..^W⟶A
5 simpr ⊢W∈WordA∧x∈0..^W→x∈0..^W
6 lencl ⊢W∈WordA→W∈ℕ0
7 6 adantr ⊢W∈WordA∧x∈0..^W→W∈ℕ0
8 nn0z ⊢W∈ℕ0→W∈ℤ
9 fzoval ⊢W∈ℤ→0..^W=0…W−1
10 7 8 9 3syl ⊢W∈WordA∧x∈0..^W→0..^W=0…W−1
11 5 10 eleqtrd ⊢W∈WordA∧x∈0..^W→x∈0…W−1
12 fznn0sub2 ⊢x∈0…W−1→W-1-x∈0…W−1
13 11 12 syl ⊢W∈WordA∧x∈0..^W→W-1-x∈0…W−1
14 13 10 eleqtrrd ⊢W∈WordA∧x∈0..^W→W-1-x∈0..^W
15 4 14 ffvelcdmd ⊢W∈WordA∧x∈0..^W→W⁡W-1-x∈A
16 15 fmpttd ⊢W∈WordA→x∈0..^W⟼W⁡W-1-x:0..^W⟶A
17 ffn ⊢x∈0..^W⟼W⁡W-1-x:0..^W⟶A→x∈0..^W⟼W⁡W-1-xFn0..^W
18 hashfn ⊢x∈0..^W⟼W⁡W-1-xFn0..^W→x∈0..^W⟼W⁡W-1-x=0..^W
19 16 17 18 3syl ⊢W∈WordA→x∈0..^W⟼W⁡W-1-x=0..^W
20 hashfzo0 ⊢W∈ℕ0→0..^W=W
21 6 20 syl ⊢W∈WordA→0..^W=W
22 2 19 21 3eqtrd ⊢W∈WordA→reverse⁡W=W