Step | Hyp | Ref
| Expression |
1 | | signsv.p |
. . . . 5
⒠⨣ =
(π β {-1, 0, 1}, π β {-1, 0, 1} β¦
if(π = 0, π, π)) |
2 | | signsv.w |
. . . . 5
β’ π = {β¨(Baseβndx), {-1,
0, 1}β©, β¨(+gβndx), ⨣
β©} |
3 | 1, 2 | signswbase 33863 |
. . . 4
β’ {-1, 0,
1} = (Baseβπ) |
4 | 1, 2 | signswmnd 33866 |
. . . . 5
β’ π β Mnd |
5 | 4 | a1i 11 |
. . . 4
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β π β
Mnd) |
6 | | eldifi 4125 |
. . . . . . . . 9
β’ (πΉ β (Word β β
{β
}) β πΉ β
Word β) |
7 | | lencl 14487 |
. . . . . . . . 9
β’ (πΉ β Word β β
(β―βπΉ) β
β0) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
β’ (πΉ β (Word β β
{β
}) β (β―βπΉ) β
β0) |
9 | | eldifsn 4789 |
. . . . . . . . 9
β’ (πΉ β (Word β β
{β
}) β (πΉ β
Word β β§ πΉ β
β
)) |
10 | | hasheq0 14327 |
. . . . . . . . . . 11
β’ (πΉ β Word β β
((β―βπΉ) = 0
β πΉ =
β
)) |
11 | 10 | necon3bid 2983 |
. . . . . . . . . 10
β’ (πΉ β Word β β
((β―βπΉ) β 0
β πΉ β
β
)) |
12 | 11 | biimpar 476 |
. . . . . . . . 9
β’ ((πΉ β Word β β§ πΉ β β
) β
(β―βπΉ) β
0) |
13 | 9, 12 | sylbi 216 |
. . . . . . . 8
β’ (πΉ β (Word β β
{β
}) β (β―βπΉ) β 0) |
14 | | elnnne0 12490 |
. . . . . . . 8
β’
((β―βπΉ)
β β β ((β―βπΉ) β β0 β§
(β―βπΉ) β
0)) |
15 | 8, 13, 14 | sylanbrc 581 |
. . . . . . 7
β’ (πΉ β (Word β β
{β
}) β (β―βπΉ) β β) |
16 | 15 | adantr 479 |
. . . . . 6
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (β―βπΉ) β β) |
17 | | nnm1nn0 12517 |
. . . . . 6
β’
((β―βπΉ)
β β β ((β―βπΉ) β 1) β
β0) |
18 | 16, 17 | syl 17 |
. . . . 5
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β ((β―βπΉ) β 1) β
β0) |
19 | | nn0uz 12868 |
. . . . 5
β’
β0 = (β€β₯β0) |
20 | 18, 19 | eleqtrdi 2841 |
. . . 4
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β ((β―βπΉ) β 1) β
(β€β₯β0)) |
21 | | ccatws1cl 14570 |
. . . . . . . . . 10
β’ ((πΉ β Word β β§ πΎ β β) β (πΉ ++ β¨βπΎββ©) β Word
β) |
22 | 21 | adantr 479 |
. . . . . . . . 9
β’ (((πΉ β Word β β§ πΎ β β) β§ π β
(0...((β―βπΉ)
β 1))) β (πΉ ++
β¨βπΎββ©) β Word
β) |
23 | | wrdf 14473 |
. . . . . . . . 9
β’ ((πΉ ++ β¨βπΎββ©) β Word
β β (πΉ ++
β¨βπΎββ©):(0..^(β―β(πΉ ++ β¨βπΎββ©)))βΆβ) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
β’ (((πΉ β Word β β§ πΎ β β) β§ π β
(0...((β―βπΉ)
β 1))) β (πΉ ++
β¨βπΎββ©):(0..^(β―β(πΉ ++ β¨βπΎββ©)))βΆβ) |
25 | 7 | nn0zd 12588 |
. . . . . . . . . . . . 13
β’ (πΉ β Word β β
(β―βπΉ) β
β€) |
26 | | fzoval 13637 |
. . . . . . . . . . . . 13
β’
((β―βπΉ)
β β€ β (0..^(β―βπΉ)) = (0...((β―βπΉ) β 1))) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . 12
β’ (πΉ β Word β β
(0..^(β―βπΉ)) =
(0...((β―βπΉ)
β 1))) |
28 | 27 | adantr 479 |
. . . . . . . . . . 11
β’ ((πΉ β Word β β§ πΎ β β) β
(0..^(β―βπΉ)) =
(0...((β―βπΉ)
β 1))) |
29 | | fzossfz 13655 |
. . . . . . . . . . 11
β’
(0..^(β―βπΉ)) β (0...(β―βπΉ)) |
30 | 28, 29 | eqsstrrdi 4036 |
. . . . . . . . . 10
β’ ((πΉ β Word β β§ πΎ β β) β
(0...((β―βπΉ)
β 1)) β (0...(β―βπΉ))) |
31 | | s1cl 14556 |
. . . . . . . . . . . . . 14
β’ (πΎ β β β
β¨βπΎββ©
β Word β) |
32 | | ccatlen 14529 |
. . . . . . . . . . . . . 14
β’ ((πΉ β Word β β§
β¨βπΎββ©
β Word β) β (β―β(πΉ ++ β¨βπΎββ©)) = ((β―βπΉ) +
(β―ββ¨βπΎββ©))) |
33 | 31, 32 | sylan2 591 |
. . . . . . . . . . . . 13
β’ ((πΉ β Word β β§ πΎ β β) β
(β―β(πΉ ++
β¨βπΎββ©)) = ((β―βπΉ) +
(β―ββ¨βπΎββ©))) |
34 | | s1len 14560 |
. . . . . . . . . . . . . 14
β’
(β―ββ¨βπΎββ©) = 1 |
35 | 34 | oveq2i 7422 |
. . . . . . . . . . . . 13
β’
((β―βπΉ) +
(β―ββ¨βπΎββ©)) = ((β―βπΉ) + 1) |
36 | 33, 35 | eqtrdi 2786 |
. . . . . . . . . . . 12
β’ ((πΉ β Word β β§ πΎ β β) β
(β―β(πΉ ++
β¨βπΎββ©)) = ((β―βπΉ) + 1)) |
37 | 36 | oveq2d 7427 |
. . . . . . . . . . 11
β’ ((πΉ β Word β β§ πΎ β β) β
(0..^(β―β(πΉ ++
β¨βπΎββ©))) =
(0..^((β―βπΉ) +
1))) |
38 | 25 | adantr 479 |
. . . . . . . . . . . . 13
β’ ((πΉ β Word β β§ πΎ β β) β
(β―βπΉ) β
β€) |
39 | 38 | peano2zd 12673 |
. . . . . . . . . . . 12
β’ ((πΉ β Word β β§ πΎ β β) β
((β―βπΉ) + 1)
β β€) |
40 | | fzoval 13637 |
. . . . . . . . . . . 12
β’
(((β―βπΉ)
+ 1) β β€ β (0..^((β―βπΉ) + 1)) = (0...(((β―βπΉ) + 1) β
1))) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . 11
β’ ((πΉ β Word β β§ πΎ β β) β
(0..^((β―βπΉ) +
1)) = (0...(((β―βπΉ) + 1) β 1))) |
42 | 7 | nn0cnd 12538 |
. . . . . . . . . . . . . 14
β’ (πΉ β Word β β
(β―βπΉ) β
β) |
43 | | 1cnd 11213 |
. . . . . . . . . . . . . 14
β’ (πΉ β Word β β 1
β β) |
44 | 42, 43 | pncand 11576 |
. . . . . . . . . . . . 13
β’ (πΉ β Word β β
(((β―βπΉ) + 1)
β 1) = (β―βπΉ)) |
45 | 44 | adantr 479 |
. . . . . . . . . . . 12
β’ ((πΉ β Word β β§ πΎ β β) β
(((β―βπΉ) + 1)
β 1) = (β―βπΉ)) |
46 | 45 | oveq2d 7427 |
. . . . . . . . . . 11
β’ ((πΉ β Word β β§ πΎ β β) β
(0...(((β―βπΉ) +
1) β 1)) = (0...(β―βπΉ))) |
47 | 37, 41, 46 | 3eqtrd 2774 |
. . . . . . . . . 10
β’ ((πΉ β Word β β§ πΎ β β) β
(0..^(β―β(πΉ ++
β¨βπΎββ©))) = (0...(β―βπΉ))) |
48 | 30, 47 | sseqtrrd 4022 |
. . . . . . . . 9
β’ ((πΉ β Word β β§ πΎ β β) β
(0...((β―βπΉ)
β 1)) β (0..^(β―β(πΉ ++ β¨βπΎββ©)))) |
49 | 48 | sselda 3981 |
. . . . . . . 8
β’ (((πΉ β Word β β§ πΎ β β) β§ π β
(0...((β―βπΉ)
β 1))) β π
β (0..^(β―β(πΉ ++ β¨βπΎββ©)))) |
50 | 24, 49 | ffvelcdmd 7086 |
. . . . . . 7
β’ (((πΉ β Word β β§ πΎ β β) β§ π β
(0...((β―βπΉ)
β 1))) β ((πΉ ++
β¨βπΎββ©)βπ) β β) |
51 | 6, 50 | sylanl1 676 |
. . . . . 6
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(0...((β―βπΉ)
β 1))) β ((πΉ ++
β¨βπΎββ©)βπ) β β) |
52 | 51 | rexrd 11268 |
. . . . 5
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(0...((β―βπΉ)
β 1))) β ((πΉ ++
β¨βπΎββ©)βπ) β
β*) |
53 | | sgncl 33835 |
. . . . 5
β’ (((πΉ ++ β¨βπΎββ©)βπ) β β*
β (sgnβ((πΉ ++
β¨βπΎββ©)βπ)) β {-1, 0, 1}) |
54 | 52, 53 | syl 17 |
. . . 4
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π β
(0...((β―βπΉ)
β 1))) β (sgnβ((πΉ ++ β¨βπΎββ©)βπ)) β {-1, 0, 1}) |
55 | 1, 2 | signswplusg 33864 |
. . . 4
⒠⨣ =
(+gβπ) |
56 | | rexr 11264 |
. . . . . 6
β’ (πΎ β β β πΎ β
β*) |
57 | | sgncl 33835 |
. . . . . 6
β’ (πΎ β β*
β (sgnβπΎ) β
{-1, 0, 1}) |
58 | 56, 57 | syl 17 |
. . . . 5
β’ (πΎ β β β
(sgnβπΎ) β {-1,
0, 1}) |
59 | 58 | adantl 480 |
. . . 4
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (sgnβπΎ) β {-1, 0, 1}) |
60 | | id 22 |
. . . . . . . . 9
β’ (π = (((β―βπΉ) β 1) + 1) β π = (((β―βπΉ) β 1) +
1)) |
61 | 42, 43 | npcand 11579 |
. . . . . . . . . 10
β’ (πΉ β Word β β
(((β―βπΉ) β
1) + 1) = (β―βπΉ)) |
62 | 61 | adantr 479 |
. . . . . . . . 9
β’ ((πΉ β Word β β§ πΎ β β) β
(((β―βπΉ) β
1) + 1) = (β―βπΉ)) |
63 | 60, 62 | sylan9eqr 2792 |
. . . . . . . 8
β’ (((πΉ β Word β β§ πΎ β β) β§ π = (((β―βπΉ) β 1) + 1)) β π = (β―βπΉ)) |
64 | 63 | fveq2d 6894 |
. . . . . . 7
β’ (((πΉ β Word β β§ πΎ β β) β§ π = (((β―βπΉ) β 1) + 1)) β
((πΉ ++ β¨βπΎββ©)βπ) = ((πΉ ++ β¨βπΎββ©)β(β―βπΉ))) |
65 | | ccatws1ls 14587 |
. . . . . . . 8
β’ ((πΉ β Word β β§ πΎ β β) β ((πΉ ++ β¨βπΎββ©)β(β―βπΉ)) = πΎ) |
66 | 65 | adantr 479 |
. . . . . . 7
β’ (((πΉ β Word β β§ πΎ β β) β§ π = (((β―βπΉ) β 1) + 1)) β
((πΉ ++ β¨βπΎββ©)β(β―βπΉ)) = πΎ) |
67 | 64, 66 | eqtrd 2770 |
. . . . . 6
β’ (((πΉ β Word β β§ πΎ β β) β§ π = (((β―βπΉ) β 1) + 1)) β
((πΉ ++ β¨βπΎββ©)βπ) = πΎ) |
68 | 6, 67 | sylanl1 676 |
. . . . 5
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π =
(((β―βπΉ) β
1) + 1)) β ((πΉ ++
β¨βπΎββ©)βπ) = πΎ) |
69 | 68 | fveq2d 6894 |
. . . 4
β’ (((πΉ β (Word β β
{β
}) β§ πΎ β
β) β§ π =
(((β―βπΉ) β
1) + 1)) β (sgnβ((πΉ ++ β¨βπΎββ©)βπ)) = (sgnβπΎ)) |
70 | 3, 5, 20, 54, 55, 59, 69 | gsumnunsn 33850 |
. . 3
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (π
Ξ£g (π β (0...(((β―βπΉ) β 1) + 1)) β¦
(sgnβ((πΉ ++
β¨βπΎββ©)βπ)))) = ((π Ξ£g (π β
(0...((β―βπΉ)
β 1)) β¦ (sgnβ((πΉ ++ β¨βπΎββ©)βπ)))) ⨣ (sgnβπΎ))) |
71 | 6, 61 | syl 17 |
. . . . . . 7
β’ (πΉ β (Word β β
{β
}) β (((β―βπΉ) β 1) + 1) = (β―βπΉ)) |
72 | 71 | adantr 479 |
. . . . . 6
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (((β―βπΉ) β 1) + 1) = (β―βπΉ)) |
73 | 72 | oveq2d 7427 |
. . . . 5
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (0...(((β―βπΉ) β 1) + 1)) =
(0...(β―βπΉ))) |
74 | 73 | mpteq1d 5242 |
. . . 4
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (π β
(0...(((β―βπΉ)
β 1) + 1)) β¦ (sgnβ((πΉ ++ β¨βπΎββ©)βπ))) = (π β (0...(β―βπΉ)) β¦ (sgnβ((πΉ ++ β¨βπΎββ©)βπ)))) |
75 | 74 | oveq2d 7427 |
. . 3
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (π
Ξ£g (π β (0...(((β―βπΉ) β 1) + 1)) β¦
(sgnβ((πΉ ++
β¨βπΎββ©)βπ)))) = (π Ξ£g (π β
(0...(β―βπΉ))
β¦ (sgnβ((πΉ ++
β¨βπΎββ©)βπ))))) |
76 | | simpll 763 |
. . . . . . . . 9
β’ (((πΉ β Word β β§ πΎ β β) β§ π β
(0...((β―βπΉ)
β 1))) β πΉ
β Word β) |
77 | 31 | ad2antlr 723 |
. . . . . . . . 9
β’ (((πΉ β Word β β§ πΎ β β) β§ π β
(0...((β―βπΉ)
β 1))) β β¨βπΎββ© β Word
β) |
78 | 28 | eleq2d 2817 |
. . . . . . . . . 10
β’ ((πΉ β Word β β§ πΎ β β) β (π β
(0..^(β―βπΉ))
β π β
(0...((β―βπΉ)
β 1)))) |
79 | 78 | biimpar 476 |
. . . . . . . . 9
β’ (((πΉ β Word β β§ πΎ β β) β§ π β
(0...((β―βπΉ)
β 1))) β π
β (0..^(β―βπΉ))) |
80 | | ccatval1 14531 |
. . . . . . . . 9
β’ ((πΉ β Word β β§
β¨βπΎββ©
β Word β β§ π
β (0..^(β―βπΉ))) β ((πΉ ++ β¨βπΎββ©)βπ) = (πΉβπ)) |
81 | 76, 77, 79, 80 | syl3anc 1369 |
. . . . . . . 8
β’ (((πΉ β Word β β§ πΎ β β) β§ π β
(0...((β―βπΉ)
β 1))) β ((πΉ ++
β¨βπΎββ©)βπ) = (πΉβπ)) |
82 | 81 | fveq2d 6894 |
. . . . . . 7
β’ (((πΉ β Word β β§ πΎ β β) β§ π β
(0...((β―βπΉ)
β 1))) β (sgnβ((πΉ ++ β¨βπΎββ©)βπ)) = (sgnβ(πΉβπ))) |
83 | 82 | mpteq2dva 5247 |
. . . . . 6
β’ ((πΉ β Word β β§ πΎ β β) β (π β
(0...((β―βπΉ)
β 1)) β¦ (sgnβ((πΉ ++ β¨βπΎββ©)βπ))) = (π β (0...((β―βπΉ) β 1)) β¦
(sgnβ(πΉβπ)))) |
84 | 6, 83 | sylan 578 |
. . . . 5
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (π β
(0...((β―βπΉ)
β 1)) β¦ (sgnβ((πΉ ++ β¨βπΎββ©)βπ))) = (π β (0...((β―βπΉ) β 1)) β¦
(sgnβ(πΉβπ)))) |
85 | 84 | oveq2d 7427 |
. . . 4
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (π
Ξ£g (π β (0...((β―βπΉ) β 1)) β¦
(sgnβ((πΉ ++
β¨βπΎββ©)βπ)))) = (π Ξ£g (π β
(0...((β―βπΉ)
β 1)) β¦ (sgnβ(πΉβπ))))) |
86 | 85 | oveq1d 7426 |
. . 3
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β ((π
Ξ£g (π β (0...((β―βπΉ) β 1)) β¦
(sgnβ((πΉ ++
β¨βπΎββ©)βπ)))) ⨣ (sgnβπΎ)) = ((π Ξ£g (π β
(0...((β―βπΉ)
β 1)) β¦ (sgnβ(πΉβπ)))) ⨣ (sgnβπΎ))) |
87 | 70, 75, 86 | 3eqtr3d 2778 |
. 2
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (π
Ξ£g (π β (0...(β―βπΉ)) β¦ (sgnβ((πΉ ++ β¨βπΎββ©)βπ)))) = ((π Ξ£g (π β
(0...((β―βπΉ)
β 1)) β¦ (sgnβ(πΉβπ)))) ⨣ (sgnβπΎ))) |
88 | | eqid 2730 |
. . . . . . . 8
β’
(β―βπΉ) =
(β―βπΉ) |
89 | 88 | olci 862 |
. . . . . . 7
β’
((β―βπΉ)
β (0..^(β―βπΉ)) β¨ (β―βπΉ) = (β―βπΉ)) |
90 | 7, 19 | eleqtrdi 2841 |
. . . . . . . 8
β’ (πΉ β Word β β
(β―βπΉ) β
(β€β₯β0)) |
91 | | fzosplitsni 13747 |
. . . . . . . 8
β’
((β―βπΉ)
β (β€β₯β0) β ((β―βπΉ) β
(0..^((β―βπΉ) +
1)) β ((β―βπΉ) β (0..^(β―βπΉ)) β¨ (β―βπΉ) = (β―βπΉ)))) |
92 | 90, 91 | syl 17 |
. . . . . . 7
β’ (πΉ β Word β β
((β―βπΉ) β
(0..^((β―βπΉ) +
1)) β ((β―βπΉ) β (0..^(β―βπΉ)) β¨ (β―βπΉ) = (β―βπΉ)))) |
93 | 89, 92 | mpbiri 257 |
. . . . . 6
β’ (πΉ β Word β β
(β―βπΉ) β
(0..^((β―βπΉ) +
1))) |
94 | 93 | adantr 479 |
. . . . 5
β’ ((πΉ β Word β β§ πΎ β β) β
(β―βπΉ) β
(0..^((β―βπΉ) +
1))) |
95 | 94, 37 | eleqtrrd 2834 |
. . . 4
β’ ((πΉ β Word β β§ πΎ β β) β
(β―βπΉ) β
(0..^(β―β(πΉ ++
β¨βπΎββ©)))) |
96 | | signsv.t |
. . . . 5
β’ π = (π β Word β β¦ (π β
(0..^(β―βπ))
β¦ (π
Ξ£g (π β (0...π) β¦ (sgnβ(πβπ)))))) |
97 | | signsv.v |
. . . . 5
β’ π = (π β Word β β¦ Ξ£π β
(1..^(β―βπ))if(((πβπ)βπ) β ((πβπ)β(π β 1)), 1, 0)) |
98 | 1, 2, 96, 97 | signstfval 33873 |
. . . 4
β’ (((πΉ ++ β¨βπΎββ©) β Word
β β§ (β―βπΉ) β (0..^(β―β(πΉ ++ β¨βπΎββ©)))) β ((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) = (π Ξ£g (π β
(0...(β―βπΉ))
β¦ (sgnβ((πΉ ++
β¨βπΎββ©)βπ))))) |
99 | 21, 95, 98 | syl2anc 582 |
. . 3
β’ ((πΉ β Word β β§ πΎ β β) β ((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) = (π Ξ£g (π β
(0...(β―βπΉ))
β¦ (sgnβ((πΉ ++
β¨βπΎββ©)βπ))))) |
100 | 6, 99 | sylan 578 |
. 2
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β ((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) = (π Ξ£g (π β
(0...(β―βπΉ))
β¦ (sgnβ((πΉ ++
β¨βπΎββ©)βπ))))) |
101 | | fzo0end 13728 |
. . . . . 6
β’
((β―βπΉ)
β β β ((β―βπΉ) β 1) β
(0..^(β―βπΉ))) |
102 | 15, 101 | syl 17 |
. . . . 5
β’ (πΉ β (Word β β
{β
}) β ((β―βπΉ) β 1) β
(0..^(β―βπΉ))) |
103 | 1, 2, 96, 97 | signstfval 33873 |
. . . . 5
β’ ((πΉ β Word β β§
((β―βπΉ) β
1) β (0..^(β―βπΉ))) β ((πβπΉ)β((β―βπΉ) β 1)) = (π Ξ£g (π β
(0...((β―βπΉ)
β 1)) β¦ (sgnβ(πΉβπ))))) |
104 | 6, 102, 103 | syl2anc 582 |
. . . 4
β’ (πΉ β (Word β β
{β
}) β ((πβπΉ)β((β―βπΉ) β 1)) = (π Ξ£g (π β
(0...((β―βπΉ)
β 1)) β¦ (sgnβ(πΉβπ))))) |
105 | 104 | adantr 479 |
. . 3
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β ((πβπΉ)β((β―βπΉ) β 1)) = (π Ξ£g (π β
(0...((β―βπΉ)
β 1)) β¦ (sgnβ(πΉβπ))))) |
106 | 105 | oveq1d 7426 |
. 2
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β (((πβπΉ)β((β―βπΉ) β 1)) ⨣ (sgnβπΎ)) = ((π Ξ£g (π β
(0...((β―βπΉ)
β 1)) β¦ (sgnβ(πΉβπ)))) ⨣ (sgnβπΎ))) |
107 | 87, 100, 106 | 3eqtr4d 2780 |
1
β’ ((πΉ β (Word β β
{β
}) β§ πΎ β
β) β ((πβ(πΉ ++ β¨βπΎββ©))β(β―βπΉ)) = (((πβπΉ)β((β―βπΉ) β 1)) ⨣ (sgnβπΎ))) |