Step | Hyp | Ref
| Expression |
1 | | oveq2 7417 |
. . . . . . . 8
β’ (π = β
β (πΉ ++ π) = (πΉ ++ β
)) |
2 | 1 | fveq2d 6896 |
. . . . . . 7
β’ (π = β
β (πβ(πΉ ++ π)) = (πβ(πΉ ++ β
))) |
3 | 2 | fveq1d 6894 |
. . . . . 6
β’ (π = β
β ((πβ(πΉ ++ π))βπ) = ((πβ(πΉ ++ β
))βπ)) |
4 | 3 | eqeq1d 2735 |
. . . . 5
β’ (π = β
β (((πβ(πΉ ++ π))βπ) = ((πβπΉ)βπ) β ((πβ(πΉ ++ β
))βπ) = ((πβπΉ)βπ))) |
5 | 4 | imbi2d 341 |
. . . 4
β’ (π = β
β (((πΉ β Word β β§ π β
(0..^(β―βπΉ)))
β ((πβ(πΉ ++ π))βπ) = ((πβπΉ)βπ)) β ((πΉ β Word β β§ π β (0..^(β―βπΉ))) β ((πβ(πΉ ++ β
))βπ) = ((πβπΉ)βπ)))) |
6 | | oveq2 7417 |
. . . . . . . 8
β’ (π = π β (πΉ ++ π) = (πΉ ++ π)) |
7 | 6 | fveq2d 6896 |
. . . . . . 7
β’ (π = π β (πβ(πΉ ++ π)) = (πβ(πΉ ++ π))) |
8 | 7 | fveq1d 6894 |
. . . . . 6
β’ (π = π β ((πβ(πΉ ++ π))βπ) = ((πβ(πΉ ++ π))βπ)) |
9 | 8 | eqeq1d 2735 |
. . . . 5
β’ (π = π β (((πβ(πΉ ++ π))βπ) = ((πβπΉ)βπ) β ((πβ(πΉ ++ π))βπ) = ((πβπΉ)βπ))) |
10 | 9 | imbi2d 341 |
. . . 4
β’ (π = π β (((πΉ β Word β β§ π β (0..^(β―βπΉ))) β ((πβ(πΉ ++ π))βπ) = ((πβπΉ)βπ)) β ((πΉ β Word β β§ π β (0..^(β―βπΉ))) β ((πβ(πΉ ++ π))βπ) = ((πβπΉ)βπ)))) |
11 | | oveq2 7417 |
. . . . . . . 8
β’ (π = (π ++ β¨βπββ©) β (πΉ ++ π) = (πΉ ++ (π ++ β¨βπββ©))) |
12 | 11 | fveq2d 6896 |
. . . . . . 7
β’ (π = (π ++ β¨βπββ©) β (πβ(πΉ ++ π)) = (πβ(πΉ ++ (π ++ β¨βπββ©)))) |
13 | 12 | fveq1d 6894 |
. . . . . 6
β’ (π = (π ++ β¨βπββ©) β ((πβ(πΉ ++ π))βπ) = ((πβ(πΉ ++ (π ++ β¨βπββ©)))βπ)) |
14 | 13 | eqeq1d 2735 |
. . . . 5
β’ (π = (π ++ β¨βπββ©) β (((πβ(πΉ ++ π))βπ) = ((πβπΉ)βπ) β ((πβ(πΉ ++ (π ++ β¨βπββ©)))βπ) = ((πβπΉ)βπ))) |
15 | 14 | imbi2d 341 |
. . . 4
β’ (π = (π ++ β¨βπββ©) β (((πΉ β Word β β§ π β (0..^(β―βπΉ))) β ((πβ(πΉ ++ π))βπ) = ((πβπΉ)βπ)) β ((πΉ β Word β β§ π β (0..^(β―βπΉ))) β ((πβ(πΉ ++ (π ++ β¨βπββ©)))βπ) = ((πβπΉ)βπ)))) |
16 | | oveq2 7417 |
. . . . . . . 8
β’ (π = πΊ β (πΉ ++ π) = (πΉ ++ πΊ)) |
17 | 16 | fveq2d 6896 |
. . . . . . 7
β’ (π = πΊ β (πβ(πΉ ++ π)) = (πβ(πΉ ++ πΊ))) |
18 | 17 | fveq1d 6894 |
. . . . . 6
β’ (π = πΊ β ((πβ(πΉ ++ π))βπ) = ((πβ(πΉ ++ πΊ))βπ)) |
19 | 18 | eqeq1d 2735 |
. . . . 5
β’ (π = πΊ β (((πβ(πΉ ++ π))βπ) = ((πβπΉ)βπ) β ((πβ(πΉ ++ πΊ))βπ) = ((πβπΉ)βπ))) |
20 | 19 | imbi2d 341 |
. . . 4
β’ (π = πΊ β (((πΉ β Word β β§ π β (0..^(β―βπΉ))) β ((πβ(πΉ ++ π))βπ) = ((πβπΉ)βπ)) β ((πΉ β Word β β§ π β (0..^(β―βπΉ))) β ((πβ(πΉ ++ πΊ))βπ) = ((πβπΉ)βπ)))) |
21 | | ccatrid 14537 |
. . . . . . 7
β’ (πΉ β Word β β
(πΉ ++ β
) = πΉ) |
22 | 21 | fveq2d 6896 |
. . . . . 6
β’ (πΉ β Word β β
(πβ(πΉ ++ β
)) = (πβπΉ)) |
23 | 22 | fveq1d 6894 |
. . . . 5
β’ (πΉ β Word β β
((πβ(πΉ ++ β
))βπ) = ((πβπΉ)βπ)) |
24 | 23 | adantr 482 |
. . . 4
β’ ((πΉ β Word β β§ π β
(0..^(β―βπΉ)))
β ((πβ(πΉ ++ β
))βπ) = ((πβπΉ)βπ)) |
25 | | s1cl 14552 |
. . . . . . . . . . . . . 14
β’ (π β β β
β¨βπββ©
β Word β) |
26 | | ccatass 14538 |
. . . . . . . . . . . . . 14
β’ ((πΉ β Word β β§ π β Word β β§
β¨βπββ©
β Word β) β ((πΉ ++ π) ++ β¨βπββ©) = (πΉ ++ (π ++ β¨βπββ©))) |
27 | 25, 26 | syl3an3 1166 |
. . . . . . . . . . . . 13
β’ ((πΉ β Word β β§ π β Word β β§ π β β) β ((πΉ ++ π) ++ β¨βπββ©) = (πΉ ++ (π ++ β¨βπββ©))) |
28 | 27 | 3expb 1121 |
. . . . . . . . . . . 12
β’ ((πΉ β Word β β§
(π β Word β
β§ π β β))
β ((πΉ ++ π) ++ β¨βπββ©) = (πΉ ++ (π ++ β¨βπββ©))) |
29 | 28 | adantlr 714 |
. . . . . . . . . . 11
β’ (((πΉ β Word β β§ π β
(0..^(β―βπΉ)))
β§ (π β Word
β β§ π β
β)) β ((πΉ ++
π) ++ β¨βπββ©) = (πΉ ++ (π ++ β¨βπββ©))) |
30 | 29 | fveq2d 6896 |
. . . . . . . . . 10
β’ (((πΉ β Word β β§ π β
(0..^(β―βπΉ)))
β§ (π β Word
β β§ π β
β)) β (πβ((πΉ ++ π) ++ β¨βπββ©)) = (πβ(πΉ ++ (π ++ β¨βπββ©)))) |
31 | 30 | fveq1d 6894 |
. . . . . . . . 9
β’ (((πΉ β Word β β§ π β
(0..^(β―βπΉ)))
β§ (π β Word
β β§ π β
β)) β ((πβ((πΉ ++ π) ++ β¨βπββ©))βπ) = ((πβ(πΉ ++ (π ++ β¨βπββ©)))βπ)) |
32 | | ccatcl 14524 |
. . . . . . . . . . 11
β’ ((πΉ β Word β β§ π β Word β) β
(πΉ ++ π) β Word β) |
33 | 32 | ad2ant2r 746 |
. . . . . . . . . 10
β’ (((πΉ β Word β β§ π β
(0..^(β―βπΉ)))
β§ (π β Word
β β§ π β
β)) β (πΉ ++
π) β Word
β) |
34 | | simprr 772 |
. . . . . . . . . 10
β’ (((πΉ β Word β β§ π β
(0..^(β―βπΉ)))
β§ (π β Word
β β§ π β
β)) β π β
β) |
35 | | lencl 14483 |
. . . . . . . . . . . . . . . 16
β’ (πΉ β Word β β
(β―βπΉ) β
β0) |
36 | 35 | nn0zd 12584 |
. . . . . . . . . . . . . . 15
β’ (πΉ β Word β β
(β―βπΉ) β
β€) |
37 | 36 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((πΉ β Word β β§ π β Word β) β
(β―βπΉ) β
β€) |
38 | | lencl 14483 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ ++ π) β Word β β
(β―β(πΉ ++ π)) β
β0) |
39 | 32, 38 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β Word β β§ π β Word β) β
(β―β(πΉ ++ π)) β
β0) |
40 | 39 | nn0zd 12584 |
. . . . . . . . . . . . . 14
β’ ((πΉ β Word β β§ π β Word β) β
(β―β(πΉ ++ π)) β
β€) |
41 | 35 | nn0red 12533 |
. . . . . . . . . . . . . . . 16
β’ (πΉ β Word β β
(β―βπΉ) β
β) |
42 | | lencl 14483 |
. . . . . . . . . . . . . . . 16
β’ (π β Word β β
(β―βπ) β
β0) |
43 | | nn0addge1 12518 |
. . . . . . . . . . . . . . . 16
β’
(((β―βπΉ)
β β β§ (β―βπ) β β0) β
(β―βπΉ) β€
((β―βπΉ) +
(β―βπ))) |
44 | 41, 42, 43 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β Word β β§ π β Word β) β
(β―βπΉ) β€
((β―βπΉ) +
(β―βπ))) |
45 | | ccatlen 14525 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β Word β β§ π β Word β) β
(β―β(πΉ ++ π)) = ((β―βπΉ) + (β―βπ))) |
46 | 44, 45 | breqtrrd 5177 |
. . . . . . . . . . . . . 14
β’ ((πΉ β Word β β§ π β Word β) β
(β―βπΉ) β€
(β―β(πΉ ++ π))) |
47 | | eluz2 12828 |
. . . . . . . . . . . . . 14
β’
((β―β(πΉ
++ π)) β
(β€β₯β(β―βπΉ)) β ((β―βπΉ) β β€ β§ (β―β(πΉ ++ π)) β β€ β§ (β―βπΉ) β€ (β―β(πΉ ++ π)))) |
48 | 37, 40, 46, 47 | syl3anbrc 1344 |
. . . . . . . . . . . . 13
β’ ((πΉ β Word β β§ π β Word β) β
(β―β(πΉ ++ π)) β
(β€β₯β(β―βπΉ))) |
49 | | fzoss2 13660 |
. . . . . . . . . . . . 13
β’
((β―β(πΉ
++ π)) β
(β€β₯β(β―βπΉ)) β (0..^(β―βπΉ)) β
(0..^(β―β(πΉ ++
π)))) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . 12
β’ ((πΉ β Word β β§ π β Word β) β
(0..^(β―βπΉ))
β (0..^(β―β(πΉ ++ π)))) |
51 | 50 | ad2ant2r 746 |
. . . . . . . . . . 11
β’ (((πΉ β Word β β§ π β
(0..^(β―βπΉ)))
β§ (π β Word
β β§ π β
β)) β (0..^(β―βπΉ)) β (0..^(β―β(πΉ ++ π)))) |
52 | | simplr 768 |
. . . . . . . . . . 11
β’ (((πΉ β Word β β§ π β
(0..^(β―βπΉ)))
β§ (π β Word
β β§ π β
β)) β π β
(0..^(β―βπΉ))) |
53 | 51, 52 | sseldd 3984 |
. . . . . . . . . 10
β’ (((πΉ β Word β β§ π β
(0..^(β―βπΉ)))
β§ (π β Word
β β§ π β
β)) β π β
(0..^(β―β(πΉ ++
π)))) |
54 | | signsv.p |
. . . . . . . . . . 11
⒠⨣ =
(π β {-1, 0, 1}, π β {-1, 0, 1} β¦
if(π = 0, π, π)) |
55 | | signsv.w |
. . . . . . . . . . 11
β’ π = {β¨(Baseβndx), {-1,
0, 1}β©, β¨(+gβndx), ⨣
β©} |
56 | | signsv.t |
. . . . . . . . . . 11
β’ π = (π β Word β β¦ (π β
(0..^(β―βπ))
β¦ (π
Ξ£g (π β (0...π) β¦ (sgnβ(πβπ)))))) |
57 | | signsv.v |
. . . . . . . . . . 11
β’ π = (π β Word β β¦ Ξ£π β
(1..^(β―βπ))if(((πβπ)βπ) β ((πβπ)β(π β 1)), 1, 0)) |
58 | 54, 55, 56, 57 | signstfvp 33582 |
. . . . . . . . . 10
β’ (((πΉ ++ π) β Word β β§ π β β β§ π β
(0..^(β―β(πΉ ++
π)))) β ((πβ((πΉ ++ π) ++ β¨βπββ©))βπ) = ((πβ(πΉ ++ π))βπ)) |
59 | 33, 34, 53, 58 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΉ β Word β β§ π β
(0..^(β―βπΉ)))
β§ (π β Word
β β§ π β
β)) β ((πβ((πΉ ++ π) ++ β¨βπββ©))βπ) = ((πβ(πΉ ++ π))βπ)) |
60 | 31, 59 | eqtr3d 2775 |
. . . . . . . 8
β’ (((πΉ β Word β β§ π β
(0..^(β―βπΉ)))
β§ (π β Word
β β§ π β
β)) β ((πβ(πΉ ++ (π ++ β¨βπββ©)))βπ) = ((πβ(πΉ ++ π))βπ)) |
61 | | id 22 |
. . . . . . . 8
β’ (((πβ(πΉ ++ π))βπ) = ((πβπΉ)βπ) β ((πβ(πΉ ++ π))βπ) = ((πβπΉ)βπ)) |
62 | 60, 61 | sylan9eq 2793 |
. . . . . . 7
β’ ((((πΉ β Word β β§ π β
(0..^(β―βπΉ)))
β§ (π β Word
β β§ π β
β)) β§ ((πβ(πΉ ++ π))βπ) = ((πβπΉ)βπ)) β ((πβ(πΉ ++ (π ++ β¨βπββ©)))βπ) = ((πβπΉ)βπ)) |
63 | 62 | ex 414 |
. . . . . 6
β’ (((πΉ β Word β β§ π β
(0..^(β―βπΉ)))
β§ (π β Word
β β§ π β
β)) β (((πβ(πΉ ++ π))βπ) = ((πβπΉ)βπ) β ((πβ(πΉ ++ (π ++ β¨βπββ©)))βπ) = ((πβπΉ)βπ))) |
64 | 63 | expcom 415 |
. . . . 5
β’ ((π β Word β β§ π β β) β ((πΉ β Word β β§ π β
(0..^(β―βπΉ)))
β (((πβ(πΉ ++ π))βπ) = ((πβπΉ)βπ) β ((πβ(πΉ ++ (π ++ β¨βπββ©)))βπ) = ((πβπΉ)βπ)))) |
65 | 64 | a2d 29 |
. . . 4
β’ ((π β Word β β§ π β β) β (((πΉ β Word β β§ π β
(0..^(β―βπΉ)))
β ((πβ(πΉ ++ π))βπ) = ((πβπΉ)βπ)) β ((πΉ β Word β β§ π β (0..^(β―βπΉ))) β ((πβ(πΉ ++ (π ++ β¨βπββ©)))βπ) = ((πβπΉ)βπ)))) |
66 | 5, 10, 15, 20, 24, 65 | wrdind 14672 |
. . 3
β’ (πΊ β Word β β
((πΉ β Word β
β§ π β
(0..^(β―βπΉ)))
β ((πβ(πΉ ++ πΊ))βπ) = ((πβπΉ)βπ))) |
67 | 66 | 3impib 1117 |
. 2
β’ ((πΊ β Word β β§ πΉ β Word β β§ π β
(0..^(β―βπΉ)))
β ((πβ(πΉ ++ πΊ))βπ) = ((πβπΉ)βπ)) |
68 | 67 | 3com12 1124 |
1
β’ ((πΉ β Word β β§ πΊ β Word β β§ π β
(0..^(β―βπΉ)))
β ((πβ(πΉ ++ πΊ))βπ) = ((πβπΉ)βπ)) |