Step | Hyp | Ref
| Expression |
1 | | revcl 14656 |
. . . 4
β’ (π β Word π΄ β (reverseβπ) β Word π΄) |
2 | | revcl 14656 |
. . . 4
β’
((reverseβπ)
β Word π΄ β
(reverseβ(reverseβπ)) β Word π΄) |
3 | | wrdf 14414 |
. . . 4
β’
((reverseβ(reverseβπ)) β Word π΄ β (reverseβ(reverseβπ)):(0..^(β―β(reverseβ(reverseβπ))))βΆπ΄) |
4 | | ffn 6673 |
. . . 4
β’
((reverseβ(reverseβπ)):(0..^(β―β(reverseβ(reverseβπ))))βΆπ΄ β (reverseβ(reverseβπ)) Fn
(0..^(β―β(reverseβ(reverseβπ))))) |
5 | 1, 2, 3, 4 | 4syl 19 |
. . 3
β’ (π β Word π΄ β (reverseβ(reverseβπ)) Fn
(0..^(β―β(reverseβ(reverseβπ))))) |
6 | | revlen 14657 |
. . . . . . 7
β’
((reverseβπ)
β Word π΄ β
(β―β(reverseβ(reverseβπ))) = (β―β(reverseβπ))) |
7 | 1, 6 | syl 17 |
. . . . . 6
β’ (π β Word π΄ β
(β―β(reverseβ(reverseβπ))) = (β―β(reverseβπ))) |
8 | | revlen 14657 |
. . . . . 6
β’ (π β Word π΄ β (β―β(reverseβπ)) = (β―βπ)) |
9 | 7, 8 | eqtrd 2777 |
. . . . 5
β’ (π β Word π΄ β
(β―β(reverseβ(reverseβπ))) = (β―βπ)) |
10 | 9 | oveq2d 7378 |
. . . 4
β’ (π β Word π΄ β
(0..^(β―β(reverseβ(reverseβπ)))) = (0..^(β―βπ))) |
11 | 10 | fneq2d 6601 |
. . 3
β’ (π β Word π΄ β ((reverseβ(reverseβπ)) Fn
(0..^(β―β(reverseβ(reverseβπ)))) β
(reverseβ(reverseβπ)) Fn (0..^(β―βπ)))) |
12 | 5, 11 | mpbid 231 |
. 2
β’ (π β Word π΄ β (reverseβ(reverseβπ)) Fn (0..^(β―βπ))) |
13 | | wrdfn 14423 |
. 2
β’ (π β Word π΄ β π Fn (0..^(β―βπ))) |
14 | | simpr 486 |
. . . . 5
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β π₯ β (0..^(β―βπ))) |
15 | 8 | adantr 482 |
. . . . . 6
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β
(β―β(reverseβπ)) = (β―βπ)) |
16 | 15 | oveq2d 7378 |
. . . . 5
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β
(0..^(β―β(reverseβπ))) = (0..^(β―βπ))) |
17 | 14, 16 | eleqtrrd 2841 |
. . . 4
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β π₯ β
(0..^(β―β(reverseβπ)))) |
18 | | revfv 14658 |
. . . 4
β’
(((reverseβπ)
β Word π΄ β§ π₯ β
(0..^(β―β(reverseβπ)))) β
((reverseβ(reverseβπ))βπ₯) = ((reverseβπ)β(((β―β(reverseβπ)) β 1) β π₯))) |
19 | 1, 17, 18 | syl2an2r 684 |
. . 3
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β
((reverseβ(reverseβπ))βπ₯) = ((reverseβπ)β(((β―β(reverseβπ)) β 1) β π₯))) |
20 | 15 | oveq1d 7377 |
. . . . 5
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β
((β―β(reverseβπ)) β 1) = ((β―βπ) β 1)) |
21 | 20 | fvoveq1d 7384 |
. . . 4
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β ((reverseβπ)β(((β―β(reverseβπ)) β 1) β π₯)) = ((reverseβπ)β(((β―βπ) β 1) β π₯))) |
22 | | lencl 14428 |
. . . . . . . . . . . 12
β’ (π β Word π΄ β (β―βπ) β
β0) |
23 | 22 | nn0zd 12532 |
. . . . . . . . . . 11
β’ (π β Word π΄ β (β―βπ) β β€) |
24 | | fzoval 13580 |
. . . . . . . . . . 11
β’
((β―βπ)
β β€ β (0..^(β―βπ)) = (0...((β―βπ) β 1))) |
25 | 23, 24 | syl 17 |
. . . . . . . . . 10
β’ (π β Word π΄ β (0..^(β―βπ)) = (0...((β―βπ) β 1))) |
26 | 25 | eleq2d 2824 |
. . . . . . . . 9
β’ (π β Word π΄ β (π₯ β (0..^(β―βπ)) β π₯ β (0...((β―βπ) β 1)))) |
27 | 26 | biimpa 478 |
. . . . . . . 8
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β π₯ β (0...((β―βπ) β 1))) |
28 | | fznn0sub2 13555 |
. . . . . . . 8
β’ (π₯ β
(0...((β―βπ)
β 1)) β (((β―βπ) β 1) β π₯) β (0...((β―βπ) β 1))) |
29 | 27, 28 | syl 17 |
. . . . . . 7
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β (((β―βπ) β 1) β π₯) β
(0...((β―βπ)
β 1))) |
30 | 25 | adantr 482 |
. . . . . . 7
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β (0..^(β―βπ)) = (0...((β―βπ) β 1))) |
31 | 29, 30 | eleqtrrd 2841 |
. . . . . 6
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β (((β―βπ) β 1) β π₯) β
(0..^(β―βπ))) |
32 | | revfv 14658 |
. . . . . 6
β’ ((π β Word π΄ β§ (((β―βπ) β 1) β π₯) β (0..^(β―βπ))) β ((reverseβπ)β(((β―βπ) β 1) β π₯)) = (πβ(((β―βπ) β 1) β (((β―βπ) β 1) β π₯)))) |
33 | 31, 32 | syldan 592 |
. . . . 5
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β ((reverseβπ)β(((β―βπ) β 1) β π₯)) = (πβ(((β―βπ) β 1) β (((β―βπ) β 1) β π₯)))) |
34 | | peano2zm 12553 |
. . . . . . . . 9
β’
((β―βπ)
β β€ β ((β―βπ) β 1) β
β€) |
35 | 23, 34 | syl 17 |
. . . . . . . 8
β’ (π β Word π΄ β ((β―βπ) β 1) β
β€) |
36 | 35 | zcnd 12615 |
. . . . . . 7
β’ (π β Word π΄ β ((β―βπ) β 1) β
β) |
37 | | elfzoelz 13579 |
. . . . . . . 8
β’ (π₯ β
(0..^(β―βπ))
β π₯ β
β€) |
38 | 37 | zcnd 12615 |
. . . . . . 7
β’ (π₯ β
(0..^(β―βπ))
β π₯ β
β) |
39 | | nncan 11437 |
. . . . . . 7
β’
((((β―βπ)
β 1) β β β§ π₯ β β) β
(((β―βπ) β
1) β (((β―βπ) β 1) β π₯)) = π₯) |
40 | 36, 38, 39 | syl2an 597 |
. . . . . 6
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β (((β―βπ) β 1) β
(((β―βπ) β
1) β π₯)) = π₯) |
41 | 40 | fveq2d 6851 |
. . . . 5
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β (πβ(((β―βπ) β 1) β (((β―βπ) β 1) β π₯))) = (πβπ₯)) |
42 | 33, 41 | eqtrd 2777 |
. . . 4
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β ((reverseβπ)β(((β―βπ) β 1) β π₯)) = (πβπ₯)) |
43 | 21, 42 | eqtrd 2777 |
. . 3
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β ((reverseβπ)β(((β―β(reverseβπ)) β 1) β π₯)) = (πβπ₯)) |
44 | 19, 43 | eqtrd 2777 |
. 2
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β
((reverseβ(reverseβπ))βπ₯) = (πβπ₯)) |
45 | 12, 13, 44 | eqfnfvd 6990 |
1
β’ (π β Word π΄ β (reverseβ(reverseβπ)) = π) |