Step | Hyp | Ref
| Expression |
1 | | signsv.p |
. . . . . . . 8
⒠⨣ =
(π β {-1, 0, 1}, π β {-1, 0, 1} β¦
if(π = 0, π, π)) |
2 | | signsv.w |
. . . . . . . 8
β’ π = {β¨(Baseβndx), {-1,
0, 1}β©, β¨(+gβndx), ⨣
β©} |
3 | | signsv.t |
. . . . . . . 8
β’ π = (π β Word β β¦ (π β
(0..^(β―βπ))
β¦ (π
Ξ£g (π β (0...π) β¦ (sgnβ(πβπ)))))) |
4 | | signsv.v |
. . . . . . . 8
β’ π = (π β Word β β¦ Ξ£π β
(1..^(β―βπ))if(((πβπ)βπ) β ((πβπ)β(π β 1)), 1, 0)) |
5 | 1, 2, 3, 4 | signstf 33646 |
. . . . . . 7
β’ (πΉ β Word β β
(πβπΉ) β Word β) |
6 | | wrdf 14471 |
. . . . . . 7
β’ ((πβπΉ) β Word β β (πβπΉ):(0..^(β―β(πβπΉ)))βΆβ) |
7 | | ffn 6717 |
. . . . . . 7
β’ ((πβπΉ):(0..^(β―β(πβπΉ)))βΆβ β (πβπΉ) Fn (0..^(β―β(πβπΉ)))) |
8 | 5, 6, 7 | 3syl 18 |
. . . . . 6
β’ (πΉ β Word β β
(πβπΉ) Fn (0..^(β―β(πβπΉ)))) |
9 | 1, 2, 3, 4 | signstlen 33647 |
. . . . . . . 8
β’ (πΉ β Word β β
(β―β(πβπΉ)) = (β―βπΉ)) |
10 | 9 | oveq2d 7427 |
. . . . . . 7
β’ (πΉ β Word β β
(0..^(β―β(πβπΉ))) = (0..^(β―βπΉ))) |
11 | 10 | fneq2d 6643 |
. . . . . 6
β’ (πΉ β Word β β
((πβπΉ) Fn (0..^(β―β(πβπΉ))) β (πβπΉ) Fn (0..^(β―βπΉ)))) |
12 | 8, 11 | mpbid 231 |
. . . . 5
β’ (πΉ β Word β β
(πβπΉ) Fn (0..^(β―βπΉ))) |
13 | | fnresin 31888 |
. . . . 5
β’ ((πβπΉ) Fn (0..^(β―βπΉ)) β ((πβπΉ) βΎ (0..^π)) Fn ((0..^(β―βπΉ)) β© (0..^π))) |
14 | 12, 13 | syl 17 |
. . . 4
β’ (πΉ β Word β β
((πβπΉ) βΎ (0..^π)) Fn ((0..^(β―βπΉ)) β© (0..^π))) |
15 | 14 | adantr 481 |
. . 3
β’ ((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β ((πβπΉ) βΎ (0..^π)) Fn ((0..^(β―βπΉ)) β© (0..^π))) |
16 | | elfzuz3 13500 |
. . . . . 6
β’ (π β
(0...(β―βπΉ))
β (β―βπΉ)
β (β€β₯βπ)) |
17 | | fzoss2 13662 |
. . . . . 6
β’
((β―βπΉ)
β (β€β₯βπ) β (0..^π) β (0..^(β―βπΉ))) |
18 | 16, 17 | syl 17 |
. . . . 5
β’ (π β
(0...(β―βπΉ))
β (0..^π) β
(0..^(β―βπΉ))) |
19 | 18 | adantl 482 |
. . . 4
β’ ((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β (0..^π) β
(0..^(β―βπΉ))) |
20 | | incom 4201 |
. . . . . 6
β’
((0..^π) β©
(0..^(β―βπΉ))) =
((0..^(β―βπΉ))
β© (0..^π)) |
21 | | df-ss 3965 |
. . . . . . 7
β’
((0..^π) β
(0..^(β―βπΉ))
β ((0..^π) β©
(0..^(β―βπΉ))) =
(0..^π)) |
22 | 21 | biimpi 215 |
. . . . . 6
β’
((0..^π) β
(0..^(β―βπΉ))
β ((0..^π) β©
(0..^(β―βπΉ))) =
(0..^π)) |
23 | 20, 22 | eqtr3id 2786 |
. . . . 5
β’
((0..^π) β
(0..^(β―βπΉ))
β ((0..^(β―βπΉ)) β© (0..^π)) = (0..^π)) |
24 | 23 | fneq2d 6643 |
. . . 4
β’
((0..^π) β
(0..^(β―βπΉ))
β (((πβπΉ) βΎ (0..^π)) Fn ((0..^(β―βπΉ)) β© (0..^π)) β ((πβπΉ) βΎ (0..^π)) Fn (0..^π))) |
25 | 19, 24 | syl 17 |
. . 3
β’ ((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β (((πβπΉ) βΎ (0..^π)) Fn ((0..^(β―βπΉ)) β© (0..^π)) β ((πβπΉ) βΎ (0..^π)) Fn (0..^π))) |
26 | 15, 25 | mpbid 231 |
. 2
β’ ((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β ((πβπΉ) βΎ (0..^π)) Fn (0..^π)) |
27 | | wrdres 32141 |
. . . 4
β’ ((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β (πΉ βΎ
(0..^π)) β Word
β) |
28 | 1, 2, 3, 4 | signstf 33646 |
. . . 4
β’ ((πΉ βΎ (0..^π)) β Word β β (πβ(πΉ βΎ (0..^π))) β Word β) |
29 | | wrdf 14471 |
. . . 4
β’ ((πβ(πΉ βΎ (0..^π))) β Word β β (πβ(πΉ βΎ (0..^π))):(0..^(β―β(πβ(πΉ βΎ (0..^π)))))βΆβ) |
30 | | ffn 6717 |
. . . 4
β’ ((πβ(πΉ βΎ (0..^π))):(0..^(β―β(πβ(πΉ βΎ (0..^π)))))βΆβ β (πβ(πΉ βΎ (0..^π))) Fn (0..^(β―β(πβ(πΉ βΎ (0..^π)))))) |
31 | 27, 28, 29, 30 | 4syl 19 |
. . 3
β’ ((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β (πβ(πΉ βΎ (0..^π))) Fn (0..^(β―β(πβ(πΉ βΎ (0..^π)))))) |
32 | 1, 2, 3, 4 | signstlen 33647 |
. . . . . . 7
β’ ((πΉ βΎ (0..^π)) β Word β β
(β―β(πβ(πΉ βΎ (0..^π)))) = (β―β(πΉ βΎ (0..^π)))) |
33 | 27, 32 | syl 17 |
. . . . . 6
β’ ((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β (β―β(πβ(πΉ βΎ (0..^π)))) = (β―β(πΉ βΎ (0..^π)))) |
34 | | wrdfn 14480 |
. . . . . . . 8
β’ (πΉ β Word β β
πΉ Fn
(0..^(β―βπΉ))) |
35 | | fnssres 6673 |
. . . . . . . 8
β’ ((πΉ Fn (0..^(β―βπΉ)) β§ (0..^π) β (0..^(β―βπΉ))) β (πΉ βΎ (0..^π)) Fn (0..^π)) |
36 | 34, 18, 35 | syl2an 596 |
. . . . . . 7
β’ ((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β (πΉ βΎ
(0..^π)) Fn (0..^π)) |
37 | | hashfn 14337 |
. . . . . . 7
β’ ((πΉ βΎ (0..^π)) Fn (0..^π) β (β―β(πΉ βΎ (0..^π))) = (β―β(0..^π))) |
38 | 36, 37 | syl 17 |
. . . . . 6
β’ ((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β (β―β(πΉ
βΎ (0..^π))) =
(β―β(0..^π))) |
39 | | elfznn0 13596 |
. . . . . . . 8
β’ (π β
(0...(β―βπΉ))
β π β
β0) |
40 | | hashfzo0 14392 |
. . . . . . . 8
β’ (π β β0
β (β―β(0..^π)) = π) |
41 | 39, 40 | syl 17 |
. . . . . . 7
β’ (π β
(0...(β―βπΉ))
β (β―β(0..^π)) = π) |
42 | 41 | adantl 482 |
. . . . . 6
β’ ((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β (β―β(0..^π)) = π) |
43 | 33, 38, 42 | 3eqtrd 2776 |
. . . . 5
β’ ((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β (β―β(πβ(πΉ βΎ (0..^π)))) = π) |
44 | 43 | oveq2d 7427 |
. . . 4
β’ ((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β (0..^(β―β(πβ(πΉ βΎ (0..^π))))) = (0..^π)) |
45 | 44 | fneq2d 6643 |
. . 3
β’ ((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β ((πβ(πΉ βΎ (0..^π))) Fn (0..^(β―β(πβ(πΉ βΎ (0..^π))))) β (πβ(πΉ βΎ (0..^π))) Fn (0..^π))) |
46 | 31, 45 | mpbid 231 |
. 2
β’ ((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β (πβ(πΉ βΎ (0..^π))) Fn (0..^π)) |
47 | | fvres 6910 |
. . . . 5
β’ (π β (0..^π) β (((πβπΉ) βΎ (0..^π))βπ) = ((πβπΉ)βπ)) |
48 | 47 | ad3antlr 729 |
. . . 4
β’
(((((πΉ β Word
β β§ π β
(0...(β―βπΉ)))
β§ π β (0..^π)) β§ π β Word β) β§ πΉ = ((πΉ βΎ (0..^π)) ++ π)) β (((πβπΉ) βΎ (0..^π))βπ) = ((πβπΉ)βπ)) |
49 | | simpr 485 |
. . . . . 6
β’
(((((πΉ β Word
β β§ π β
(0...(β―βπΉ)))
β§ π β (0..^π)) β§ π β Word β) β§ πΉ = ((πΉ βΎ (0..^π)) ++ π)) β πΉ = ((πΉ βΎ (0..^π)) ++ π)) |
50 | 49 | fveq2d 6895 |
. . . . 5
β’
(((((πΉ β Word
β β§ π β
(0...(β―βπΉ)))
β§ π β (0..^π)) β§ π β Word β) β§ πΉ = ((πΉ βΎ (0..^π)) ++ π)) β (πβπΉ) = (πβ((πΉ βΎ (0..^π)) ++ π))) |
51 | 50 | fveq1d 6893 |
. . . 4
β’
(((((πΉ β Word
β β§ π β
(0...(β―βπΉ)))
β§ π β (0..^π)) β§ π β Word β) β§ πΉ = ((πΉ βΎ (0..^π)) ++ π)) β ((πβπΉ)βπ) = ((πβ((πΉ βΎ (0..^π)) ++ π))βπ)) |
52 | 27 | ad3antrrr 728 |
. . . . 5
β’
(((((πΉ β Word
β β§ π β
(0...(β―βπΉ)))
β§ π β (0..^π)) β§ π β Word β) β§ πΉ = ((πΉ βΎ (0..^π)) ++ π)) β (πΉ βΎ (0..^π)) β Word β) |
53 | | simplr 767 |
. . . . 5
β’
(((((πΉ β Word
β β§ π β
(0...(β―βπΉ)))
β§ π β (0..^π)) β§ π β Word β) β§ πΉ = ((πΉ βΎ (0..^π)) ++ π)) β π β Word β) |
54 | 38, 42 | eqtrd 2772 |
. . . . . . . . 9
β’ ((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β (β―β(πΉ
βΎ (0..^π))) = π) |
55 | 54 | oveq2d 7427 |
. . . . . . . 8
β’ ((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β (0..^(β―β(πΉ βΎ (0..^π)))) = (0..^π)) |
56 | 55 | eleq2d 2819 |
. . . . . . 7
β’ ((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β (π β
(0..^(β―β(πΉ
βΎ (0..^π)))) β
π β (0..^π))) |
57 | 56 | biimpar 478 |
. . . . . 6
β’ (((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β§ π β (0..^π)) β π β (0..^(β―β(πΉ βΎ (0..^π))))) |
58 | 57 | ad2antrr 724 |
. . . . 5
β’
(((((πΉ β Word
β β§ π β
(0...(β―βπΉ)))
β§ π β (0..^π)) β§ π β Word β) β§ πΉ = ((πΉ βΎ (0..^π)) ++ π)) β π β (0..^(β―β(πΉ βΎ (0..^π))))) |
59 | 1, 2, 3, 4 | signstfvc 33654 |
. . . . 5
β’ (((πΉ βΎ (0..^π)) β Word β β§ π β Word β β§ π β
(0..^(β―β(πΉ
βΎ (0..^π))))) β
((πβ((πΉ βΎ (0..^π)) ++ π))βπ) = ((πβ(πΉ βΎ (0..^π)))βπ)) |
60 | 52, 53, 58, 59 | syl3anc 1371 |
. . . 4
β’
(((((πΉ β Word
β β§ π β
(0...(β―βπΉ)))
β§ π β (0..^π)) β§ π β Word β) β§ πΉ = ((πΉ βΎ (0..^π)) ++ π)) β ((πβ((πΉ βΎ (0..^π)) ++ π))βπ) = ((πβ(πΉ βΎ (0..^π)))βπ)) |
61 | 48, 51, 60 | 3eqtrd 2776 |
. . 3
β’
(((((πΉ β Word
β β§ π β
(0...(β―βπΉ)))
β§ π β (0..^π)) β§ π β Word β) β§ πΉ = ((πΉ βΎ (0..^π)) ++ π)) β (((πβπΉ) βΎ (0..^π))βπ) = ((πβ(πΉ βΎ (0..^π)))βπ)) |
62 | | wrdsplex 32142 |
. . . 4
β’ ((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β βπ β Word
βπΉ = ((πΉ βΎ (0..^π)) ++ π)) |
63 | 62 | adantr 481 |
. . 3
β’ (((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β§ π β (0..^π)) β βπ β Word βπΉ = ((πΉ βΎ (0..^π)) ++ π)) |
64 | 61, 63 | r19.29a 3162 |
. 2
β’ (((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β§ π β (0..^π)) β (((πβπΉ) βΎ (0..^π))βπ) = ((πβ(πΉ βΎ (0..^π)))βπ)) |
65 | 26, 46, 64 | eqfnfvd 7035 |
1
β’ ((πΉ β Word β β§ π β
(0...(β―βπΉ)))
β ((πβπΉ) βΎ (0..^π)) = (πβ(πΉ βΎ (0..^π)))) |