Metamath Proof Explorer

Theorem revrev

Description: Reversal is an involution on words. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Assertion revrev ⊢W∈WordA→reverse⁡reverse⁡W=W

Proof

Step Hyp Ref Expression
1 revcl ⊢W∈WordA→reverse⁡W∈WordA
2 revcl ⊢reverse⁡W∈WordA→reverse⁡reverse⁡W∈WordA
3 wrdf ⊢reverse⁡reverse⁡W∈WordA→reverse⁡reverse⁡W:0..^reverse⁡reverse⁡W⟶A
4 ffn ⊢reverse⁡reverse⁡W:0..^reverse⁡reverse⁡W⟶A→reverse⁡reverse⁡WFn0..^reverse⁡reverse⁡W
5 1 2 3 4 4syl ⊢W∈WordA→reverse⁡reverse⁡WFn0..^reverse⁡reverse⁡W
6 revlen ⊢reverse⁡W∈WordA→reverse⁡reverse⁡W=reverse⁡W
7 1 6 syl ⊢W∈WordA→reverse⁡reverse⁡W=reverse⁡W
8 revlen ⊢W∈WordA→reverse⁡W=W
9 7 8 eqtrd ⊢W∈WordA→reverse⁡reverse⁡W=W
10 9 oveq2d ⊢W∈WordA→0..^reverse⁡reverse⁡W=0..^W
11 10 fneq2d ⊢W∈WordA→reverse⁡reverse⁡WFn0..^reverse⁡reverse⁡W↔reverse⁡reverse⁡WFn0..^W
12 5 11 mpbid ⊢W∈WordA→reverse⁡reverse⁡WFn0..^W
13 wrdfn ⊢W∈WordA→WFn0..^W
14 simpr ⊢W∈WordA∧x∈0..^W→x∈0..^W
15 8 adantr ⊢W∈WordA∧x∈0..^W→reverse⁡W=W
16 15 oveq2d ⊢W∈WordA∧x∈0..^W→0..^reverse⁡W=0..^W
17 14 16 eleqtrrd ⊢W∈WordA∧x∈0..^W→x∈0..^reverse⁡W
18 revfv ⊢reverse⁡W∈WordA∧x∈0..^reverse⁡W→reverse⁡reverse⁡W⁡x=reverse⁡W⁡reverse⁡W-1-x
19 1 17 18 syl2an2r ⊢W∈WordA∧x∈0..^W→reverse⁡reverse⁡W⁡x=reverse⁡W⁡reverse⁡W-1-x
20 15 oveq1d ⊢W∈WordA∧x∈0..^W→reverse⁡W−1=W−1
21 20 fvoveq1d ⊢W∈WordA∧x∈0..^W→reverse⁡W⁡reverse⁡W-1-x=reverse⁡W⁡W-1-x
22 lencl ⊢W∈WordA→W∈ℕ0
23 22 nn0zd ⊢W∈WordA→W∈ℤ
24 fzoval ⊢W∈ℤ→0..^W=0…W−1
25 23 24 syl ⊢W∈WordA→0..^W=0…W−1
26 25 eleq2d ⊢W∈WordA→x∈0..^W↔x∈0…W−1
27 26 biimpa ⊢W∈WordA∧x∈0..^W→x∈0…W−1
28 fznn0sub2 ⊢x∈0…W−1→W-1-x∈0…W−1
29 27 28 syl ⊢W∈WordA∧x∈0..^W→W-1-x∈0…W−1
30 25 adantr ⊢W∈WordA∧x∈0..^W→0..^W=0…W−1
31 29 30 eleqtrrd ⊢W∈WordA∧x∈0..^W→W-1-x∈0..^W
32 revfv ⊢W∈WordA∧W-1-x∈0..^W→reverse⁡W⁡W-1-x=W⁡W-1-W-1-x
33 31 32 syldan ⊢W∈WordA∧x∈0..^W→reverse⁡W⁡W-1-x=W⁡W-1-W-1-x
34 peano2zm ⊢W∈ℤ→W−1∈ℤ
35 23 34 syl ⊢W∈WordA→W−1∈ℤ
36 35 zcnd ⊢W∈WordA→W−1∈ℂ
37 elfzoelz ⊢x∈0..^W→x∈ℤ
38 37 zcnd ⊢x∈0..^W→x∈ℂ
39 nncan ⊢W−1∈ℂ∧x∈ℂ→W-1-W-1-x=x
40 36 38 39 syl2an ⊢W∈WordA∧x∈0..^W→W-1-W-1-x=x
41 40 fveq2d ⊢W∈WordA∧x∈0..^W→W⁡W-1-W-1-x=W⁡x
42 33 41 eqtrd ⊢W∈WordA∧x∈0..^W→reverse⁡W⁡W-1-x=W⁡x
43 21 42 eqtrd ⊢W∈WordA∧x∈0..^W→reverse⁡W⁡reverse⁡W-1-x=W⁡x
44 19 43 eqtrd ⊢W∈WordA∧x∈0..^W→reverse⁡reverse⁡W⁡x=W⁡x
45 12 13 44 eqfnfvd ⊢W∈WordA→reverse⁡reverse⁡W=W