Step | Hyp | Ref
| Expression |
1 | | revval 14655 |
. . 3
β’ (π β Word π΄ β (reverseβπ) = (π₯ β (0..^(β―βπ)) β¦ (πβ(((β―βπ) β 1) β π₯)))) |
2 | 1 | fveq2d 6851 |
. 2
β’ (π β Word π΄ β (β―β(reverseβπ)) = (β―β(π₯ β
(0..^(β―βπ))
β¦ (πβ(((β―βπ) β 1) β π₯))))) |
3 | | wrdf 14414 |
. . . . . 6
β’ (π β Word π΄ β π:(0..^(β―βπ))βΆπ΄) |
4 | 3 | adantr 482 |
. . . . 5
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β π:(0..^(β―βπ))βΆπ΄) |
5 | | simpr 486 |
. . . . . . . 8
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β π₯ β (0..^(β―βπ))) |
6 | | lencl 14428 |
. . . . . . . . . 10
β’ (π β Word π΄ β (β―βπ) β
β0) |
7 | 6 | adantr 482 |
. . . . . . . . 9
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β (β―βπ) β
β0) |
8 | | nn0z 12531 |
. . . . . . . . 9
β’
((β―βπ)
β β0 β (β―βπ) β β€) |
9 | | fzoval 13580 |
. . . . . . . . 9
β’
((β―βπ)
β β€ β (0..^(β―βπ)) = (0...((β―βπ) β 1))) |
10 | 7, 8, 9 | 3syl 18 |
. . . . . . . 8
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β (0..^(β―βπ)) = (0...((β―βπ) β 1))) |
11 | 5, 10 | eleqtrd 2840 |
. . . . . . 7
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β π₯ β (0...((β―βπ) β 1))) |
12 | | fznn0sub2 13555 |
. . . . . . 7
β’ (π₯ β
(0...((β―βπ)
β 1)) β (((β―βπ) β 1) β π₯) β (0...((β―βπ) β 1))) |
13 | 11, 12 | syl 17 |
. . . . . 6
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β (((β―βπ) β 1) β π₯) β
(0...((β―βπ)
β 1))) |
14 | 13, 10 | eleqtrrd 2841 |
. . . . 5
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β (((β―βπ) β 1) β π₯) β
(0..^(β―βπ))) |
15 | 4, 14 | ffvelcdmd 7041 |
. . . 4
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β (πβ(((β―βπ) β 1) β π₯)) β π΄) |
16 | 15 | fmpttd 7068 |
. . 3
β’ (π β Word π΄ β (π₯ β (0..^(β―βπ)) β¦ (πβ(((β―βπ) β 1) β π₯))):(0..^(β―βπ))βΆπ΄) |
17 | | ffn 6673 |
. . 3
β’ ((π₯ β
(0..^(β―βπ))
β¦ (πβ(((β―βπ) β 1) β π₯))):(0..^(β―βπ))βΆπ΄ β (π₯ β (0..^(β―βπ)) β¦ (πβ(((β―βπ) β 1) β π₯))) Fn (0..^(β―βπ))) |
18 | | hashfn 14282 |
. . 3
β’ ((π₯ β
(0..^(β―βπ))
β¦ (πβ(((β―βπ) β 1) β π₯))) Fn (0..^(β―βπ)) β (β―β(π₯ β (0..^(β―βπ)) β¦ (πβ(((β―βπ) β 1) β π₯)))) =
(β―β(0..^(β―βπ)))) |
19 | 16, 17, 18 | 3syl 18 |
. 2
β’ (π β Word π΄ β (β―β(π₯ β (0..^(β―βπ)) β¦ (πβ(((β―βπ) β 1) β π₯)))) =
(β―β(0..^(β―βπ)))) |
20 | | hashfzo0 14337 |
. . 3
β’
((β―βπ)
β β0 β (β―β(0..^(β―βπ))) = (β―βπ)) |
21 | 6, 20 | syl 17 |
. 2
β’ (π β Word π΄ β
(β―β(0..^(β―βπ))) = (β―βπ)) |
22 | 2, 19, 21 | 3eqtrd 2781 |
1
β’ (π β Word π΄ β (β―β(reverseβπ)) = (β―βπ)) |