Step | Hyp | Ref
| Expression |
1 | | s1cli 14500 |
. . . . 5
β’
β¨βπββ© β Word V |
2 | | s1len 14501 |
. . . . . . 7
β’
(β―ββ¨βπββ©) = 1 |
3 | | 1nn 12171 |
. . . . . . 7
β’ 1 β
β |
4 | 2, 3 | eqeltri 2834 |
. . . . . 6
β’
(β―ββ¨βπββ©) β
β |
5 | | lbfzo0 13619 |
. . . . . 6
β’ (0 β
(0..^(β―ββ¨βπββ©)) β
(β―ββ¨βπββ©) β
β) |
6 | 4, 5 | mpbir 230 |
. . . . 5
β’ 0 β
(0..^(β―ββ¨βπββ©)) |
7 | | revfv 14658 |
. . . . 5
β’
((β¨βπββ© β Word V β§ 0 β
(0..^(β―ββ¨βπββ©))) β
((reverseββ¨βπββ©)β0) =
(β¨βπββ©β(((β―ββ¨βπββ©) β 1) β
0))) |
8 | 1, 6, 7 | mp2an 691 |
. . . 4
β’
((reverseββ¨βπββ©)β0) =
(β¨βπββ©β(((β―ββ¨βπββ©) β 1) β
0)) |
9 | 2 | oveq1i 7372 |
. . . . . . . . 9
β’
((β―ββ¨βπββ©) β 1) = (1 β
1) |
10 | | 1m1e0 12232 |
. . . . . . . . 9
β’ (1
β 1) = 0 |
11 | 9, 10 | eqtri 2765 |
. . . . . . . 8
β’
((β―ββ¨βπββ©) β 1) =
0 |
12 | 11 | oveq1i 7372 |
. . . . . . 7
β’
(((β―ββ¨βπββ©) β 1) β 0) = (0
β 0) |
13 | | 0m0e0 12280 |
. . . . . . 7
β’ (0
β 0) = 0 |
14 | 12, 13 | eqtri 2765 |
. . . . . 6
β’
(((β―ββ¨βπββ©) β 1) β 0) =
0 |
15 | 14 | fveq2i 6850 |
. . . . 5
β’
(β¨βπββ©β(((β―ββ¨βπββ©) β 1) β 0)) =
(β¨βπββ©β0) |
16 | | ids1 14492 |
. . . . . . 7
β’
β¨βπββ© = β¨β( I
βπ)ββ© |
17 | 16 | fveq1i 6848 |
. . . . . 6
β’
(β¨βπββ©β0) = (β¨β( I
βπ)ββ©β0) |
18 | | fvex 6860 |
. . . . . . 7
β’ ( I
βπ) β
V |
19 | | s1fv 14505 |
. . . . . . 7
β’ (( I
βπ) β V β
(β¨β( I βπ)ββ©β0) = ( I βπ)) |
20 | 18, 19 | ax-mp 5 |
. . . . . 6
β’
(β¨β( I βπ)ββ©β0) = ( I βπ) |
21 | 17, 20 | eqtri 2765 |
. . . . 5
β’
(β¨βπββ©β0) = ( I βπ) |
22 | 15, 21 | eqtri 2765 |
. . . 4
β’
(β¨βπββ©β(((β―ββ¨βπββ©) β 1) β 0)) = ( I
βπ) |
23 | 8, 22 | eqtri 2765 |
. . 3
β’
((reverseββ¨βπββ©)β0) = ( I βπ) |
24 | | s1eq 14495 |
. . 3
β’
(((reverseββ¨βπββ©)β0) = ( I βπ) β
β¨β((reverseββ¨βπββ©)β0)ββ© =
β¨β( I βπ)ββ©) |
25 | 23, 24 | ax-mp 5 |
. 2
β’
β¨β((reverseββ¨βπββ©)β0)ββ© =
β¨β( I βπ)ββ© |
26 | | revcl 14656 |
. . . 4
β’
(β¨βπββ© β Word V β
(reverseββ¨βπββ©) β Word
V) |
27 | 1, 26 | ax-mp 5 |
. . 3
β’
(reverseββ¨βπββ©) β Word
V |
28 | | revlen 14657 |
. . . . 5
β’
(β¨βπββ© β Word V β
(β―β(reverseββ¨βπββ©)) =
(β―ββ¨βπββ©)) |
29 | 1, 28 | ax-mp 5 |
. . . 4
β’
(β―β(reverseββ¨βπββ©)) =
(β―ββ¨βπββ©) |
30 | 29, 2 | eqtri 2765 |
. . 3
β’
(β―β(reverseββ¨βπββ©)) = 1 |
31 | | eqs1 14507 |
. . 3
β’
(((reverseββ¨βπββ©) β Word V β§
(β―β(reverseββ¨βπββ©)) = 1) β
(reverseββ¨βπββ©) =
β¨β((reverseββ¨βπββ©)β0)ββ©) |
32 | 27, 30, 31 | mp2an 691 |
. 2
β’
(reverseββ¨βπββ©) =
β¨β((reverseββ¨βπββ©)β0)ββ© |
33 | 25, 32, 16 | 3eqtr4i 2775 |
1
β’
(reverseββ¨βπββ©) = β¨βπββ© |